feat: more consistent use of ext, and updating porting notes. (#5242)

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

Mathlib/Algebra/Category/GroupCat/Basic.lean

@@ -363,9 +363,7 @@ set_option linter.uppercaseLean3 false in
 -- the forgetful functor is representable.
 theorem injective_of_mono {G H : AddCommGroupCat.{0}} (f : G ⟶ H) [Mono f] : Function.Injective f :=
   fun g₁ g₂ h => by
-  have t0 : asHom g₁ ≫ f = asHom g₂ ≫ f := by
-    apply int_hom_ext
-    simpa using h
+  have t0 : asHom g₁ ≫ f = asHom g₂ ≫ f := by aesop_cat
   have t1 : asHom g₁ = asHom g₂ := (cancel_mono _).1 t0
   apply asHom_injective t1
 set_option linter.uppercaseLean3 false in

Mathlib/Algebra/Category/GroupCat/Colimits.lean

@@ -327,7 +327,7 @@ noncomputable def cokernelIsoQuotient {G H : AddCommGroupCat.{u}} (f : G ⟶ H)
     simp only [coequalizer_as_cokernel, cokernel.π_desc_assoc, Category.comp_id]
     rfl
   inv_hom_id := by
-    ext x : 2
+    ext x
     exact QuotientAddGroup.induction_on x <| cokernel.π_desc_apply f _ _
 #align AddCommGroup.cokernel_iso_quotient AddCommGroupCat.cokernelIsoQuotient
 

Mathlib/Algebra/Category/GroupCat/Limits.lean

@@ -431,6 +431,8 @@ def kernelIsoKer {G H : AddCommGroupCat.{u}} (f : G ⟶ H) :
     rintro ⟨x, (hx : f _ = 0)⟩
     exact hx
   hom_inv_id := by
+    -- Porting note: it would be nice to do the next two steps by a single `ext`,
+    -- but this will require thinking carefully about the relative priorities of `@[ext]` lemmas.
     refine equalizer.hom_ext ?_
     ext x
     dsimp

Mathlib/Algebra/Homology/ImageToKernel.lean

@@ -274,22 +274,18 @@ theorem imageSubobjectMap_comp_imageToKernel (p : α.right = β.left) :
 #align image_subobject_map_comp_image_to_kernel imageSubobjectMap_comp_imageToKernel
 
 variable [HasCokernel (imageToKernel f g w)] [HasCokernel (imageToKernel f' g' w')]
-
 variable [HasCokernel (imageToKernel f₁ g₁ w₁)]
-
 variable [HasCokernel (imageToKernel f₂ g₂ w₂)]
-
 variable [HasCokernel (imageToKernel f₃ g₃ w₃)]
 
 /-- Given compatible commutative squares between
 a pair `f g` and a pair `f' g'` satisfying `f ≫ g = 0` and `f' ≫ g' = 0`,
 we get a morphism on homology.
 -/
 def homology.map (p : α.right = β.left) : homology f g w ⟶ homology f' g' w' :=
-  cokernel.desc _ (kernelSubobjectMap β ≫ cokernel.π _)
-    (by
-      rw [imageSubobjectMap_comp_imageToKernel_assoc w w' α β p]
-      simp only [cokernel.condition, comp_zero])
+  cokernel.desc _ (kernelSubobjectMap β ≫ cokernel.π _) <| by
+    rw [imageSubobjectMap_comp_imageToKernel_assoc w w' α β p]
+    simp only [cokernel.condition, comp_zero]
 #align homology.map homology.map
 
 -- porting note: removed elementwise attribute which does not seem to be helpful here,
@@ -318,13 +314,15 @@ theorem homology.map_desc (p : α.right = β.left) {D : V} (k : (kernelSubobject
     (z : imageToKernel f' g' w' ≫ k = 0) :
     homology.map w w' α β p ≫ homology.desc f' g' w' k z =
       homology.desc f g w (kernelSubobjectMap β ≫ k)
-        (by simp only [imageSubobjectMap_comp_imageToKernel_assoc w w' α β p, z, comp_zero]) :=
-  by ext ; simp only [homology.π_desc, homology.π_map_assoc]
+        (by simp only [imageSubobjectMap_comp_imageToKernel_assoc w w' α β p, z, comp_zero]) := by
+  ext
+  simp only [homology.π_desc, homology.π_map_assoc]
 #align homology.map_desc homology.map_desc
 
 @[simp]
 theorem homology.map_id : homology.map w w (𝟙 _) (𝟙 _) rfl = 𝟙 _ := by
-  ext ; simp only [homology.π_map, kernelSubobjectMap_id, Category.id_comp, Category.comp_id]
+  ext
+  simp only [homology.π_map, kernelSubobjectMap_id, Category.id_comp, Category.comp_id]
 #align homology.map_id homology.map_id
 
 /-- Auxiliary lemma for homology computations. -/
@@ -340,7 +338,8 @@ theorem homology.comp_right_eq_comp_left {V : Type _} [Category V] {A₁ B₁ C
 theorem homology.map_comp (p₁ : α₁.right = β₁.left) (p₂ : α₂.right = β₂.left) :
     homology.map w₁ w₂ α₁ β₁ p₁ ≫ homology.map w₂ w₃ α₂ β₂ p₂ =
       homology.map w₁ w₃ (α₁ ≫ α₂) (β₁ ≫ β₂) (homology.comp_right_eq_comp_left p₁ p₂) := by
-  ext ; simp only [kernelSubobjectMap_comp, homology.π_map_assoc, homology.π_map, Category.assoc]
+  ext
+  simp only [kernelSubobjectMap_comp, homology.π_map_assoc, homology.π_map, Category.assoc]
 #align homology.map_comp homology.map_comp
 
 /-- An isomorphism between two three-term complexes induces an isomorphism on homology. -/
@@ -414,17 +413,16 @@ this variant provides a morphism
 which is sometimes more convenient.
 -/
 def imageToKernel' (w : f ≫ g = 0) : image f ⟶ kernel g :=
-  kernel.lift g (image.ι f)
-    (by
-      ext
-      simpa using w)
+  kernel.lift g (image.ι f) <| by
+    ext
+    simpa using w
 #align image_to_kernel' imageToKernel'
 
 @[simp]
 theorem imageSubobjectIso_imageToKernel' (w : f ≫ g = 0) :
     (imageSubobjectIso f).hom ≫ imageToKernel' f g w =
       imageToKernel f g w ≫ (kernelSubobjectIso g).hom := by
-  apply equalizer.hom_ext
+  ext
   simp [imageToKernel']
 #align image_subobject_iso_image_to_kernel' imageSubobjectIso_imageToKernel'
 
@@ -447,12 +445,15 @@ def homologyIsoCokernelImageToKernel' (w : f ≫ g = 0) :
   inv := cokernel.map _ _ (imageSubobjectIso f).inv (kernelSubobjectIso g).inv
       (by simp only [imageToKernel'_kernelSubobjectIso])
   hom_inv_id := by
+    -- Just calling `ext` here uses the higher priority `homology.ext`,
+    -- which precomposes with `homology.π`.
+    -- As we are trying to work in terms of `cokernel`, it is better to use `coequalizer.hom_ext`.
     apply coequalizer.hom_ext
     simp only [Iso.hom_inv_id_assoc, cokernel.π_desc, cokernel.π_desc_assoc, Category.assoc,
       coequalizer_as_cokernel]
     exact (Category.comp_id _).symm
   inv_hom_id := by
-    apply coequalizer.hom_ext
+    ext
     simp only [Iso.inv_hom_id_assoc, cokernel.π_desc, Category.comp_id, cokernel.π_desc_assoc,
       Category.assoc]
 #align homology_iso_cokernel_image_to_kernel' homologyIsoCokernelImageToKernel'
@@ -464,7 +465,7 @@ variable [HasEqualizers V]
 def homologyIsoCokernelLift (w : f ≫ g = 0) : homology f g w ≅ cokernel (kernel.lift g f w) := by
   refine' homologyIsoCokernelImageToKernel' f g w ≪≫ _
   have p : factorThruImage f ≫ imageToKernel' f g w = kernel.lift g f w := by
-    apply equalizer.hom_ext
+    ext
     simp [imageToKernel']
   exact (cokernelEpiComp _ _).symm ≪≫ cokernelIsoOfEq p
 #align homology_iso_cokernel_lift homologyIsoCokernelLift

Mathlib/Algebra/Homology/Opposite.lean

@@ -71,9 +71,7 @@ def homologyOp {X Y Z : V} (f : X ⟶ Y) (g : Y ⟶ Z) (w : f ≫ g = 0) :
     homology g.op f.op (by rw [← op_comp, w, op_zero]) ≅ Opposite.op (homology f g w) :=
   cokernelIsoOfEq (imageToKernel_op _ _ w) ≪≫ cokernelEpiComp _ _ ≪≫ cokernelCompIsIso _ _ ≪≫
     cokernelOpOp _ ≪≫ (homologyIsoKernelDesc _ _ _ ≪≫
-    kernelIsoOfEq (by
-    -- Porting note: broken ext
-      apply coequalizer.hom_ext; simp only [image.fac, cokernel.π_desc, cokernel.π_desc_assoc]) ≪≫
+    kernelIsoOfEq (by ext; simp only [image.fac, cokernel.π_desc, cokernel.π_desc_assoc]) ≪≫
     kernelCompMono _ (image.ι g)).op
 #align homology_op homologyOp
 
@@ -83,9 +81,7 @@ def homologyUnop {X Y Z : Vᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) (w : f ≫ g = 0)
     homology g.unop f.unop (by rw [← unop_comp, w, unop_zero]) ≅ Opposite.unop (homology f g w) :=
   cokernelIsoOfEq (imageToKernel_unop _ _ w) ≪≫ cokernelEpiComp _ _ ≪≫ cokernelCompIsIso _ _ ≪≫
     cokernelUnopUnop _ ≪≫ (homologyIsoKernelDesc _ _ _ ≪≫
-    kernelIsoOfEq (by
-    -- Porting note: broken ext
-      apply coequalizer.hom_ext; simp only [image.fac, cokernel.π_desc, cokernel.π_desc_assoc]) ≪≫
+    kernelIsoOfEq (by ext; simp only [image.fac, cokernel.π_desc, cokernel.π_desc_assoc]) ≪≫
     kernelCompMono _ (image.ι g)).unop
 #align homology_unop homologyUnop
 

Mathlib/Algebra/Homology/QuasiIso.lean

@@ -114,7 +114,7 @@ noncomputable def toSingle₀CokernelAtZeroIso : cokernel (X.d 1 0) ≅ Y :=
 theorem toSingle₀CokernelAtZeroIso_hom_eq [hf : QuasiIso f] :
     f.toSingle₀CokernelAtZeroIso.hom =
       cokernel.desc (X.d 1 0) (f.f 0) (by rw [← f.2 1 0 rfl]; exact comp_zero) := by
-  apply coequalizer.hom_ext
+  ext
   dsimp only [toSingle₀CokernelAtZeroIso, ChainComplex.homologyZeroIso, homologyOfZeroRight,
     homology.mapIso, ChainComplex.homologyFunctor0Single₀, cokernel.map]
   dsimp [asIso]
@@ -164,7 +164,7 @@ noncomputable def fromSingle₀KernelAtZeroIso [hf : QuasiIso f] : kernel (X.d 0
 theorem fromSingle₀KernelAtZeroIso_inv_eq [hf : QuasiIso f] :
     f.fromSingle₀KernelAtZeroIso.inv =
       kernel.lift (X.d 0 1) (f.f 0) (by rw [f.2 0 1 rfl]; exact zero_comp) := by
-  apply equalizer.hom_ext
+  ext
   dsimp only [fromSingle₀KernelAtZeroIso, CochainComplex.homologyZeroIso, homologyOfZeroLeft,
     homology.mapIso, CochainComplex.homologyFunctor0Single₀, kernel.map]
   simp only [Iso.trans_inv, Iso.app_inv, Iso.symm_inv, Category.assoc, equalizer_as_kernel,

Mathlib/AlgebraicGeometry/PresheafedSpace.lean

@@ -186,6 +186,10 @@ instance categoryOfPresheafedSpaces : Category (PresheafedSpace C) where
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.PresheafedSpace.category_of_PresheafedSpaces AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces
 
+variable {C}
+
+-- Porting note: adding an ext lemma.
+-- See https://github.com/leanprover-community/mathlib4/issues/5229
 @[ext]
 theorem ext {X Y : PresheafedSpace C} (α β : X ⟶ Y) (w : α.base = β.base)
     (h : α.c ≫ whiskerRight (eqToHom (by rw [w])) _ = β.c) : α = β :=

Mathlib/AlgebraicGeometry/PresheafedSpace/HasColimits.lean

@@ -167,8 +167,8 @@ def pushforwardDiagramToColimit (F : J ⥤ PresheafedSpace.{_, _, v} C) :
       (op ((Opens.map (F.map g).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj U.unop)))
       (op ((Opens.map (colimit.ι (F ⋙ PresheafedSpace.forget C) j₂)).obj (unop U)))
       _]
-    -- Now we show the open sets are equal.
     swap
+    -- Now we show the open sets are equal.
     · apply unop_injective
       rw [← Opens.map_comp_obj]
       congr
@@ -212,11 +212,12 @@ def colimitCocone (F : J ⥤ PresheafedSpace.{_, _, v} C) : Cocone F where
         { base := colimit.ι (F ⋙ PresheafedSpace.forget C) j
           c := limit.π _ (op j) }
       naturality := fun {j j'} f => by
-        fapply PresheafedSpace.ext
+        ext1
+        -- See https://github.com/leanprover/std4/pull/158
+        swap
         · ext x
           exact colimit.w_apply (F ⋙ PresheafedSpace.forget C) f x
-        · ext U
-          rcases U with ⟨U, hU⟩
+        · ext ⟨U, hU⟩
           dsimp
           rw [PresheafedSpace.id_c_app, map_id]
           erw [id_comp]
@@ -303,11 +304,12 @@ set_option linter.uppercaseLean3 false in
 
 theorem desc_fac (F : J ⥤ PresheafedSpace.{_, _, v} C) (s : Cocone F) (j : J) :
     (colimitCocone F).ι.app j ≫ desc F s = s.ι.app j := by
-  fapply PresheafedSpace.ext
+  ext U
+  -- See https://github.com/leanprover/std4/pull/158
+  swap
   · simp [desc]
   · -- Porting note : the original proof is just `ext; dsimp [desc, descCApp]; simpa`,
     -- but this has to be expanded a bit
-    ext U
     rw [NatTrans.comp_app, PresheafedSpace.comp_c_app, whiskerRight_app]
     dsimp [desc, descCApp]
     simp only [eqToHom_app, op_obj, Opens.map_comp_obj, eqToHom_map, Functor.leftOp, assoc]
@@ -331,14 +333,14 @@ def colimitCoconeIsColimit (F : J ⥤ PresheafedSpace.{_, _, v} C) :
     have t :
       m.base =
         colimit.desc (F ⋙ PresheafedSpace.forget C) ((PresheafedSpace.forget C).mapCocone s) := by
-      apply CategoryTheory.Limits.colimit.hom_ext
-      intro j
-      apply ContinuousMap.ext
-      intro x
+      dsimp
+      ext j
       rw [colimit.ι_desc, mapCocone_ι_app, ← w j]
       simp
-    fapply PresheafedSpace.ext
+    ext : 1
+    swap
     -- could `ext` please not reorder goals?
+    -- See https://github.com/leanprover/std4/pull/158
     · exact t
     · refine NatTrans.ext _ _ (funext fun U => limit_obj_ext fun j => ?_)
       dsimp only [colimitCocone_pt, colimit_carrier, leftOp_obj, pushforwardDiagramToColimit_obj,

Mathlib/AlgebraicGeometry/SheafedSpace.lean

@@ -90,6 +90,13 @@ instance : Category (SheafedSpace C) :=
   show Category (InducedCategory (PresheafedSpace C) SheafedSpace.toPresheafedSpace) by
     infer_instance
 
+-- Porting note: adding an ext lemma.
+-- See https://github.com/leanprover-community/mathlib4/issues/5229
+@[ext]
+theorem ext {X Y : SheafedSpace C} (α β : X ⟶ Y) (w : α.base = β.base)
+    (h : α.c ≫ whiskerRight (eqToHom (by rw [w])) _ = β.c) : α = β :=
+  PresheafedSpace.ext α β w h
+
 /-- Forgetting the sheaf condition is a functor from `SheafedSpace C` to `PresheafedSpace C`. -/
 def forgetToPresheafedSpace : SheafedSpace C ⥤ PresheafedSpace C :=
   inducedFunctor _

Mathlib/AlgebraicGeometry/Spec.lean

@@ -189,13 +189,16 @@ theorem Spec.basicOpen_hom_ext {X : RingedSpace.{u}} {R : CommRingCat.{u}}
       (toOpen R U ≫ α.c.app (op U)) ≫ X.presheaf.map (eqToHom (by rw [w])) =
         toOpen R U ≫ β.c.app (op U)) :
     α = β := by
-  refine PresheafedSpace.ext (α := α) (β := β) w ?_
+  ext : 1
+  -- See https://github.com/leanprover/std4/pull/158
+  swap
+  · exact w
   · apply
       ((TopCat.Sheaf.pushforward β.base).obj X.sheaf).hom_ext _ PrimeSpectrum.isBasis_basic_opens
     intro r
     apply (StructureSheaf.to_basicOpen_epi R r).1
-    specialize h r
     -- Porting note : was a one-liner `simpa using h r`
+    specialize h r
     simp only [sheafedSpaceObj_carrier, Functor.op_obj, unop_op, TopCat.Presheaf.pushforwardObj_obj,
       sheafedSpaceObj_presheaf, Category.assoc] at h
     rw [NatTrans.comp_app, ←h]

Mathlib/AlgebraicGeometry/Stalks.lean

@@ -104,6 +104,7 @@ set_option linter.uppercaseLean3 false in
 theorem restrictStalkIso_inv_eq_ofRestrict {U : TopCat} (X : PresheafedSpace.{_, _, v} C)
     {f : U ⟶ (X : TopCat.{v})} (h : OpenEmbedding f) (x : U) :
     (X.restrictStalkIso h x).inv = stalkMap (X.ofRestrict h) x := by
+  -- We can't use `ext` here due to https://github.com/leanprover/std4/pull/159
   refine colimit.hom_ext fun V => ?_
   induction V with | h V => ?_
   let i : (h.isOpenMap.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V :=
@@ -147,6 +148,7 @@ theorem comp {X Y Z : PresheafedSpace.{_, _, v} C} (α : X ⟶ Y) (β : Y ⟶ Z)
       (stalkMap β (α.base x) : Z.stalk (β.base (α.base x)) ⟶ Y.stalk (α.base x)) ≫
         (stalkMap α x : Y.stalk (α.base x) ⟶ X.stalk x) := by
   dsimp [stalkMap, stalkFunctor, stalkPushforward]
+  -- We can't use `ext` here due to https://github.com/leanprover/std4/pull/159
   refine colimit.hom_ext fun U => ?_
   induction U with | h U => ?_
   cases U
@@ -165,8 +167,10 @@ either side of the equality.
 theorem congr {X Y : PresheafedSpace.{_, _, v} C} (α β : X ⟶ Y)
     (h₁ : α = β) (x x' : X) (h₂ : x = x') :
     stalkMap α x ≫ eqToHom (show X.stalk x = X.stalk x' by rw [h₂]) =
-      eqToHom (show Y.stalk (α.base x) = Y.stalk (β.base x') by rw [h₁, h₂]) ≫ stalkMap β x' :=
-  stalk_hom_ext _ fun U hx => by subst h₁; subst h₂; simp
+      eqToHom (show Y.stalk (α.base x) = Y.stalk (β.base x') by rw [h₁, h₂]) ≫ stalkMap β x' := by
+  ext
+  substs h₁ h₂
+  simp
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.PresheafedSpace.stalk_map.congr AlgebraicGeometry.PresheafedSpace.stalkMap.congr
 
@@ -225,6 +229,7 @@ theorem stalkSpecializes_stalkMap {X Y : PresheafedSpace.{_, _, v} C}
   -- Porting note : the original one liner `dsimp [stalkMap]; simp [stalkMap]` doesn't work,
   -- I had to uglify this
   dsimp [stalkSpecializes, stalkMap, stalkFunctor, stalkPushforward]
+  -- We can't use `ext` here due to https://github.com/leanprover/std4/pull/159
   refine colimit.hom_ext fun j => ?_
   induction j with | h j => ?_
   dsimp

Mathlib/AlgebraicGeometry/StructureSheaf.lean

@@ -577,6 +577,10 @@ def stalkIso (x : PrimeSpectrum.Top R) :
   hom := stalkToFiberRingHom R x
   inv := localizationToStalk R x
   hom_inv_id :=
+    -- Porting note: We should be able to replace the next two lines with `ext U hxU s`,
+    -- but there seems to be a bug in `ext` whereby
+    -- it will not do multiple introductions for a single lemma, if you name the arguments.
+    -- See https://github.com/leanprover/std4/pull/159
     (structureSheaf R).presheaf.stalk_hom_ext fun U hxU => by
       ext s
       simp only [FunctorToTypes.map_comp_apply, CommRingCat.forget_map,

Mathlib/AlgebraicTopology/SplitSimplicialObject.lean

@@ -215,9 +215,7 @@ def summand (A : IndexSet Δ) : C :=
 variable [HasFiniteCoproducts C]
 
 /-- The coproduct of the family `summand N Δ` -/
-@[simp]
-def coprod :=
-  ∐ summand N Δ
+abbrev coprod := ∐ summand N Δ
 #align simplicial_object.splitting.coprod SimplicialObject.Splitting.coprod
 
 variable {Δ}
@@ -301,8 +299,7 @@ theorem ιSummand_comp_app (f : X ⟶ Y) {Δ : SimplexCategoryᵒᵖ} (A : Index
 theorem hom_ext' {Z : C} {Δ : SimplexCategoryᵒᵖ} (f g : X.obj Δ ⟶ Z)
     (h : ∀ A : IndexSet Δ, s.ιSummand A ≫ f = s.ιSummand A ≫ g) : f = g := by
   rw [← cancel_epi (s.iso Δ).hom]
-  apply colimit.hom_ext
-  rintro ⟨A⟩
+  ext A
   simpa only [ιSummand_eq, iso_hom, map, colimit.ι_desc_assoc, Cofan.mk_ι_app] using h A
 #align simplicial_object.splitting.hom_ext' SimplicialObject.Splitting.hom_ext'
 
@@ -338,7 +335,7 @@ def ofIso (e : X ≅ Y) : Splitting Y where
   ι n := s.ι n ≫ e.hom.app (op [n])
   map_isIso Δ := by
     convert (inferInstance : IsIso ((s.iso Δ).hom ≫ e.hom.app Δ))
-    apply colimit.hom_ext
+    ext
     simp [map]
 #align simplicial_object.splitting.of_iso SimplicialObject.Splitting.ofIso