feat : add ext lemma for Type u (#3593)

This lemma, which was not needed in mathlib3, simplifies several proofs (back to the state they were in in mathlib3). Note on what's going on here: Lean 3 `ext` would fall back on "try all ext lemmas" if it failed, and thus it could see through lots of definitional equalities. Lean 4 `ext` doesn't do this (because it's inefficient) and so we need to add more `ext` lemmas in order to recover Lean 3 functionality.
leanprover-community · Apr 22, 2023 · 68f5770 · 68f5770
1 parent 0b676a2
commit 68f5770
Show file tree

Hide file tree

Showing 6 changed files with 12 additions and 14 deletions.
diff --git a/Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean b/Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean
@@ -59,11 +59,9 @@ instance unit_isIso_of_L_fully_faithful [Full L] [Faithful L] : IsIso (Adjunctio
             aesop_cat },
           ⟨by
             ext x
-            funext f
             apply L.map_injective
             aesop_cat, by
             ext x
-            funext f
             dsimp
             simp only [Adjunction.homEquiv_counit, preimage_comp, preimage_map, Category.assoc]
             rw [← h.unit_naturality]
@@ -85,11 +83,9 @@ instance counit_isIso_of_R_fully_faithful [Full R] [Faithful R] : IsIso (Adjunct
               aesop_cat },
             ⟨by
               ext x
-              funext f
               apply R.map_injective
               simp, by
               ext x
-              funext f
               dsimp
               simp only [Adjunction.homEquiv_unit, preimage_comp, preimage_map]
               rw [← h.counit_naturality]

diff --git a/Mathlib/CategoryTheory/Elements.lean b/Mathlib/CategoryTheory/Elements.lean
@@ -200,8 +200,7 @@ def toCostructuredArrow (F : Cᵒᵖ ⥤ Type v) : F.Elementsᵒᵖ ⥤ Costruct
   map f := by
     fapply CostructuredArrow.homMk
     · exact f.unop.val.unop
-    · ext Z
-      funext y
+    · ext Z y
       dsimp
       simp only [FunctorToTypes.map_comp_apply, ← f.unop.2]
 #align category_theory.category_of_elements.to_costructured_arrow CategoryTheory.CategoryOfElements.toCostructuredArrow
@@ -256,8 +255,7 @@ theorem to_fromCostructuredArrow_eq (F : Cᵒᵖ ⥤ Type v) :
     simp only [Functor.id_obj, Functor.rightOp_obj, toCostructuredArrow_obj, Functor.comp_obj,
       CostructuredArrow.mk]
     congr
-    ext x
-    funext f
+    ext x f
     convert congr_fun (X_hom.naturality f.op).symm (𝟙 X_left)
     simp
   · intro X Y f
@@ -285,8 +283,7 @@ theorem costructuredArrow_yoneda_equivalence_naturality {F₁ F₂ : Cᵒᵖ ⥤
     simp only [CostructuredArrow.map_mk, toCostructuredArrow_obj, Functor.op_obj,
       Functor.comp_obj]
     congr
-    ext
-    funext f
+    ext _ f
     simpa using congr_fun (α.naturality f.op).symm (unop X).snd
   · intro X Y f
     ext

diff --git a/Mathlib/CategoryTheory/Sites/SheafOfTypes.lean b/Mathlib/CategoryTheory/Sites/SheafOfTypes.lean
@@ -511,7 +511,6 @@ theorem extension_iff_amalgamation {P : Cᵒᵖ ⥤ Type v₁} (x : S.functor
     convert h f hf
     rw [yonedaEquiv_naturality]
     simp [yonedaEquiv]
-    rfl
 #align category_theory.presieve.extension_iff_amalgamation CategoryTheory.Presieve.extension_iff_amalgamation
 
 /-- The yoneda version of the sheaf condition is equivalent to the sheaf condition.

diff --git a/Mathlib/CategoryTheory/Sites/Sieves.lean b/Mathlib/CategoryTheory/Sites/Sieves.lean
@@ -778,8 +778,7 @@ theorem natTransOfLe_comm {S T : Sieve X} (h : S ≤ T) :
 /-- The presheaf induced by a sieve is a subobject of the yoneda embedding. -/
 instance functorInclusion_is_mono : Mono S.functorInclusion :=
   ⟨fun f g h => by
-    ext Y
-    funext y
+    ext Y y
     simpa [Subtype.ext_iff_val] using congr_fun (NatTrans.congr_app h Y) y⟩
 #align category_theory.sieve.functor_inclusion_is_mono CategoryTheory.Sieve.functorInclusion_is_mono
 

diff --git a/Mathlib/CategoryTheory/Types.lean b/Mathlib/CategoryTheory/Types.lean
@@ -55,6 +55,13 @@ theorem types_hom {α β : Type u} : (α ⟶ β) = (α → β) :=
   rfl
 #align category_theory.types_hom CategoryTheory.types_hom
 
+-- porting note: this lemma was not here in Lean 3. Lean 3 `ext` would solve this goal
+-- because of its "if all else fails, apply all `ext` lemmas" policy,
+-- which apparently we want to move away from.
+@[ext] theorem types_ext {α β : Type u} (f g : α ⟶ β) (h : ∀ a : α, f a = g a) : f = g := by
+  funext x
+  exact h x
+
 theorem types_id (X : Type u) : 𝟙 X = id :=
   rfl
 #align category_theory.types_id CategoryTheory.types_id

diff --git a/Mathlib/CategoryTheory/Yoneda.lean b/Mathlib/CategoryTheory/Yoneda.lean
@@ -50,7 +50,7 @@ def yoneda : C ⥤ Cᵒᵖ ⥤ Type v₁
     { app := fun Y g => g ≫ f
       naturality := fun Y Y' g => by funext Z; aesop_cat }
   map_id := by aesop_cat
-  map_comp := fun f g => by ext Y; dsimp; funext f; simp
+  map_comp := fun f g => by ext Y; dsimp; rw [Category.assoc];
 #align category_theory.yoneda CategoryTheory.yoneda
 
 /-- The co-Yoneda embedding, as a functor from `Cᵒᵖ` into co-presheaves on `C`.