awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan.{u_4, v, u} Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst_1 : ∀ (i : ι), HasPullback (f i) v
inst_2 : HasPullback u v
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
c : Cofan P :=
  Cofan.mk (pullback u v) fun (p : ι × ι') ↦ pullback.lift (q₁ p.1 p.2 ≫ a.inj p.1) (q₂ p.1 p.2 ≫ b.inj p.2) ⋯
hc : IsColimit c
⊢ IsPullback (Cofan.IsColimit.desc hd fun (p : ι × ι') ↦ q₁ p.1 p.2 ≫ a.inj p.1)
    (Cofan.IsColimit.desc hd fun (p : ι × ι') ↦ q₂ p.1 p.2 ≫ b.inj p.2) u v
have refine_1 : pullback u v ≅ d.pt
Tactic: refine (IsPullback.of_hasPullback u v).of_iso
      ?_ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ (by simp) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan.{u_4, v, u} Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst_1 : ∀ (i : ι), HasPullback (f i) v
inst_2 : HasPullback u v
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
c : Cofan P :=
  Cofan.mk (pullback u v) fun (p : ι × ι') ↦ pullback.lift (q₁ p.1 p.2 ≫ a.inj p.1) (q₂ p.1 p.2 ≫ b.inj p.2) ⋯
hc : IsColimit c
refine_1 : pullback u v ≅ d.pt
⊢ IsPullback (Cofan.IsColimit.desc hd fun (p : ι × ι') ↦ q₁ p.1 p.2 ≫ a.inj p.1)
    (Cofan.IsColimit.desc hd fun (p : ι × ι') ↦ q₂ p.1 p.2 ≫ b.inj p.2) u v
have refine_2 : pullback.fst u v ≫ Iso.hom (Iso.refl a.pt) =
  (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun (p : ι × ι') ↦ q₁ p.1 p.2 ≫ a.inj p.1
Tactic: refine (IsPullback.of_hasPullback u v).of_iso
      ?_ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ (by simp) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan.{u_4, v, u} Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst_1 : ∀ (i : ι), HasPullback (f i) v
inst_2 : HasPullback u v
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
c : Cofan P :=
  Cofan.mk (pullback u v) fun (p : ι × ι') ↦ pullback.lift (q₁ p.1 p.2 ≫ a.inj p.1) (q₂ p.1 p.2 ≫ b.inj p.2) ⋯
hc : IsColimit c
refine_1 : pullback u v ≅ d.pt
refine_2 :
  pullback.fst u v ≫ Iso.hom (Iso.refl a.pt) =
    (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun (p : ι × ι') ↦ q₁ p.1 p.2 ≫ a.inj p.1
⊢ IsPullback (Cofan.IsColimit.desc hd fun (p : ι × ι') ↦ q₁ p.1 p.2 ≫ a.inj p.1)
    (Cofan.IsColimit.desc hd fun (p : ι × ι') ↦ q₂ p.1 p.2 ≫ b.inj p.2) u v
have refine_3 : pullback.snd u v ≫ Iso.hom (Iso.refl b.pt) =
  (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun (p : ι × ι') ↦ q₂ p.1 p.2 ≫ b.inj p.2
Tactic: refine (IsPullback.of_hasPullback u v).of_iso
      ?_ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ (by simp) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan.{u_4, v, u} Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst_1 : ∀ (i : ι), HasPullback (f i) v
inst_2 : HasPullback u v
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
c : Cofan P :=
  Cofan.mk (pullback u v) fun (p : ι × ι') ↦ pullback.lift (q₁ p.1 p.2 ≫ a.inj p.1) (q₂ p.1 p.2 ≫ b.inj p.2) ⋯
hc : IsColimit c
⊢ pullback.fst u v ≫ Iso.hom (Iso.refl a.pt) =
    (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun (p : ι × ι') ↦ q₁ p.1 p.2 ≫ a.inj p.1
have refine_2 : ∀ (i : ι × ι'),
  c.inj i ≫ pullback.fst u v ≫ Iso.hom (Iso.refl a.pt) =
    c.inj i ≫ (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun (p : ι × ι') ↦ q₁ p.1 p.2 ≫ a.inj p.1
Tactic: refine Cofan.IsColimit.hom_ext hc _ _ fun i ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_3
ι' : Type u_4
S : C
X : ι → C
a : Cofan.{u_3, v, u} X
hau : IsUniversalColimit a
Y : ι' → C
b : Cofan.{u_4, v, u} Y
hbu : IsUniversalColimit b
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
u : a.pt ⟶ S
v : b.pt ⟶ S
inst_1 : ∀ (i : ι), HasPullback (f i) v
inst_2 : HasPullback u v
P : ι × ι' → C
q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i
q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j
hP : ∀ (i : ι) (j : ι'), IsPullback (q₁ i j) (q₂ i j) (f i) (g j)
d : Cofan P
hd : IsColimit d
hu : ∀ (i : ι), a.inj i ≫ u = f i
hv : ∀ (i : ι'), b.inj i ≫ v = g i
c : Cofan P :=
  Cofan.mk (pullback u v) fun (p : ι × ι') ↦ pullback.lift (q₁ p.1 p.2 ≫ a.inj p.1) (q₂ p.1 p.2 ≫ b.inj p.2) ⋯
hc : IsColimit c
⊢ pullback.snd u v ≫ Iso.hom (Iso.refl b.pt) =
    (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun (p : ι × ι') ↦ q₂ p.1 p.2 ≫ b.inj p.2
have refine_3 : ∀ (i : ι × ι'),
  c.inj i ≫ pullback.snd u v ≫ Iso.hom (Iso.refl b.pt) =
    c.inj i ≫ (hc.coconePointUniqueUpToIso hd).hom ≫ Cofan.IsColimit.desc hd fun (p : ι × ι') ↦ q₂ p.1 p.2 ≫ b.inj p.2
Tactic: refine Cofan.IsColimit.hom_ext hc _ _ fun i ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : Cᵒᵖ
s : Cocone.{v, v, u, v + 1} (Functor.obj coyoneda X)
Y : C
⊢ CategoryStruct.comp (Y := Functor.obj (Functor.obj (Functor.const C) (Cocone.pt (colimitCocone X))) Y)
      (NatTrans.app (Cocone.ι (colimitCocone X)) Y)
      (↾fun (x : Cocone.pt (colimitCocone X)) ↦
        (hom (FC := TypeCat.Fun) (s.ι.app (unop X)) :
            (a : (fun (X : Type v) ↦ X) ((coyoneda.obj X).obj (unop X))) →
              (fun (X : Type v) ↦ X) (((Functor.const C).obj s.pt).obj (unop X)))
          (𝟙 (unop X))) =
    s.ι.app Y
have h : ∀ (f : Functor.obj (Functor.obj coyoneda X) Y),
  TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y := Functor.obj (Functor.obj (Functor.const C) (Cocone.pt (colimitCocone X))) Y)
          (NatTrans.app (Cocone.ι (colimitCocone X)) Y)
          (↾fun (x : Cocone.pt (colimitCocone X)) ↦
            (hom (FC := TypeCat.Fun) (s.ι.app (unop X)) :
                (a : (fun (X : Type v) ↦ X) ((coyoneda.obj X).obj (unop X))) →
                  (fun (X : Type v) ↦ X) (((Functor.const C).obj s.pt).obj (unop X)))
              (𝟙 (unop X)))))
      f =
    (hom (FC := TypeCat.Fun) (s.ι.app Y)).toFun f
Tactic: ext f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X : Cᵒᵖ
s : Cocone.{v, v, u, v + 1} (Functor.obj coyoneda X)
m : Cocone.pt (colimitCocone X) ⟶ s.pt
w : ∀ (j : C), NatTrans.app (Cocone.ι (colimitCocone X)) j ≫ m = s.ι.app j
⊢ m =
    ↾fun (x : Cocone.pt (colimitCocone X)) ↦
      (hom (FC := TypeCat.Fun) (s.ι.app (unop X)) :
          (a : (fun (X : Type v) ↦ X) ((coyoneda.obj X).obj (unop X))) →
            (fun (X : Type v) ↦ X) (((Functor.const C).obj s.pt).obj (unop X)))
        (𝟙 (unop X))
have h : (hom (FC := TypeCat.Fun) m).toFun PUnit.unit =
  TypeCat.Fun.toFun
    (hom (FC := TypeCat.Fun)
      (↾fun (x : Cocone.pt (colimitCocone X)) ↦
        (hom (FC := TypeCat.Fun) (s.ι.app (unop X)) :
            (a : (fun (X : Type v) ↦ X) ((coyoneda.obj X).obj (unop X))) →
              (fun (X : Type v) ↦ X) (((Functor.const C).obj s.pt).obj (unop X)))
          (𝟙 (unop X))))
    PUnit.unit
Tactic: ext ⟨⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J Cᵒᵖ
X : C
c : Cone F
hc : IsLimit c
⊢ Nonempty (IsLimit (F := F ⋙ Functor.obj yoneda X) (Functor.mapCone (Functor.obj yoneda X) c))
have rw : ∀ s ∈ (F ⋙ Functor.obj yoneda X).sections,
  ∃! x : Cone.pt (F := F ⋙ Functor.obj yoneda X) (Functor.mapCone (Functor.obj yoneda X) c),
    ∀ (j : J),
      (hom (FC := TypeCat.Fun) (NatTrans.app (Cone.π (Functor.mapCone (Functor.obj yoneda X) c)) j) :
            (a : (fun (X : Type v) ↦ X) (((Functor.const J).obj ((yoneda.obj X).mapCone c).pt).obj j)) →
              (fun (X : Type v) ↦ X) ((F ⋙ yoneda.obj X).obj j))
          x =
        s j
Tactic: rw [Types.isLimit_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J Cᵒᵖ
c : Cone F
hc : (X : C) → IsLimit (F := F ⋙ Functor.obj yoneda X) (Functor.mapCone (Functor.obj yoneda X) c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m.unop =
    Quiver.Hom.unop
      (Quiver.Hom.op
        ((hom (FC := TypeCat.Fun) (IsLimit.lift (hc (unop s.pt)) (Functor.mapCone (Functor.obj yoneda (unop s.pt)) s)) :
            (a : (fun (X : Type v) ↦ X) ((yoneda.obj (unop s.pt)).mapCone s).pt) →
              (fun (X : Type v) ↦ X) ((yoneda.obj (unop s.pt)).mapCone c).pt)
          (𝟙 (unop s.pt))))
have a : Eq (α := (↑(F ⋙ Functor.obj yoneda (unop s.pt)).sections : Type (max v w)))
  ((Types.isLimitEquivSections (hc (unop s.pt)) :
        (a : ((yoneda.obj (unop s.pt)).mapCone c).pt) → (↑(F ⋙ yoneda.obj (unop s.pt)).sections : Type (max v w)))
      m.unop :
    (↑(F ⋙ Functor.obj yoneda (unop s.pt)).sections : Type (max v w)))
  ((Types.isLimitEquivSections (hc (unop s.pt)) :
        (a : ((yoneda.obj (unop s.pt)).mapCone c).pt) → (↑(F ⋙ yoneda.obj (unop s.pt)).sections : Type (max v w)))
      (Quiver.Hom.unop
        (Quiver.Hom.op
          ((hom (FC := TypeCat.Fun)
                (IsLimit.lift (hc (unop s.pt)) (Functor.mapCone (Functor.obj yoneda (unop s.pt)) s)) :
              (a : (fun (X : Type v) ↦ X) ((yoneda.obj (unop s.pt)).mapCone s).pt) →
                (fun (X : Type v) ↦ X) ((yoneda.obj (unop s.pt)).mapCone c).pt)
            (𝟙 (unop s.pt))))) :
    (↑(F ⋙ Functor.obj yoneda (unop s.pt)).sections : Type (max v w)))
Tactic: apply (Types.isLimitEquivSections (hc s.pt.unop)).injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J Cᵒᵖ
c : Cone F
hc : (X : C) → IsLimit (F := F ⋙ Functor.obj yoneda X) (Functor.mapCone (Functor.obj yoneda X) c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ Eq (α := (↑(F ⋙ Functor.obj yoneda (unop s.pt)).sections : Type (max v w)))
    ((Types.isLimitEquivSections (hc (unop s.pt)) :
          (a : ((yoneda.obj (unop s.pt)).mapCone c).pt) → (↑(F ⋙ yoneda.obj (unop s.pt)).sections : Type (max v w)))
        m.unop :
      (↑(F ⋙ Functor.obj yoneda (unop s.pt)).sections : Type (max v w)))
    ((Types.isLimitEquivSections (hc (unop s.pt)) :
          (a : ((yoneda.obj (unop s.pt)).mapCone c).pt) → (↑(F ⋙ yoneda.obj (unop s.pt)).sections : Type (max v w)))
        (Quiver.Hom.unop
          (Quiver.Hom.op
            ((hom (FC := TypeCat.Fun)
                  (IsLimit.lift (hc (unop s.pt)) (Functor.mapCone (Functor.obj yoneda (unop s.pt)) s)) :
                (a : (fun (X : Type v) ↦ X) ((yoneda.obj (unop s.pt)).mapCone s).pt) →
                  (fun (X : Type v) ↦ X) ((yoneda.obj (unop s.pt)).mapCone c).pt)
              (𝟙 (unop s.pt))))) :
      (↑(F ⋙ Functor.obj yoneda (unop s.pt)).sections : Type (max v w)))
have a : ∀ (j : J),
  Eq.{v + 1} (α := (F ⋙ Functor.obj yoneda (unop s.pt)).obj j)
    ((↑((Types.isLimitEquivSections (hc (unop s.pt)) :
              (a : ((yoneda.obj (unop s.pt)).mapCone c).pt) → (↑(F ⋙ yoneda.obj (unop s.pt)).sections : Type (max v w)))
            m.unop) :
        (j : J) → (F ⋙ yoneda.obj (unop s.pt)).obj j)
      j)
    ((↑((Types.isLimitEquivSections (hc (unop s.pt)) :
              (a : ((yoneda.obj (unop s.pt)).mapCone c).pt) → (↑(F ⋙ yoneda.obj (unop s.pt)).sections : Type (max v w)))
            (Quiver.Hom.unop
              (Quiver.Hom.op
                ((hom (FC := TypeCat.Fun)
                      (IsLimit.lift (hc (unop s.pt)) (Functor.mapCone (Functor.obj yoneda (unop s.pt)) s)) :
                    (a : (fun (X : Type v) ↦ X) ((yoneda.obj (unop s.pt)).mapCone s).pt) →
                      (fun (X : Type v) ↦ X) ((yoneda.obj (unop s.pt)).mapCone c).pt)
                  (𝟙 (unop s.pt)))))) :
        (j : J) → (F ⋙ yoneda.obj (unop s.pt)).obj j)
      j)
Tactic: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J Cᵒᵖ
c : Cone F
hc : (X : C) → IsLimit (F := F ⋙ Functor.obj yoneda X) (Functor.mapCone (Functor.obj yoneda X) c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
j : J
⊢ Eq.{v + 1} (α := (F ⋙ Functor.obj yoneda (unop s.pt)).obj j)
    ((↑((Types.isLimitEquivSections (hc (unop s.pt)) :
              (a : ((yoneda.obj (unop s.pt)).mapCone c).pt) → (↑(F ⋙ yoneda.obj (unop s.pt)).sections : Type (max v w)))
            m.unop) :
        (j : J) → (F ⋙ yoneda.obj (unop s.pt)).obj j)
      j)
    ((↑((Types.isLimitEquivSections (hc (unop s.pt)) :
              (a : ((yoneda.obj (unop s.pt)).mapCone c).pt) → (↑(F ⋙ yoneda.obj (unop s.pt)).sections : Type (max v w)))
            (Quiver.Hom.unop
              (Quiver.Hom.op
                ((hom (FC := TypeCat.Fun)
                      (IsLimit.lift (hc (unop s.pt)) (Functor.mapCone (Functor.obj yoneda (unop s.pt)) s)) :
                    (a : (fun (X : Type v) ↦ X) ((yoneda.obj (unop s.pt)).mapCone s).pt) →
                      (fun (X : Type v) ↦ X) ((yoneda.obj (unop s.pt)).mapCone c).pt)
                  (𝟙 (unop s.pt)))))) :
        (j : J) → (F ⋙ yoneda.obj (unop s.pt)).obj j)
      j)
have eq : Eq (α := (F ⋙ Functor.obj yoneda (unop s.pt)).obj j)
  ((hom (FC := TypeCat.Fun)
          (IsLimit.lift (hc (unop s.pt)) (Functor.mapCone (Functor.obj yoneda (unop s.pt)) s) ≫
            NatTrans.app (Cone.π (Functor.mapCone (Functor.obj yoneda (unop s.pt)) c)) j) :
        (a : ((yoneda.obj (unop s.pt)).mapCone s).pt) → (F ⋙ yoneda.obj (unop s.pt)).obj j)
      (𝟙 (unop s.pt)) :
    (F ⋙ Functor.obj yoneda (unop s.pt)).obj j)
  (((@hom _ types TypeCat.Fun _ _ _ _ _ (NatTrans.app (Cone.π (Functor.mapCone (Functor.obj yoneda (unop s.pt)) s)) j) :
          TypeCat.Fun
            (Cone.pt (F := F ⋙ Functor.obj yoneda (unop s.pt)) (Functor.mapCone (Functor.obj yoneda (unop s.pt)) s))
            ((F ⋙ Functor.obj yoneda (unop s.pt)).obj j)) :
        (a : ((yoneda.obj (unop s.pt)).mapCone s).pt) → (F ⋙ yoneda.obj (unop s.pt)).obj j)
      (𝟙 (unop s.pt)) :
    (F ⋙ Functor.obj yoneda (unop s.pt)).obj j)
Tactic: have eq := congr_hom ((hc s.pt.unop).fac ((yoneda.obj s.pt.unop).mapCone s) j) (𝟙 (unop s.pt))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J Cᵒᵖ
c : Cone F
hc : (X : C) → IsLimit (F := F ⋙ Functor.obj yoneda X) (Functor.mapCone (Functor.obj yoneda X) c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
j : J
eq :
  Eq (α := (F ⋙ Functor.obj yoneda (unop s.pt)).obj j)
    ((hom (FC := TypeCat.Fun)
            (IsLimit.lift (hc (unop s.pt)) (Functor.mapCone (Functor.obj yoneda (unop s.pt)) s) ≫
              NatTrans.app (Cone.π (Functor.mapCone (Functor.obj yoneda (unop s.pt)) c)) j) :
          (a : ((yoneda.obj (unop s.pt)).mapCone s).pt) → (F ⋙ yoneda.obj (unop s.pt)).obj j)
        (𝟙 (unop s.pt)) :
      (F ⋙ Functor.obj yoneda (unop s.pt)).obj j)
    (((@hom _ types TypeCat.Fun _ _ _ _ _
              (NatTrans.app (Cone.π (Functor.mapCone (Functor.obj yoneda (unop s.pt)) s)) j) :
            TypeCat.Fun
              (Cone.pt (F := F ⋙ Functor.obj yoneda (unop s.pt)) (Functor.mapCone (Functor.obj yoneda (unop s.pt)) s))
              ((F ⋙ Functor.obj yoneda (unop s.pt)).obj j)) :
          (a : ((yoneda.obj (unop s.pt)).mapCone s).pt) → (F ⋙ yoneda.obj (unop s.pt)).obj j)
        (𝟙 (unop s.pt)) :
      (F ⋙ Functor.obj yoneda (unop s.pt)).obj j)
⊢ Eq.{v + 1} (α := (F ⋙ Functor.obj yoneda (unop s.pt)).obj j)
    ((↑((Types.isLimitEquivSections (hc (unop s.pt)) :
              (a : ((yoneda.obj (unop s.pt)).mapCone c).pt) → (↑(F ⋙ yoneda.obj (unop s.pt)).sections : Type (max v w)))
            m.unop) :
        (j : J) → (F ⋙ yoneda.obj (unop s.pt)).obj j)
      j)
    ((↑((Types.isLimitEquivSections (hc (unop s.pt)) :
              (a : ((yoneda.obj (unop s.pt)).mapCone c).pt) → (↑(F ⋙ yoneda.obj (unop s.pt)).sections : Type (max v w)))
            (Quiver.Hom.unop
              (Quiver.Hom.op
                ((hom (FC := TypeCat.Fun)
                      (IsLimit.lift (hc (unop s.pt)) (Functor.mapCone (Functor.obj yoneda (unop s.pt)) s)) :
                    (a : (fun (X : Type v) ↦ X) ((yoneda.obj (unop s.pt)).mapCone s).pt) →
                      (fun (X : Type v) ↦ X) ((yoneda.obj (unop s.pt)).mapCone c).pt)
                  (𝟙 (unop s.pt)))))) :
        (j : J) → (F ⋙ yoneda.obj (unop s.pt)).obj j)
      j)
have a : (c.π.app j).unop ≫ m.unop =
  (c.π.app j).unop ≫
    (@hom _ types TypeCat.Fun _ _ _ _ _
          (IsLimit.lift (hc (unop s.pt)) (Functor.mapCone (Functor.obj yoneda (unop s.pt)) s)) :
        (a : unop s.pt ⟶ unop s.pt) → unop c.pt ⟶ unop s.pt)
      (𝟙 (unop s.pt))
Tactic: dsimp [Types.isLimitEquivSections, Types.sectionOfCone]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
c : Cocone F
x : (X : C) → IsLimit (F := F.op ⋙ Functor.obj yoneda X) (Functor.mapCone (Functor.obj yoneda X) c.op)
⊢ (fun (h : IsColimit c) (x : C) ↦
        (isLimitOfPreserves (Functor.obj yoneda x) h.op :
          IsLimit (F := F.op ⋙ Functor.obj yoneda x) (Functor.mapCone (Functor.obj yoneda x) c.op)))
      ((fun (h : (X : C) → IsLimit (F := F.op ⋙ Functor.obj yoneda X) (Functor.mapCone (Functor.obj yoneda X) c.op)) ↦
          (yonedaJointlyReflectsLimits F.op c.op h).unop)
        x) =
    x
have h : ∀ (x_1 : C),
  (fun (h : IsColimit c) (x : C) ↦
        (isLimitOfPreserves (Functor.obj yoneda x) h.op :
          IsLimit (F := F.op ⋙ Functor.obj yoneda x) (Functor.mapCone (Functor.obj yoneda x) c.op)))
      ((fun (h : (X : C) → IsLimit (F := F.op ⋙ Functor.obj yoneda X) (Functor.mapCone (Functor.obj yoneda X) c.op)) ↦
          (yonedaJointlyReflectsLimits F.op c.op h).unop)
        x)
      x_1 =
    x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
X : Cᵒᵖ
c : Cone F
hc : IsLimit c
⊢ Nonempty (IsLimit (F := F ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) c))
have rw : ∀ s ∈ (F ⋙ Functor.obj coyoneda X).sections,
  ∃! x : Cone.pt (F := F ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) c),
    ∀ (j : J),
      (hom (FC := TypeCat.Fun) (NatTrans.app (Cone.π (Functor.mapCone (Functor.obj coyoneda X) c)) j) :
            (a : (fun (X : Type v) ↦ X) (((Functor.const J).obj ((coyoneda.obj X).mapCone c).pt).obj j)) →
              (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj X).obj j))
          x =
        s j
Tactic: rw [Types.isLimit_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit (F := F ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ m =
    (hom (FC := TypeCat.Fun) (IsLimit.lift (hc (op s.pt)) (Functor.mapCone (Functor.obj coyoneda (op s.pt)) s)) :
        (a : (fun (X : Type v) ↦ X) ((coyoneda.obj (op s.pt)).mapCone s).pt) →
          (fun (X : Type v) ↦ X) ((coyoneda.obj (op s.pt)).mapCone c).pt)
      (𝟙 (unop (op s.pt)))
have a : Eq (α := (↑(F ⋙ Functor.obj coyoneda (op s.pt)).sections : Type (max v w)))
  ((Types.isLimitEquivSections (hc (op s.pt)) :
        (a : ((coyoneda.obj (op s.pt)).mapCone c).pt) → (↑(F ⋙ coyoneda.obj (op s.pt)).sections : Type (max v w)))
      m :
    (↑(F ⋙ Functor.obj coyoneda (op s.pt)).sections : Type (max v w)))
  ((Types.isLimitEquivSections (hc (op s.pt)) :
        (a : ((coyoneda.obj (op s.pt)).mapCone c).pt) → (↑(F ⋙ coyoneda.obj (op s.pt)).sections : Type (max v w)))
      ((hom (FC := TypeCat.Fun) (IsLimit.lift (hc (op s.pt)) (Functor.mapCone (Functor.obj coyoneda (op s.pt)) s)) :
          (a : (fun (X : Type v) ↦ X) ((coyoneda.obj (op s.pt)).mapCone s).pt) →
            (fun (X : Type v) ↦ X) ((coyoneda.obj (op s.pt)).mapCone c).pt)
        (𝟙 (unop (op s.pt)))) :
    (↑(F ⋙ Functor.obj coyoneda (op s.pt)).sections : Type (max v w)))
Tactic: apply (Types.isLimitEquivSections (hc (op s.pt))).injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit (F := F ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
⊢ Eq (α := (↑(F ⋙ Functor.obj coyoneda (op s.pt)).sections : Type (max v w)))
    ((Types.isLimitEquivSections (hc (op s.pt)) :
          (a : ((coyoneda.obj (op s.pt)).mapCone c).pt) → (↑(F ⋙ coyoneda.obj (op s.pt)).sections : Type (max v w)))
        m :
      (↑(F ⋙ Functor.obj coyoneda (op s.pt)).sections : Type (max v w)))
    ((Types.isLimitEquivSections (hc (op s.pt)) :
          (a : ((coyoneda.obj (op s.pt)).mapCone c).pt) → (↑(F ⋙ coyoneda.obj (op s.pt)).sections : Type (max v w)))
        ((hom (FC := TypeCat.Fun) (IsLimit.lift (hc (op s.pt)) (Functor.mapCone (Functor.obj coyoneda (op s.pt)) s)) :
            (a : (fun (X : Type v) ↦ X) ((coyoneda.obj (op s.pt)).mapCone s).pt) →
              (fun (X : Type v) ↦ X) ((coyoneda.obj (op s.pt)).mapCone c).pt)
          (𝟙 (unop (op s.pt)))) :
      (↑(F ⋙ Functor.obj coyoneda (op s.pt)).sections : Type (max v w)))
have a : ∀ (j : J),
  Eq.{v + 1} (α := (F ⋙ Functor.obj coyoneda (op s.pt)).obj j)
    ((↑((Types.isLimitEquivSections (hc (op s.pt)) :
              (a : ((coyoneda.obj (op s.pt)).mapCone c).pt) → (↑(F ⋙ coyoneda.obj (op s.pt)).sections : Type (max v w)))
            m) :
        (j : J) → (F ⋙ coyoneda.obj (op s.pt)).obj j)
      j)
    ((↑((Types.isLimitEquivSections (hc (op s.pt)) :
              (a : ((coyoneda.obj (op s.pt)).mapCone c).pt) → (↑(F ⋙ coyoneda.obj (op s.pt)).sections : Type (max v w)))
            ((hom (FC := TypeCat.Fun)
                  (IsLimit.lift (hc (op s.pt)) (Functor.mapCone (Functor.obj coyoneda (op s.pt)) s)) :
                (a : (fun (X : Type v) ↦ X) ((coyoneda.obj (op s.pt)).mapCone s).pt) →
                  (fun (X : Type v) ↦ X) ((coyoneda.obj (op s.pt)).mapCone c).pt)
              (𝟙 (unop (op s.pt))))) :
        (j : J) → (F ⋙ coyoneda.obj (op s.pt)).obj j)
      j)
Tactic: ext j