Bump Poly to v4.34.1 + some proof insertions

.gitignore

@@ -40,6 +40,7 @@ docs/_includes/sorries.md
 *.synctex.gz(busy)
 *.pdfsync
 *.json
+!vendor/checkdecls/lake-manifest.json
 *.auctex-auto
 
 build/

Poly/Bifunctor/Basic.lean

@@ -39,8 +39,11 @@ theorem comp₂_comp {𝒞' : Type*} [Category 𝒞']
 def comp₂_iso {F₁ F₂ : 𝒟' ⥤ 𝒟} {P₁ P₂ : 𝒞 ⥤ 𝒟 ⥤ ℰ}
     (i : F₁ ≅ F₂) (j : P₁ ≅ P₂) : F₁ ⋙₂ P₁ ≅ F₂ ⋙₂ P₂ :=
   NatIso.ofComponents₂ (fun C D => (j.app C).app (F₁.obj D) ≪≫ (P₂.obj C).mapIso (i.app D))
-    (fun _ _ => by simp [NatTrans.naturality_app_assoc])
+    (fun _ _ => by
+      dsimp [comp₂]
+      simp [NatTrans.naturality_app_assoc])
     (fun C f => by
+      dsimp [comp₂]
       have := congr_arg (P₂.obj C).map (i.hom.naturality f)
       simp only [map_comp] at this
       simp [this])
@@ -70,12 +73,12 @@ theorem comp₂_naturality₂_left (F : 𝒟 ⥤ 𝒞) (P : 𝒞ᵒᵖ ⥤ 𝒟
     (i : F ⋙₂ coyoneda (C := 𝒞) ⟶ P) (X Y : 𝒞) (Z : 𝒟) (f : X ⟶ Y) (g : Y ⟶ F.obj Z) :
     -- The `op`s really are a pain. Why can't they be definitional like in Lean 3 :(
     (i.app <| .op X).app Z (f ≫ g) = (P.map f.op).app Z ((i.app <| .op Y).app Z g) := by
-  simp [← FunctorToTypes.naturality₂_left]
+  exact FunctorToTypes.naturality₂_left _ _ i f.op g
 
 theorem comp₂_naturality₂_right (F : 𝒟 ⥤ 𝒞) (P : 𝒞ᵒᵖ ⥤ 𝒟 ⥤ Type v)
     (i : F ⋙₂ coyoneda (C := 𝒞) ⟶ P) (X : 𝒞) (Y Z : 𝒟) (f : X ⟶ F.obj Y) (g : Y ⟶ Z) :
     (i.app <| .op X).app Z (f ≫ F.map g) = (P.obj <| .op X).map g ((i.app <| .op X).app Y f) := by
-  simp [← FunctorToTypes.naturality₂_right]
+  exact FunctorToTypes.naturality₂_right _ _ i g f
 
 end coyoneda
 
@@ -87,8 +90,14 @@ variable {𝒟 : Type*} [Category 𝒟]
 def coyoneda_iso {F : 𝒞 ⥤ 𝒟} {G : 𝒟 ⥤ 𝒞} (A : F ⊣ G) :
     F.op ⋙ coyoneda (C := 𝒟) ≅ G ⋙₂ coyoneda (C := 𝒞) :=
   NatIso.ofComponents₂ (fun C D => Equiv.toIso <| A.homEquiv C.unop D)
-    (fun _ _ => by ext : 1; simp [A.homEquiv_naturality_left])
-    (fun _ _ => by ext : 1; simp [A.homEquiv_naturality_right])
+    (fun _ f => by
+      apply ConcreteCategory.hom_ext
+      intro g
+      exact A.homEquiv_naturality_left f.unop g)
+    (fun _ f => by
+      apply ConcreteCategory.hom_ext
+      intro g
+      exact A.homEquiv_naturality_right g f)
 
 end Adjunction
 end CategoryTheory

Poly/Bifunctor/Sigma.lean

@@ -45,20 +45,22 @@ a functor `F'` s.t. `F'.Elements ≅ F.Elements × 𝒟`; very awkward.
 - known concrete instances are `𝒟 ∈ {Type, Cat, Grpd}` -/
 def Sigma {F : 𝒞 ⥤ Type w} (G : F.Elements ⥤ 𝒟 ⥤ Type v) : 𝒞 ⥤ 𝒟 ⥤ Type (max w v) := by
   refine curry.obj {
-    obj := fun (C, D) => (a : F.obj C) × (G.obj ⟨C, a⟩).obj D
-    map := fun (f, g) ⟨a, b⟩ =>
-      ⟨F.map f a, (G.map ⟨f, rfl⟩).app _ ((G.obj ⟨_, a⟩).map g b)⟩
+    obj := fun (C, D) => (a : F.obj C) × (G.obj (F.elementsMk C a)).obj D
+    map := fun fg => TypeCat.ofHom fun ⟨a, b⟩ =>
+      ⟨F.map fg.1 a, (G.map ⟨fg.1, rfl⟩).app _ ((G.obj (F.elementsMk _ a)).map fg.2 b)⟩
     map_id := ?_
     map_comp := ?_
   } <;> {
     intros
-    ext ⟨a, b⟩ : 1
-    dsimp
+    apply ConcreteCategory.hom_ext
+    rintro ⟨a, b⟩
+    dsimp +instances
     congr! 1 with h
     . simp
-    . rw! [h]; simp [FunctorToTypes.naturality]
+    . rw! [h]; simp [NatTrans.naturality_apply]
   }
 
+set_option backward.isDefEq.respectTransparency.types false in
 def Sigma.isoCongrLeft {F₁ F₂ : 𝒞 ⥤ Type w}
     /- Q: What kind of map `F₂.Elements ⥤ F₁.Elements`
     could `NatTrans.mapElements i.hom` generalize to?
@@ -69,38 +71,42 @@ def Sigma.isoCongrLeft {F₁ F₂ : 𝒞 ⥤ Type w}
   refine NatIso.ofComponents₂
     (fun C D => Equiv.toIso {
       toFun := fun ⟨a, b⟩ => ⟨i.hom.app C a, b⟩
-      invFun := fun ⟨a, b⟩ => ⟨i.inv.app C a, cast (by simp) b⟩
-      left_inv := fun ⟨_, _⟩ => by simp
-      right_inv := fun ⟨_, _⟩ => by simp
+      invFun := fun ⟨a, b⟩ => ⟨i.inv.app C a, cast (by simp [NatTrans.mapElements]) b⟩
+      left_inv := fun ⟨_, _⟩ => by simp [Sigma, NatTrans.mapElements]
+      right_inv := fun ⟨_, _⟩ => by simp [Sigma]
     }) ?_ ?_ <;> {
       intros
-      ext : 1
-      dsimp
+      apply ConcreteCategory.hom_ext
+      rintro ⟨a, b⟩
+      dsimp +instances [Sigma, Equiv.toIso]
       apply have h := ?_; Sigma.ext h ?_
-      . simp [FunctorToTypes.naturality]
-      . dsimp [Sigma] at h ⊢
+      . simp [NatTrans.naturality_apply]
+      . dsimp +instances [Sigma] at h ⊢
         rw! [← h]
         simp [NatTrans.mapElements]
     }
 
+set_option backward.isDefEq.respectTransparency.types false in
 def Sigma.isoCongrRight {F : 𝒞 ⥤ Type w} {G₁ G₂ : F.Elements ⥤ 𝒟 ⥤ Type v} (i : G₁ ≅ G₂) :
     Sigma G₁ ≅ Sigma G₂ := by
   refine NatIso.ofComponents₂
     (fun C D => Equiv.toIso {
-      toFun := fun ⟨a, b⟩ => ⟨a, (i.hom.app ⟨C, a⟩).app D b⟩
-      invFun := fun ⟨a, b⟩ => ⟨a, (i.inv.app ⟨C, a⟩).app D b⟩
-      left_inv := fun ⟨_, _⟩ => by simp
-      right_inv := fun ⟨_, _⟩ => by simp
+      toFun := fun ⟨a, b⟩ => ⟨a, (i.hom.app (F.elementsMk C a)).app D b⟩
+      invFun := fun ⟨a, b⟩ => ⟨a, (i.inv.app (F.elementsMk C a)).app D b⟩
+      left_inv := fun ⟨_, _⟩ => by simp [Sigma]
+      right_inv := fun ⟨_, _⟩ => by simp [Sigma]
     }) ?_ ?_ <;> {
       intros
-      ext : 1
-      dsimp
+      apply ConcreteCategory.hom_ext
+      rintro ⟨a, b⟩
+      dsimp +instances [Sigma, Equiv.toIso]
       apply have h := ?_; Sigma.ext h ?_
       . simp
-      . dsimp [Sigma] at h ⊢
-        simp [FunctorToTypes.naturality₂_left, FunctorToTypes.naturality₂_right]
+      . dsimp +instances [Sigma] at h ⊢
+        simp [FunctorToTypes.naturality₂_left]
     }
 
+set_option backward.isDefEq.respectTransparency false in
 theorem comp₂_Sigma {𝒟' : Type*} [Category 𝒟']
     {F : 𝒞 ⥤ Type w} (G : 𝒟' ⥤ 𝒟) (P : F.Elements ⥤ 𝒟 ⥤ Type v) :
     G ⋙₂ Sigma P = Sigma (G ⋙₂ P) := by
@@ -110,12 +116,15 @@ theorem comp₂_Sigma {𝒟' : Type*} [Category 𝒟']
     . intro; simp
     . intros
       apply heq_of_eq
-      ext : 1
-      apply Sigma.ext <;> simp
+      apply ConcreteCategory.hom_ext
+      intro x
+      apply Sigma.ext <;> simp [comp₂, Sigma]
   . intros
     apply heq_of_eq
-    ext : 3
-    apply Sigma.ext <;> simp
+    ext D : 2
+    apply ConcreteCategory.hom_ext
+    intro x
+    apply Sigma.ext <;> simp [comp₂, Sigma]
 
 end CategoryTheory.Functor
 
@@ -133,41 +142,60 @@ def equiv_Sigma {A : 𝒞} (X : 𝒞) (U : Over A) : (X ⟶ U.left) ≃ (b : X 
   invFun p := p.snd.left
   left_inv _ := by simp
   right_inv := fun _ => by
-    dsimp; congr! 1 with h
+    dsimp +instances; congr! 1 with h
     . simp
     . rw! [h]; simp
 
 @[simps]
 def equivalence_Elements (A : 𝒞) : (yoneda.obj A).Elements ≌ (Over A)ᵒᵖ where
   functor := {
-    obj := fun x => .op <| Over.mk x.snd
-    map := fun f => .op <| Over.homMk f.val.unop (by simpa using f.property)
+    obj := fun x => .op <| Over.mk x.val
+    map := fun f => .op <| Over.homMk f.hom.unop (by simpa using f.map_val)
   }
   inverse := {
-    obj := fun U => ⟨.op U.unop.left, U.unop.hom⟩
+    obj := fun U => (yoneda.obj A).elementsMk (.op U.unop.left) U.unop.hom
     map := fun f => ⟨.op f.unop.left, by simp⟩
   }
-  unitIso := NatIso.ofComponents Iso.refl (by simp)
+  unitIso := NatIso.ofComponents Iso.refl (by intro X Y f; simp; rfl)
   counitIso := NatIso.ofComponents Iso.refl
     -- TODO: `simp` fails to unify `id_comp`/`comp_id`
     (fun f => by simp [Category.comp_id f, Category.id_comp f])
 
+set_option backward.isDefEq.respectTransparency.types false in
 /-- For `X ∈ 𝒞` and `f ∈ 𝒞/A`, `𝒞(X, Over.forget f) ≅ Σ(g: X ⟶ A), 𝒞/A(g, f)`. -/
 def forget_iso_Sigma (A : 𝒞) :
     Over.forget A ⋙₂ coyoneda (C := 𝒞) ≅
     Functor.Sigma ((equivalence_Elements A).functor ⋙ coyoneda (C := Over A)) := by
   refine NatIso.ofComponents₂ (fun X U => Equiv.toIso <| equiv_Sigma X.unop U) ?_ ?_
   . intros X Y U f
-    ext : 1
-    dsimp
+    apply ConcreteCategory.hom_ext
+    intro g
+    change X.unop ⟶ U.left at g
+    dsimp +instances [Functor.comp₂, Functor.Sigma]
+    simp only [Equiv.toIso_hom_hom_apply]
+    change (⟨(f.unop ≫ g) ≫ U.hom, Over.homMk (f.unop ≫ g) rfl⟩ :
+      (b : Y.unop ⟶ A) × (Over.mk b ⟶ U)) =
+      ⟨f.unop ≫ (g ≫ U.hom),
+        (Over.homMk f.unop rfl :
+          Over.mk (f.unop ≫ (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom)) ≫
+        Over.homMk g rfl ≫ 𝟙 U⟩
     apply have h := ?_; Sigma.ext h ?_
     . simp
     . dsimp at h ⊢
       rw! [h]
       simp
   . intros X Y U f
-    ext : 1
-    dsimp
+    apply ConcreteCategory.hom_ext
+    intro g
+    change U.unop ⟶ X.left at g
+    dsimp +instances [Functor.comp₂, Functor.Sigma]
+    simp only [Equiv.toIso_hom_hom_apply]
+    change (⟨(g ≫ f.left) ≫ Y.hom, Over.homMk (g ≫ f.left) rfl⟩ :
+      (b : U.unop ⟶ A) × (Over.mk b ⟶ Y)) =
+      ⟨𝟙 U.unop ≫ (g ≫ X.hom),
+        (Over.homMk (𝟙 U.unop) rfl :
+          Over.mk (𝟙 U.unop ≫ (g ≫ X.hom)) ⟶ Over.mk (g ≫ X.hom)) ≫
+        Over.homMk g rfl ≫ f⟩
     apply have h := ?_; Sigma.ext h ?_
     . simp
     . dsimp at h ⊢