chore: cleanup of some ext porting notes (#5176)

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>

Author: kim-em

Mathlib/Algebra/ContinuedFractions/Basic.lean

@@ -112,13 +112,15 @@ We store the sequence of partial numerators and denominators in a sequence of
 `GeneralizedContinuedFraction.Pair`s `s`.
 For convenience, one often writes `[h; (a₀, b₀), (a₁, b₁), (a₂, b₂),...]`.
 -/
-@[ext] -- Porting note: added to replace the manually written ext lemmas
+@[ext]
 structure GeneralizedContinuedFraction where
   /-- Head term -/
   h : α
   /-- Sequence of partial numerator and denominator pairs. -/
   s : Stream'.Seq <| Pair α
 #align generalized_continued_fraction GeneralizedContinuedFraction
+#align generalized_continued_fraction.ext_iff GeneralizedContinuedFraction.ext_iff
+#align generalized_continued_fraction.ext GeneralizedContinuedFraction.ext
 
 variable {α}
 
@@ -403,8 +405,3 @@ def convergents' (g : GeneralizedContinuedFraction K) (n : ℕ) : K :=
 #align generalized_continued_fraction.convergents' GeneralizedContinuedFraction.convergents'
 
 end GeneralizedContinuedFraction
-
--- Porting note: The `ext`-lemmas that were here can be autogenerated by
--- the `@[ext]` attribute on `GeneralizedContinuedFraction`.
-#align generalized_continued_fraction.ext_iff GeneralizedContinuedFraction.ext_iff
-#align generalized_continued_fraction.ext GeneralizedContinuedFraction.ext

Mathlib/Algebra/DirectSum/Basic.lean

@@ -38,6 +38,7 @@ Note: `open DirectSum` will enable the notation `⨁ i, β i` for `DirectSum β`
 def DirectSum [∀ i, AddCommMonoid (β i)] : Type _ :=
   -- Porting note: Failed to synthesize
   -- Π₀ i, β i deriving AddCommMonoid, Inhabited
+  -- See https://github.com/leanprover-community/mathlib4/issues/5020
   Π₀ i, β i
 #align direct_sum DirectSum
 
@@ -209,7 +210,7 @@ theorem toAddMonoid_of (i) (x : β i) : toAddMonoid φ (of β i x) = φ i x :=
 
 theorem toAddMonoid.unique (f : ⨁ i, β i) : ψ f = toAddMonoid (fun i => ψ.comp (of β i)) f := by
   congr
-  -- Porting note: ext applied unsuitable ext lemma
+  -- Porting note: ext applies addHom_ext' here, which isn't what we want.
   apply Dfinsupp.addHom_ext'
   simp [toAddMonoid, of]
 #align direct_sum.to_add_monoid.unique DirectSum.toAddMonoid.unique

Mathlib/Algebra/DirectSum/Ring.lean

@@ -254,10 +254,7 @@ private theorem mul_assoc (a b c : ⨁ i, A i) : a * b * c = a * (b * c) := by
       simp only [coe_comp, Function.comp_apply, AddMonoidHom.compHom_apply_apply, aux, flip_apply,
         AddMonoidHom.flipHom_apply] at sol
       exact sol
-  -- Porting note: Next three lines used to be a single `ext` which does not work anymore
-  refine DirectSum.addHom_ext' (fun ai ↦ AddMonoidHom.ext (fun ax ↦ ?_))
-  refine DirectSum.addHom_ext' (fun bi ↦ AddMonoidHom.ext (fun bx ↦ ?_))
-  refine DirectSum.addHom_ext' (fun ci ↦ AddMonoidHom.ext (fun cx ↦ ?_))
+  ext ai ax bi bx ci cx
   dsimp only [coe_comp, Function.comp_apply, AddMonoidHom.compHom_apply_apply, flip_apply,
     AddMonoidHom.flipHom_apply]
   simp_rw [mulHom_of_of]

Mathlib/Algebra/Free.lean

@@ -119,8 +119,7 @@ def lift : (α → β) ≃ (FreeMagma α →ₙ* β) where
     map_mul' := fun x y ↦ rfl }
   invFun F := F ∘ of
   left_inv f := by rfl
--- Porting note: replaced ext by FreeMagma.hom_ext
-  right_inv F := FreeMagma.hom_ext (rfl)
+  right_inv F := by ext; rfl
 #align free_magma.lift FreeMagma.lift
 
 @[to_additive (attr := simp)]
@@ -468,7 +467,7 @@ variable {α : Type u}
 @[to_additive]
 instance : Semigroup (FreeSemigroup α) where
   mul L1 L2 := ⟨L1.1, L1.2 ++ L2.1 :: L2.2⟩
--- Porting note: replaced ext by FreeSemigroup.ext
+  -- Porting note: replaced ext by FreeSemigroup.ext
   mul_assoc _L1 _L2 _L3 := FreeSemigroup.ext _ _ rfl <| List.append_assoc _ _ _
 
 @[to_additive (attr := simp)]

Mathlib/Algebra/FreeMonoid/Basic.lean

@@ -269,9 +269,9 @@ theorem lift_restrict (f : FreeMonoid α →* M) : lift (f ∘ of) = f := lift.a
 #align free_add_monoid.lift_restrict FreeAddMonoid.lift_restrict
 
 @[to_additive]
-theorem comp_lift (g : M →* N) (f : α → M) : g.comp (lift f) = lift (g ∘ f) :=
-  -- Porting note: replace ext by FreeMonoid.hom_eq
-  FreeMonoid.hom_eq (by simp)
+theorem comp_lift (g : M →* N) (f : α → M) : g.comp (lift f) = lift (g ∘ f) := by
+  ext
+  simp
 #align free_monoid.comp_lift FreeMonoid.comp_lift
 #align free_add_monoid.comp_lift FreeAddMonoid.comp_lift
 

Mathlib/Data/Bitvec/Lemmas.lean

@@ -127,7 +127,7 @@ theorem decide_addLsb_mod_two {x b} : decide (addLsb x b % 2 = 1) = b := by
 
 theorem ofNat_toNat {n : ℕ} (v : Bitvec n) : Bitvec.ofNat n v.toNat = v := by
   cases' v with xs h
-  -- Porting note: was `ext1`
+  -- Porting note: was `ext1`, but that now applies `Vector.ext` rather than `Subtype.ext`.
   apply Subtype.ext
   change Vector.toList _ = xs
   dsimp [Bitvec.toNat, bitsToNat]

Mathlib/Data/Dfinsupp/Multiset.lean

@@ -83,18 +83,7 @@ theorem toDfinsupp_singleton (a : α) : toDfinsupp {a} = Dfinsupp.single a 1 :=
 /-- `Multiset.toDfinsupp` as an `AddEquiv`. -/
 @[simps! apply symm_apply]
 def equivDfinsupp : Multiset α ≃+ Π₀ _ : α, ℕ :=
-  AddMonoidHom.toAddEquiv Multiset.toDfinsupp Dfinsupp.toMultiset
-    (by
-      -- Porting note: used to be ext.
-      /- potential bug: in lean 3, `trace.ext` outputs
-         "matched goal to rule: dfinsupp.add_hom_ext'"
-         but that lemma does not apply!-/
-      apply Multiset.addHom_ext
-      simp)
-    (by
-      -- Porting note: used to be ext
-      apply Dfinsupp.addHom_ext
-      simp)
+  AddMonoidHom.toAddEquiv Multiset.toDfinsupp Dfinsupp.toMultiset (by ext; simp) (by ext; simp)
 #align multiset.equiv_dfinsupp Multiset.equivDfinsupp
 
 @[simp]

Mathlib/Data/Finsupp/Basic.lean

@@ -628,16 +628,10 @@ def mapDomainEmbedding {α β : Type _} (f : α ↪ β) : (α →₀ ℕ) ↪ β
 theorem mapDomain.addMonoidHom_comp_mapRange [AddCommMonoid N] (f : α → β) (g : M →+ N) :
     (mapDomain.addMonoidHom f).comp (mapRange.addMonoidHom g) =
       (mapRange.addMonoidHom g).comp (mapDomain.addMonoidHom f) := by
-  apply Finsupp.addHom_ext'
-  intro x
-  apply AddMonoidHom.ext
-  intro x_1
-  apply Finsupp.ext
-  intro a
+  ext
   simp only [AddMonoidHom.coe_comp, Finsupp.mapRange_single, Finsupp.mapDomain.addMonoidHom_apply,
     Finsupp.singleAddHom_apply, eq_self_iff_true, Function.comp_apply, Finsupp.mapDomain_single,
     Finsupp.mapRange.addMonoidHom_apply]
-  -- porting note: this is ugly, just expanded the Lean 3 proof; `ext` didn't work in the same way
 #align finsupp.map_domain.add_monoid_hom_comp_map_range Finsupp.mapDomain.addMonoidHom_comp_mapRange
 
 /-- When `g` preserves addition, `mapRange` and `mapDomain` commute. -/