chore: robustifying for debug.byAsSorry (part 3) (#15120)

cf #14993 and #15119

Author: kim-em

Mathlib/Algebra/Associated/Basic.lean

@@ -845,7 +845,7 @@ theorem mul_eq_one_iff {x y : Associates α} : x * y = 1 ↔ x = 1 ∧ y = 1 :=
     (Quotient.inductionOn₂ x y fun a b h =>
       have : a * b ~ᵤ 1 := Quotient.exact h
       ⟨Quotient.sound <| associated_one_of_associated_mul_one this,
-        Quotient.sound <| associated_one_of_associated_mul_one <| by rwa [mul_comm] at this⟩)
+        Quotient.sound <| associated_one_of_associated_mul_one (b := a) (by rwa [mul_comm])⟩)
     (by simp (config := { contextual := true }))
 
 theorem units_eq_one (u : (Associates α)ˣ) : u = 1 :=

Mathlib/Algebra/Field/Basic.lean

@@ -228,7 +228,9 @@ noncomputable abbrev DivisionRing.ofIsUnitOrEqZero [Ring R] (h : ∀ a : R, IsUn
   toRing := ‹Ring R›
   __ := groupWithZeroOfIsUnitOrEqZero h
   nnqsmul := _
+  nnqsmul_def := fun q a => rfl
   qsmul := _
+  qsmul_def := fun q a => rfl
 
 /-- Constructs a `Field` structure on a `CommRing` consisting only of units and 0. -/
 -- See note [reducible non-instances]

Mathlib/Algebra/Field/Opposite.lean

@@ -34,13 +34,15 @@ instance instDivisionSemiring [DivisionSemiring α] : DivisionSemiring αᵐᵒ
   __ := instSemiring
   __ := instGroupWithZero
   nnqsmul := _
+  nnqsmul_def := fun q a => rfl
   nnratCast_def q := unop_injective $ by rw [unop_nnratCast, unop_div, unop_natCast, unop_natCast,
     NNRat.cast_def, div_eq_mul_inv, Nat.cast_comm]
 
 instance instDivisionRing [DivisionRing α] : DivisionRing αᵐᵒᵖ where
   __ := instRing
   __ := instDivisionSemiring
   qsmul := _
+  qsmul_def := fun q a => rfl
   ratCast_def q := unop_injective <| by rw [unop_ratCast, Rat.cast_def, unop_div,
     unop_natCast, unop_intCast, Int.commute_cast, div_eq_mul_inv]
 
@@ -60,13 +62,15 @@ instance instDivisionSemiring [DivisionSemiring α] : DivisionSemiring αᵃᵒ
   __ := instSemiring
   __ := instGroupWithZero
   nnqsmul := _
+  nnqsmul_def := fun q a => rfl
   nnratCast_def q := unop_injective $ by rw [unop_nnratCast, unop_div, unop_natCast, unop_natCast,
     NNRat.cast_def, div_eq_mul_inv]
 
 instance instDivisionRing [DivisionRing α] : DivisionRing αᵃᵒᵖ where
   __ := instRing
   __ := instDivisionSemiring
   qsmul := _
+  qsmul_def := fun q a => rfl
   ratCast_def q := unop_injective <| by rw [unop_ratCast, Rat.cast_def, unop_div, unop_natCast,
     unop_intCast, div_eq_mul_inv]
 

Mathlib/Algebra/Group/Submonoid/Operations.lean

@@ -297,13 +297,15 @@ theorem map_id (S : Submonoid M) : S.map (MonoidHom.id M) = S :=
 
 section GaloisCoinsertion
 
-variable {ι : Type*} {f : F} (hf : Function.Injective f)
+variable {ι : Type*} {f : F}
 
 /-- `map f` and `comap f` form a `GaloisCoinsertion` when `f` is injective. -/
 @[to_additive " `map f` and `comap f` form a `GaloisCoinsertion` when `f` is injective. "]
-def gciMapComap : GaloisCoinsertion (map f) (comap f) :=
+def gciMapComap (hf : Function.Injective f) : GaloisCoinsertion (map f) (comap f) :=
   (gc_map_comap f).toGaloisCoinsertion fun S x => by simp [mem_comap, mem_map, hf.eq_iff]
 
+variable (hf : Function.Injective f)
+
 @[to_additive]
 theorem comap_map_eq_of_injective (S : Submonoid M) : (S.map f).comap f = S :=
   (gciMapComap hf).u_l_eq _

Mathlib/Algebra/Order/Group/OrderIso.lean

@@ -35,7 +35,7 @@ variable (α)
 @[to_additive (attr := simps!) "`x ↦ -x` as an order-reversing equivalence."]
 def OrderIso.inv : α ≃o αᵒᵈ where
   toEquiv := (Equiv.inv α).trans OrderDual.toDual
-  map_rel_iff' {_ _} := @inv_le_inv_iff α _ _ _ _ _ _
+  map_rel_iff' {_ _} := inv_le_inv_iff (α := α)
 
 end
 
@@ -55,7 +55,7 @@ theorem le_inv' : a ≤ b⁻¹ ↔ b ≤ a⁻¹ :=
 @[to_additive (attr := simps!) "`x ↦ a - x` as an order-reversing equivalence."]
 def OrderIso.divLeft (a : α) : α ≃o αᵒᵈ where
   toEquiv := (Equiv.divLeft a).trans OrderDual.toDual
-  map_rel_iff' {_ _} := @div_le_div_iff_left α _ _ _ _ _ _ _
+  map_rel_iff' {_ _} := div_le_div_iff_left (α := α) _
 
 end TypeclassesLeftRightLE
 

Mathlib/Algebra/Order/Hom/Monoid.lean

@@ -182,15 +182,18 @@ end OrderedZero
 section OrderedAddCommGroup
 
 variable [OrderedAddCommGroup α] [OrderedAddCommMonoid β] [i : FunLike F α β]
-variable [iamhc : AddMonoidHomClass F α β] (f : F)
+variable (f : F)
 
-theorem monotone_iff_map_nonneg : Monotone (f : α → β) ↔ ∀ a, 0 ≤ a → 0 ≤ f a :=
+theorem monotone_iff_map_nonneg [iamhc : AddMonoidHomClass F α β] :
+    Monotone (f : α → β) ↔ ∀ a, 0 ≤ a → 0 ≤ f a :=
   ⟨fun h a => by
     rw [← map_zero f]
     apply h, fun h a b hl => by
     rw [← sub_add_cancel b a, map_add f]
     exact le_add_of_nonneg_left (h _ <| sub_nonneg.2 hl)⟩
 
+variable [iamhc : AddMonoidHomClass F α β]
+
 theorem antitone_iff_map_nonpos : Antitone (f : α → β) ↔ ∀ a, 0 ≤ a → f a ≤ 0 :=
   monotone_toDual_comp_iff.symm.trans <| monotone_iff_map_nonneg (β := βᵒᵈ) (iamhc := iamhc) _
 
@@ -202,7 +205,8 @@ theorem antitone_iff_map_nonneg : Antitone (f : α → β) ↔ ∀ a ≤ 0, 0 
 
 variable [CovariantClass β β (· + ·) (· < ·)]
 
-theorem strictMono_iff_map_pos : StrictMono (f : α → β) ↔ ∀ a, 0 < a → 0 < f a := by
+theorem strictMono_iff_map_pos [iamhc : AddMonoidHomClass F α β]  :
+    StrictMono (f : α → β) ↔ ∀ a, 0 < a → 0 < f a := by
   refine ⟨fun h a => ?_, fun h a b hl => ?_⟩
   · rw [← map_zero f]
     apply h

Mathlib/CategoryTheory/Category/GaloisConnection.lean

@@ -28,8 +28,10 @@ def GaloisConnection.adjunction {l : X → Y} {u : Y → X} (gc : GaloisConnecti
     gc.monotone_l.functor ⊣ gc.monotone_u.functor :=
   CategoryTheory.Adjunction.mkOfHomEquiv
     { homEquiv := fun X Y =>
-        ⟨fun f => CategoryTheory.homOfLE (gc.le_u f.le),
-         fun f => CategoryTheory.homOfLE (gc.l_le f.le), _, _⟩ }
+        { toFun := fun f => CategoryTheory.homOfLE (gc.le_u f.le)
+          invFun := fun f => CategoryTheory.homOfLE (gc.l_le f.le)
+          left_inv := by aesop_cat
+          right_inv := by aesop_cat } }
 
 end
 

Mathlib/CategoryTheory/ComposableArrows.lean

@@ -481,14 +481,13 @@ abbrev δlast (F : ComposableArrows C (n + 1)) := δlastFunctor.obj F
 section
 
 variable {F G : ComposableArrows C (n + 1)}
-  (α : F.obj' 0 ⟶ G.obj' 0)
-  (β : F.δ₀ ⟶ G.δ₀)
-  (w : F.map' 0 1 ≫ app' β 0 = α ≫ G.map' 0 1)
+
 
 /-- Inductive construction of morphisms in `ComposableArrows C (n + 1)`: in order to construct
 a morphism `F ⟶ G`, it suffices to provide `α : F.obj' 0 ⟶ G.obj' 0` and `β : F.δ₀ ⟶ G.δ₀`
 such that `F.map' 0 1 ≫ app' β 0 = α ≫ G.map' 0 1`. -/
-def homMkSucc : F ⟶ G :=
+def homMkSucc (α : F.obj' 0 ⟶ G.obj' 0) (β : F.δ₀ ⟶ G.δ₀)
+    (w : F.map' 0 1 ≫ app' β 0 = α ≫ G.map' 0 1) : F ⟶ G :=
   homMk
     (fun i => match i with
       | ⟨0, _⟩ => α
@@ -498,6 +497,9 @@ def homMkSucc : F ⟶ G :=
       · exact w
       · exact naturality' β i (i + 1))
 
+variable (α : F.obj' 0 ⟶ G.obj' 0) (β : F.δ₀ ⟶ G.δ₀)
+  (w : F.map' 0 1 ≫ app' β 0 = α ≫ G.map' 0 1)
+
 @[simp]
 lemma homMkSucc_app_zero : (homMkSucc α β w).app 0 = α := rfl
 

Mathlib/CategoryTheory/Core.lean

@@ -72,7 +72,7 @@ variable {C} {G : Type u₂} [Groupoid.{v₂} G]
 /-- A functor from a groupoid to a category C factors through the core of C. -/
 def functorToCore (F : G ⥤ C) : G ⥤ Core C where
   obj X := F.obj X
-  map f := ⟨F.map f, F.map (Groupoid.inv f), _, _⟩
+  map f := { hom := F.map f, inv := F.map (Groupoid.inv f) }
 
 /-- We can functorially associate to any functor from a groupoid to the core of a category `C`,
 a functor from the groupoid to `C`, simply by composing with the embedding `Core C ⥤ C`.

Mathlib/CategoryTheory/FiberedCategory/HomLift.lean

@@ -71,14 +71,16 @@ protected lemma id {p : 𝒳 ⥤ 𝒮} {R : 𝒮} {a : 𝒳} (ha : p.obj a = R)
 
 section
 
-variable {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ]
+variable {R S : 𝒮} {a b : 𝒳}
 
-lemma domain_eq : p.obj a = R := by
+lemma domain_eq (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ] : p.obj a = R := by
   subst_hom_lift p f φ; rfl
 
-lemma codomain_eq : p.obj b = S := by
+lemma codomain_eq (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ] : p.obj b = S := by
   subst_hom_lift p f φ; rfl
 
+variable (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ]
+
 lemma fac : f = eqToHom (domain_eq p f φ).symm ≫ p.map φ ≫ eqToHom (codomain_eq p f φ) := by
   subst_hom_lift p f φ; simp
 

Mathlib/CategoryTheory/LiftingProperties/Adjunction.lean

@@ -30,16 +30,18 @@ namespace CommSq
 section
 
 variable {A B : C} {X Y : D} {i : A ⟶ B} {p : X ⟶ Y} {u : G.obj A ⟶ X} {v : G.obj B ⟶ Y}
-  (sq : CommSq u (G.map i) p v) (adj : G ⊣ F)
 
 /-- When we have an adjunction `G ⊣ F`, any commutative square where the left
 map is of the form `G.map i` and the right map is `p` has an "adjoint" commutative
 square whose left map is `i` and whose right map is `F.map p`. -/
-theorem right_adjoint : CommSq (adj.homEquiv _ _ u) i (F.map p) (adj.homEquiv _ _ v) :=
+theorem right_adjoint (sq : CommSq u (G.map i) p v) (adj : G ⊣ F) :
+    CommSq (adj.homEquiv _ _ u) i (F.map p) (adj.homEquiv _ _ v) :=
   ⟨by
     simp only [Adjunction.homEquiv_unit, assoc, ← F.map_comp, sq.w]
     rw [F.map_comp, Adjunction.unit_naturality_assoc]⟩
 
+variable (sq : CommSq u (G.map i) p v) (adj : G ⊣ F)
+
 /-- The liftings of a commutative are in bijection with the liftings of its (right)
 adjoint square. -/
 def rightAdjointLiftStructEquiv : sq.LiftStruct ≃ (sq.right_adjoint adj).LiftStruct where
@@ -72,19 +74,22 @@ end
 section
 
 variable {A B : C} {X Y : D} {i : A ⟶ B} {p : X ⟶ Y} {u : A ⟶ F.obj X} {v : B ⟶ F.obj Y}
-  (sq : CommSq u i (F.map p) v) (adj : G ⊣ F)
 
 /-- When we have an adjunction `G ⊣ F`, any commutative square where the left
 map is of the form `i` and the right map is `F.map p` has an "adjoint" commutative
 square whose left map is `G.map i` and whose right map is `p`. -/
-theorem left_adjoint : CommSq ((adj.homEquiv _ _).symm u) (G.map i) p ((adj.homEquiv _ _).symm v) :=
+theorem left_adjoint (sq : CommSq u i (F.map p) v) (adj : G ⊣ F) :
+    CommSq ((adj.homEquiv _ _).symm u) (G.map i) p ((adj.homEquiv _ _).symm v) :=
   ⟨by
     simp only [Adjunction.homEquiv_counit, assoc, ← G.map_comp_assoc, ← sq.w]
     rw [G.map_comp, assoc, Adjunction.counit_naturality]⟩
 
+variable (sq : CommSq u i (F.map p) v) (adj : G ⊣ F)
+
 /-- The liftings of a commutative are in bijection with the liftings of its (left)
 adjoint square. -/
-def leftAdjointLiftStructEquiv : sq.LiftStruct ≃ (sq.left_adjoint adj).LiftStruct where
+def leftAdjointLiftStructEquiv :
+    sq.LiftStruct ≃ (sq.left_adjoint adj).LiftStruct where
   toFun l :=
     { l := (adj.homEquiv _ _).symm l.l
       fac_left := by rw [← adj.homEquiv_naturality_left_symm, l.fac_left]

Mathlib/Control/LawfulFix.lean

@@ -158,9 +158,8 @@ theorem fix_le {X : (a : _) → Part <| β a} (hX : f X ≤ X) : Part.fix f ≤
     · apply hX
 
 variable {f}
-variable (hc : Continuous f)
 
-theorem fix_eq : Part.fix f = f (Part.fix f) := by
+theorem fix_eq (hc : Continuous f) : Part.fix f = f (Part.fix f) := by
   rw [fix_eq_ωSup f, hc]
   apply le_antisymm
   · apply ωSup_le_ωSup_of_le _

Mathlib/Data/Fintype/Card.lean

@@ -431,7 +431,8 @@ theorem card_lt_of_injective_of_not_mem (f : α → β) (h : Function.Injective
   calc
     card α = (univ.map ⟨f, h⟩).card := (card_map _).symm
     _ < card β :=
-      Finset.card_lt_univ_of_not_mem <| by rwa [← mem_coe, coe_map, coe_univ, Set.image_univ]
+      Finset.card_lt_univ_of_not_mem (x := b) <| by
+        rwa [← mem_coe, coe_map, coe_univ, Set.image_univ]
 
 theorem card_lt_of_injective_not_surjective (f : α → β) (h : Function.Injective f)
     (h' : ¬Function.Surjective f) : card α < card β :=
@@ -755,7 +756,7 @@ theorem Fintype.card_subtype_le [Fintype α] (p : α → Prop) [DecidablePred p]
 
 theorem Fintype.card_subtype_lt [Fintype α] {p : α → Prop} [DecidablePred p] {x : α} (hx : ¬p x) :
     Fintype.card { x // p x } < Fintype.card α :=
-  Fintype.card_lt_of_injective_of_not_mem (↑) Subtype.coe_injective <| by
+  Fintype.card_lt_of_injective_of_not_mem (b := x) (↑) Subtype.coe_injective <| by
     rwa [Subtype.range_coe_subtype]
 
 theorem Fintype.card_subtype [Fintype α] (p : α → Prop) [DecidablePred p] :

Mathlib/Deprecated/Group.lean

@@ -161,7 +161,7 @@ end IsMonoidHom
 homomorphism."]
 theorem IsMulHom.to_isMonoidHom [MulOneClass α] [Group β] {f : α → β} (hf : IsMulHom f) :
     IsMonoidHom f :=
-  { map_one := mul_right_eq_self.1 <| by rw [← hf.map_mul, one_mul]
+  { map_one := (mul_right_eq_self (a := f 1)).1 <| by rw [← hf.map_mul, one_mul]
     map_mul := hf.map_mul }
 
 namespace IsMonoidHom

Mathlib/Order/Irreducible.lean

@@ -185,7 +185,7 @@ variable [WellFoundedGT α]
 elements. This is the order-theoretic analogue of prime factorisation. -/
 theorem exists_infIrred_decomposition (a : α) :
     ∃ s : Finset α, s.inf id = a ∧ ∀ ⦃b⦄, b ∈ s → InfIrred b :=
-  @exists_supIrred_decomposition αᵒᵈ _ _ _ _
+  exists_supIrred_decomposition (α := αᵒᵈ) _
 
 end SemilatticeInf