fix: remove references to non-heterogenous operators in theorem statements (#8086)

Some of these are likely porting errors.
Statements should always be about the heterogenous versions because these are the ones with notation.

For places where we are abusing defeq, this debuts the trick of using `(by exact a : B) = (by exact a1) + (by exact b2)` to ensure the `=` and `+` are typed as `B` instead of `A`.

Author: eric-wieser

Mathlib/Algebra/Category/GroupCat/Colimits.lean

@@ -128,17 +128,18 @@ theorem quot_zero : Quot.mk Setoid.r zero = (0 : ColimitType.{w} F) :=
 #align AddCommGroup.colimits.quot_zero AddCommGroupCat.Colimits.quot_zero
 
 @[simp]
-theorem quot_neg (x) : Quot.mk Setoid.r (neg x) =
+theorem quot_neg (x) :
     -- Porting note : force Lean to treat `ColimitType F` no as `Quot _`
-    Neg.neg (α := ColimitType.{w} F) (Quot.mk Setoid.r x : ColimitType.{w} F) :=
+    (by exact Quot.mk Setoid.r (neg x) : ColimitType.{w} F) =
+      -(by exact Quot.mk Setoid.r x) :=
   rfl
 #align AddCommGroup.colimits.quot_neg AddCommGroupCat.Colimits.quot_neg
 
 @[simp]
 theorem quot_add (x y) :
-    Quot.mk Setoid.r (add x y) =
-    -- Porting note : force Lean to treat `ColimitType F` no as `Quot _`
-    Add.add (α := ColimitType.{w} F) (Quot.mk Setoid.r x) (Quot.mk Setoid.r y) :=
+    (by exact Quot.mk Setoid.r (add x y) : ColimitType.{w} F) =
+      -- Porting note : force Lean to treat `ColimitType F` no as `Quot _`
+      (by exact Quot.mk Setoid.r x) + (by exact Quot.mk Setoid.r y) :=
   rfl
 #align AddCommGroup.colimits.quot_add AddCommGroupCat.Colimits.quot_add
 
@@ -220,7 +221,7 @@ def descMorphism (s : Cocone F) : colimit.{w} F ⟶ s.pt where
   toFun := descFun F s
   map_zero' := rfl
   -- Porting note : in `mathlib3`, nothing needs to be done after `induction`
-  map_add' x y := Quot.induction_on₂ x y fun _ _ => by dsimp [(· + ·)]; rw [←quot_add F]; rfl
+  map_add' x y := Quot.induction_on₂ x y fun _ _ => by dsimp; rw [←quot_add F]; rfl
 #align AddCommGroup.colimits.desc_morphism AddCommGroupCat.Colimits.descMorphism
 
 /-- Evidence that the proposed colimit is the colimit. -/

Mathlib/Algebra/Category/Ring/Colimits.lean

@@ -191,26 +191,26 @@ theorem quot_one : Quot.mk Setoid.r one = (1 : ColimitType F) :=
 @[simp]
 theorem quot_neg (x : Prequotient F) :
     -- Porting note : Lean can't see `Quot.mk Setoid.r x` is a `ColimitType F` even with type
-    -- annotation so use `Neg.neg (α := ColimitType F)` to tell Lean negation happens inside
-    -- `ColimitType F`.
-    (Quot.mk Setoid.r (neg x) : ColimitType F) =
-    Neg.neg (α := ColimitType F) (Quot.mk Setoid.r x) :=
+    -- annotation unless we use `by exact` to change the elaboration order.
+    (by exact Quot.mk Setoid.r (neg x) : ColimitType F) = -(by exact Quot.mk Setoid.r x) :=
   rfl
 #align CommRing.colimits.quot_neg CommRingCat.Colimits.quot_neg
 
 -- Porting note : Lean can't see `Quot.mk Setoid.r x` is a `ColimitType F` even with type annotation
--- so use `Add.add (α := ColimitType F)` to tell Lean addition happens inside `ColimitType F`.
+-- unless we use `by exact` to change the elaboration order.
 @[simp]
 theorem quot_add (x y) :
-    Quot.mk Setoid.r (add x y) = Add.add (α := ColimitType F) (Quot.mk _ x) (Quot.mk _ y) :=
+    (by exact Quot.mk Setoid.r (add x y) : ColimitType F) =
+      (by exact Quot.mk _ x) + (by exact Quot.mk _ y) :=
   rfl
 #align CommRing.colimits.quot_add CommRingCat.Colimits.quot_add
 
 -- Porting note : Lean can't see `Quot.mk Setoid.r x` is a `ColimitType F` even with type annotation
--- so use `Mul.mul (α := ColimitType F)` to tell Lean multiplication happens inside `ColimitType F`.
+-- unless we use `by exact` to change the elaboration order.
 @[simp]
 theorem quot_mul (x y) :
-    Quot.mk Setoid.r (mul x y) = Mul.mul (α := ColimitType F) (Quot.mk _ x) (Quot.mk _ y) :=
+    (by exact Quot.mk Setoid.r (mul x y) : ColimitType F) =
+      (by exact Quot.mk _ x) * (by exact Quot.mk _ y) :=
   rfl
 #align CommRing.colimits.quot_mul CommRingCat.Colimits.quot_mul
 
@@ -309,7 +309,7 @@ def descMorphism (s : Cocone F) : colimit F ⟶ s.pt where
   map_zero' := rfl
   map_add' x y := by
     refine Quot.induction_on₂ x y fun a b => ?_
-    dsimp [descFun, (· + ·)]
+    dsimp [descFun]
     rw [←quot_add]
     rfl
   map_mul' x y := by exact Quot.induction_on₂ x y fun a b => rfl

Mathlib/Algebra/CharP/Two.lean

@@ -73,7 +73,7 @@ theorem neg_eq' : Neg.neg = (id : R → R) :=
 theorem sub_eq_add (x y : R) : x - y = x + y := by rw [sub_eq_add_neg, neg_eq]
 #align char_two.sub_eq_add CharTwo.sub_eq_add
 
-theorem sub_eq_add' : Sub.sub = ((· + ·) : R → R → R) :=
+theorem sub_eq_add' : HSub.hSub = ((· + ·) : R → R → R) :=
   funext fun x => funext fun y => sub_eq_add x y
 #align char_two.sub_eq_add' CharTwo.sub_eq_add'
 

Mathlib/Algebra/Free.lean

@@ -250,7 +250,7 @@ theorem traverse_mul (x y : FreeMagma α) :
 
 @[to_additive (attr := simp)]
 theorem traverse_mul' :
-    Function.comp (traverse F) ∘ @Mul.mul (FreeMagma α) _ = fun x y ↦
+    Function.comp (traverse F) ∘ (HMul.hMul : FreeMagma α → FreeMagma α → FreeMagma α) = fun x y ↦
       (· * ·) <$> traverse F x <*> traverse F y := rfl
 #align free_magma.traverse_mul' FreeMagma.traverse_mul'
 
@@ -664,8 +664,9 @@ theorem traverse_mul (x y : FreeSemigroup α) :
 
 @[to_additive (attr := simp)]
 theorem traverse_mul' :
-    Function.comp (traverse F) ∘ @Mul.mul (FreeSemigroup α) _ = fun x y ↦
-      (· * ·) <$> traverse F x <*> traverse F y := funext fun x ↦ funext fun y ↦ traverse_mul F x y
+    Function.comp (traverse F) ∘ (HMul.hMul : FreeSemigroup α → FreeSemigroup α → FreeSemigroup α) =
+      fun x y ↦ (· * ·) <$> traverse F x <*> traverse F y :=
+  funext fun x ↦ funext fun y ↦ traverse_mul F x y
 #align free_semigroup.traverse_mul' FreeSemigroup.traverse_mul'
 
 end

Mathlib/Algebra/Group/Ext.lean

@@ -19,14 +19,20 @@ in `Algebra.Group.Defs`.
 To get equality of `npow` etc, we define a monoid homomorphism between two monoid structures on the
 same type, then apply lemmas like `MonoidHom.map_div`, `MonoidHom.map_pow` etc.
 
+To refer to the `*` operator of a particular instance `i`, we use
+`(letI := i; HMul.hMul : M → M → M)` instead of `i.mul` (which elaborates to `Mul.mul`), as the
+former uses `HMul.hMul` which is the canonical spelling.
+
 ## Tags
 monoid, group, extensionality
 -/
 
 universe u
 
 @[to_additive (attr := ext)]
-theorem Monoid.ext {M : Type u} ⦃m₁ m₂ : Monoid M⦄ (h_mul : m₁.mul = m₂.mul) : m₁ = m₂ := by
+theorem Monoid.ext {M : Type u} ⦃m₁ m₂ : Monoid M⦄
+    (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M)) :
+    m₁ = m₂ := by
   have : m₁.toMulOneClass = m₂.toMulOneClass := MulOneClass.ext h_mul
   have h₁ : m₁.one = m₂.one := congr_arg (·.one) (this)
   let f : @MonoidHom M M m₁.toMulOneClass m₂.toMulOneClass :=
@@ -50,7 +56,8 @@ theorem CommMonoid.toMonoid_injective {M : Type u} :
 #align add_comm_monoid.to_add_monoid_injective AddCommMonoid.toAddMonoid_injective
 
 @[to_additive (attr := ext)]
-theorem CommMonoid.ext {M : Type*} ⦃m₁ m₂ : CommMonoid M⦄ (h_mul : m₁.mul = m₂.mul) : m₁ = m₂ :=
+theorem CommMonoid.ext {M : Type*} ⦃m₁ m₂ : CommMonoid M⦄
+    (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M)) : m₁ = m₂ :=
   CommMonoid.toMonoid_injective <| Monoid.ext h_mul
 #align comm_monoid.ext CommMonoid.ext
 #align add_comm_monoid.ext AddCommMonoid.ext
@@ -64,7 +71,8 @@ theorem LeftCancelMonoid.toMonoid_injective {M : Type u} :
 #align add_left_cancel_monoid.to_add_monoid_injective AddLeftCancelMonoid.toAddMonoid_injective
 
 @[to_additive (attr := ext)]
-theorem LeftCancelMonoid.ext {M : Type u} ⦃m₁ m₂ : LeftCancelMonoid M⦄ (h_mul : m₁.mul = m₂.mul) :
+theorem LeftCancelMonoid.ext {M : Type u} ⦃m₁ m₂ : LeftCancelMonoid M⦄
+    (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M)) :
     m₁ = m₂ :=
   LeftCancelMonoid.toMonoid_injective <| Monoid.ext h_mul
 #align left_cancel_monoid.ext LeftCancelMonoid.ext
@@ -79,7 +87,8 @@ theorem RightCancelMonoid.toMonoid_injective {M : Type u} :
 #align add_right_cancel_monoid.to_add_monoid_injective AddRightCancelMonoid.toAddMonoid_injective
 
 @[to_additive (attr := ext)]
-theorem RightCancelMonoid.ext {M : Type u} ⦃m₁ m₂ : RightCancelMonoid M⦄ (h_mul : m₁.mul = m₂.mul) :
+theorem RightCancelMonoid.ext {M : Type u} ⦃m₁ m₂ : RightCancelMonoid M⦄
+    (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M))  :
     m₁ = m₂ :=
   RightCancelMonoid.toMonoid_injective <| Monoid.ext h_mul
 #align right_cancel_monoid.ext RightCancelMonoid.ext
@@ -94,7 +103,8 @@ theorem CancelMonoid.toLeftCancelMonoid_injective {M : Type u} :
 #align add_cancel_monoid.to_left_cancel_add_monoid_injective AddCancelMonoid.toAddLeftCancelMonoid_injective
 
 @[to_additive (attr := ext)]
-theorem CancelMonoid.ext {M : Type*} ⦃m₁ m₂ : CancelMonoid M⦄ (h_mul : m₁.mul = m₂.mul) :
+theorem CancelMonoid.ext {M : Type*} ⦃m₁ m₂ : CancelMonoid M⦄
+    (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M)) :
     m₁ = m₂ :=
   CancelMonoid.toLeftCancelMonoid_injective <| LeftCancelMonoid.ext h_mul
 #align cancel_monoid.ext CancelMonoid.ext
@@ -111,15 +121,17 @@ theorem CancelCommMonoid.toCommMonoid_injective {M : Type u} :
 #align add_cancel_comm_monoid.to_add_comm_monoid_injective AddCancelCommMonoid.toAddCommMonoid_injective
 
 @[to_additive (attr := ext)]
-theorem CancelCommMonoid.ext {M : Type*} ⦃m₁ m₂ : CancelCommMonoid M⦄ (h_mul : m₁.mul = m₂.mul) :
+theorem CancelCommMonoid.ext {M : Type*} ⦃m₁ m₂ : CancelCommMonoid M⦄
+    (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M)) :
     m₁ = m₂ :=
   CancelCommMonoid.toCommMonoid_injective <| CommMonoid.ext h_mul
 #align cancel_comm_monoid.ext CancelCommMonoid.ext
 #align add_cancel_comm_monoid.ext AddCancelCommMonoid.ext
 
 @[to_additive (attr := ext)]
-theorem DivInvMonoid.ext {M : Type*} ⦃m₁ m₂ : DivInvMonoid M⦄ (h_mul : m₁.mul = m₂.mul)
-    (h_inv : m₁.inv = m₂.inv) : m₁ = m₂ := by
+theorem DivInvMonoid.ext {M : Type*} ⦃m₁ m₂ : DivInvMonoid M⦄
+    (h_mul : (letI := m₁; HMul.hMul : M → M → M) = (letI := m₂; HMul.hMul : M → M → M))
+    (h_inv : (letI := m₁; Inv.inv : M → M) = (letI := m₂; Inv.inv : M → M)) : m₁ = m₂ := by
   have h_mon := Monoid.ext h_mul
   have h₁ : m₁.one = m₂.one := congr_arg (·.one) h_mon
   let f : @MonoidHom M M m₁.toMulOneClass m₂.toMulOneClass :=

Mathlib/Algebra/Order/LatticeGroup.lean

@@ -237,7 +237,7 @@ theorem neg_eq_one_iff' {a : α} : a⁻ = 1 ↔ a⁻¹ ≤ 1 :=
 #align lattice_ordered_comm_group.neg_eq_zero_iff' LatticeOrderedGroup.neg_eq_zero_iff'
 
 @[to_additive]
-theorem neg_eq_one_iff [CovariantClass α α Mul.mul LE.le] {a : α} : a⁻ = 1 ↔ 1 ≤ a := by
+theorem neg_eq_one_iff [CovariantClass α α HMul.hMul LE.le] {a : α} : a⁻ = 1 ↔ 1 ≤ a := by
   rw [le_antisymm_iff, neg_le_one_iff, inv_le_one', and_iff_left (one_le_neg _)]
 #align lattice_ordered_comm_group.neg_eq_one_iff LatticeOrderedGroup.neg_eq_one_iff
 #align lattice_ordered_comm_group.neg_eq_zero_iff LatticeOrderedGroup.neg_eq_zero_iff

Mathlib/Algebra/Order/Monoid/OrderDual.lean

@@ -88,7 +88,7 @@ instance orderedCommMonoid [OrderedCommMonoid α] : OrderedCommMonoid αᵒᵈ :
 
 @[to_additive OrderDual.OrderedCancelAddCommMonoid.to_contravariantClass]
 instance OrderedCancelCommMonoid.to_contravariantClass [OrderedCancelCommMonoid α] :
-    ContravariantClass αᵒᵈ αᵒᵈ Mul.mul LE.le where
+    ContravariantClass αᵒᵈ αᵒᵈ HMul.hMul LE.le where
     -- Porting note: We need to specify the implicit arguments here because of
     -- https://github.com/leanprover/lean4/issues/1892
     -- We should be able to remove this after nightly-2022-11-30 arrives.

Mathlib/Geometry/Manifold/MFDeriv.lean

@@ -1616,11 +1616,11 @@ theorem MDifferentiable.add (hf : MDifferentiable I 𝓘(𝕜, E') f)
   (hf x).add (hg x)
 #align mdifferentiable.add MDifferentiable.add
 
--- porting note: forcing types using `@Add.add`
+-- porting note: forcing types using `by exact`
 theorem mfderiv_add (hf : MDifferentiableAt I 𝓘(𝕜, E') f z)
     (hg : MDifferentiableAt I 𝓘(𝕜, E') g z) :
-    (mfderiv I 𝓘(𝕜, E') (f + g) z : TangentSpace I z →L[𝕜] E') =
-      @Add.add (TangentSpace I z →L[𝕜] E') _ (mfderiv I 𝓘(𝕜, E') f z) (mfderiv I 𝓘(𝕜, E') g z) :=
+    (by exact mfderiv I 𝓘(𝕜, E') (f + g) z : TangentSpace I z →L[𝕜] E') =
+      (by exact mfderiv I 𝓘(𝕜, E') f z) + (by exact mfderiv I 𝓘(𝕜, E') g z) :=
   (hf.hasMFDerivAt.add hg.hasMFDerivAt).mfderiv
 #align mfderiv_add mfderiv_add
 
@@ -1693,8 +1693,8 @@ theorem MDifferentiable.sub (hf : MDifferentiable I 𝓘(𝕜, E') f)
 
 theorem mfderiv_sub (hf : MDifferentiableAt I 𝓘(𝕜, E') f z)
     (hg : MDifferentiableAt I 𝓘(𝕜, E') g z) :
-    (mfderiv I 𝓘(𝕜, E') (f - g) z : TangentSpace I z →L[𝕜] E') =
-      @Sub.sub (TangentSpace I z →L[𝕜] E') _ (mfderiv I 𝓘(𝕜, E') f z) (mfderiv I 𝓘(𝕜, E') g z) :=
+    (by exact mfderiv I 𝓘(𝕜, E') (f - g) z : TangentSpace I z →L[𝕜] E') =
+      (by exact mfderiv I 𝓘(𝕜, E') f z) - (by exact mfderiv I 𝓘(𝕜, E') g z) :=
   (hf.hasMFDerivAt.sub hg.hasMFDerivAt).mfderiv
 #align mfderiv_sub mfderiv_sub