awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.SigmaConst (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst_2 : HasCoproduct.{u_1, v, u} (C := C) fun (x : α) ↦ R
inst_3 : HasCoproduct.{u_2, v, u} (C := C) fun (x : β) ↦ R
inst_4 : HasCoproduct.{u_2, v, u} (C := C) fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R
s :
  Cofork.{v, u} (C := C) (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
    (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0
m :
  Cocone.pt.{0, v, 0, u} (F :=
      parallelPair (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
        (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0)
      (sigmaConstCokernelCofork R f) ⟶
    s.pt
hm : Cofork.π (sigmaConstCokernelCofork R f) ≫ m = s.π
b : β
hb : b ∈ (Set.range f)ᶜ
⊢ Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) ≫
      m =
    CategoryStruct.comp (Y := sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
      (Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb))
      (Sigma.desc fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦
        Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (↑x : β) ≫ s.π)
have h : Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
      (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) ≫
    m =
  Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) : β) ≫ s.π
Tactic: rw [Sigma.ι_desc, ← hm, ι_sigmaConstCokernelCofork_π_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.SigmaConst (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst_2 : HasCoproduct.{u_1, v, u} (C := C) fun (x : α) ↦ R
inst_3 : HasCoproduct.{u_2, v, u} (C := C) fun (x : β) ↦ R
inst_4 : HasCoproduct.{u_2, v, u} (C := C) fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R
s :
  Cofork.{v, u} (C := C) (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
    (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0
m :
  Cocone.pt.{0, v, 0, u} (F :=
      parallelPair (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
        (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0)
      (sigmaConstCokernelCofork R f) ⟶
    s.pt
hm : Cofork.π (sigmaConstCokernelCofork R f) ≫ m = s.π
b : β
hb : b ∈ (Set.range f)ᶜ
h :
  Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) ≫
      m =
    Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) : β) ≫
      s.π
⊢ Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) ≫
      m =
    CategoryStruct.comp (Y := sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
      (Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb))
      (Sigma.desc fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦
        Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (↑x : β) ≫ s.π)
have h₁ : Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
      (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) ≫
    m =
  Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) : β) ≫
    Cofork.π (sigmaConstCokernelCofork R f) ≫ m
Tactic: rw [Sigma.ι_desc, ← hm, ι_sigmaConstCokernelCofork_π_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.SigmaConst (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst_2 : HasCoproduct.{u_1, v, u} (C := C) fun (x : α) ↦ R
inst_3 : HasCoproduct.{u_2, v, u} (C := C) fun (x : β) ↦ R
inst_4 : HasCoproduct.{u_2, v, u} (C := C) fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R
s :
  Cofork.{v, u} (C := C) (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
    (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0
m :
  Cocone.pt.{0, v, 0, u} (F :=
      parallelPair (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
        (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0)
      (sigmaConstCokernelCofork R f) ⟶
    s.pt
hm : Cofork.π (sigmaConstCokernelCofork R f) ≫ m = s.π
b : β
hb : b ∈ (Set.range f)ᶜ
h :
  Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) ≫
      m =
    Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) : β) ≫
      s.π
h₁ :
  Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) ≫
      m =
    Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) : β) ≫
      Cofork.π (sigmaConstCokernelCofork R f) ≫ m
⊢ Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) ≫
      m =
    CategoryStruct.comp (Y := sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
      (Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb))
      (Sigma.desc fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦
        Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (↑x : β) ≫ s.π)
have h₂ : Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
      (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) ≫
    m =
  Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
      (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ)
        (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) : β) hb) ≫
    m
Tactic: rw [Sigma.ι_desc, ← hm, ι_sigmaConstCokernelCofork_π_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.SigmaConst (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
α : Type u_1
β : Type u_2
f : α → β
inst_2 : HasCoproduct.{u_1, v, u} (C := C) fun (x : α) ↦ R
inst_3 : HasCoproduct.{u_2, v, u} (C := C) fun (x : β) ↦ R
inst_4 : HasCoproduct.{u_2, v, u} (C := C) fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R
s :
  Cofork.{v, u} (C := C) (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
    (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0
m :
  Cocone.pt.{0, v, 0, u} (F :=
      parallelPair (X := sigmaObj.{u_1, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{u_2, v, u} fun (x : β) ↦ R)
        (Sigma.map' f fun (x : α) ↦ 𝟙 R) 0)
      (sigmaConstCokernelCofork R f) ⟶
    s.pt
hm : Cofork.π (sigmaConstCokernelCofork R f) ≫ m = s.π
b : β
hb : b ∈ (Set.range f)ᶜ
h :
  Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) ≫
      m =
    Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) : β) ≫
      s.π
h₁ :
  Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) ≫
      m =
    Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) : β) ≫
      Cofork.π (sigmaConstCokernelCofork R f) ≫ m
h₂ :
  Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) ≫
      m =
    Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ)
          (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) : β) hb) ≫
      m
⊢ Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) ≫
      m =
    CategoryStruct.comp (Y := sigmaObj.{u_2, v, u} fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
      (Sigma.ι.{u_2, v, u} (C := C) (fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦ R)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb))
      (Sigma.desc fun (x : (↑(Set.range f)ᶜ : Type u_2)) ↦
        Sigma.ι.{u_2, v, u} (C := C) (fun (x : β) ↦ R) (↑x : β) ≫ s.π)
have h₃ : (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ (Set.range f)ᶜ) b hb) : β) ∉ Set.range f
Tactic: rw [Sigma.ι_desc, ← hm, ι_sigmaConstCokernelCofork_π_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.SigmaConst (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
R : C
inst_2 : HasCoproducts.{w, v, u} C
α β : Type w
f : α ⟶ β
⊢ HasCokernel.{v, u} (X := Functor.obj.{w, v, w + 1, u} (Functor.obj sigmaConst R) α)
    (Functor.map (Functor.obj sigmaConst R) f)
have dsimp : HasCokernel.{v, u} (C := C) (X := sigmaObj.{w, v, u} fun (x : α) ↦ R) (Y := sigmaObj.{w, v, u} fun (x : β) ↦ R)
  (Sigma.map' (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : α) → β) fun (x : α) ↦ 𝟙 R)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Ulift (goal)
Goal:
J : Type w
inst : Category.{w', w} J
K : Functor.{w', u, w, u + 1} J (Type u)
c : Cone K
hc : IsLimit c
⊢ Nonempty (IsLimit (uliftFunctor.{v, u}.mapCone c))
have rw : ∀ s ∈ (K ⋙ uliftFunctor.{v, u}).sections,
  ∃! x : (uliftFunctor.{v, u}.mapCone c).pt,
    ∀ (j : J),
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((uliftFunctor.{v, u}.mapCone c).π.app j) :
            (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const J).obj (uliftFunctor.{v, u}.mapCone c).pt).obj j)) →
              (fun (X : Type (max u v)) ↦ X) ((K ⋙ uliftFunctor.{v, u}).obj j))
          x =
        s j
Tactic: rw [Types.isLimit_iff ((uliftFunctor.{v, u}).mapCone c)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Ulift (goal)
Goal:
J : Type w
inst : Category.{w', w} J
K : Functor.{w', u, w, u + 1} J (Type u)
c : Cone K
hc : IsLimit c
s : (j : J) → (K ⋙ uliftFunctor.{v, u}).obj j
hs : s ∈ (K ⋙ uliftFunctor.{v, u}).sections
⊢ ∃! x : (uliftFunctor.{v, u}.mapCone c).pt,
    ∀ (j : J),
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((uliftFunctor.{v, u}.mapCone c).π.app j) :
            (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const J).obj (uliftFunctor.{v, u}.mapCone c).pt).obj j)) →
              (fun (X : Type (max u v)) ↦ X) ((K ⋙ uliftFunctor.{v, u}).obj j))
          x =
        s j
have obtain : ∀ (x : c.pt)
  (hx₁ :
    ∀ (j : J),
      Eq (α := (fun (X : Type u) ↦ X) (K.obj j))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.π.app j) :
              (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j)) → (fun (X : Type u) ↦ X) (K.obj j))
            x :
          (fun (X : Type u) ↦ X) (K.obj j))
        ((↑(((sectionsEquiv K).symm :
                    (a : (↑(K ⋙ uliftFunctor.{v, u}).sections : Type (max (max u w) v))) →
                      (↑K.sections : Type (max u w)))
                  (Subtype.mk (p := fun (x : (j : J) → (K ⋙ uliftFunctor.{v, u}).obj j) ↦
                    x ∈ (K ⋙ uliftFunctor.{v, u}).sections) s sorry)) :
              (j : J) → K.obj j)
            j :
          K.obj j))
  (hx₂ :
    ∀ (y : c.pt),
      (fun (x : c.pt) ↦
            ∀ (j : J),
              Eq (α := (fun (X : Type u) ↦ X) (K.obj j))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.π.app j) :
                      (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj j)) →
                        (fun (X : Type u) ↦ X) (K.obj j))
                    x :
                  (fun (X : Type u) ↦ X) (K.obj j))
                ((↑(((sectionsEquiv K).symm :
                            (a : (↑(K ⋙ uliftFunctor.{v, u}).sections : Type (max (max u w) v))) →
                              (↑K.sections : Type (max u w)))
                          (Subtype.mk (p := fun (x : (j : J) → (K ⋙ uliftFunctor.{v, u}).obj j) ↦
                            x ∈ (K ⋙ uliftFunctor.{v, u}).sections) s sorry)) :
                      (j : J) → K.obj j)
                    j :
                  K.obj j))
          y →
        y = x),
  ∃! x : (uliftFunctor.{v, u}.mapCone c).pt,
    ∀ (j : J),
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((uliftFunctor.{v, u}.mapCone c).π.app j) :
            (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const J).obj (uliftFunctor.{v, u}.mapCone c).pt).obj j)) →
              (fun (X : Type (max u v)) ↦ X) ((K ⋙ uliftFunctor.{v, u}).obj j))
          x =
        s j
Tactic: obtain ⟨x, hx₁, hx₂⟩ := (Types.isLimit_iff c).mp ⟨hc⟩ _ ((sectionsEquiv K).symm ⟨s, hs⟩).2
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Ulift (goal)
Goal:
J_1 : Type u_1
inst : Category.{v_1, u_1} J_1
K : Functor.{v_1, u, u_1, u + 1} J_1 (Type u)
c_1 : Cocone K
hc_1 : IsColimit c_1
lc : Cocone (K ⋙ uliftFunctor.{v, u})
J : Type w
x : Category.{w', w} J
F : Functor.{w', u, w, u + 1} J (Type u)
c : Cocone F
hc : IsColimit c
⊢ Nonempty (IsColimit (uliftFunctor.{v, u}.mapCocone c))
have rw : Functor.CoconeTypes.IsColimit (J := J) (F := F ⋙ uliftFunctor.{v, u})
  (((F ⋙ uliftFunctor.{v, u}).coconeTypesEquiv.symm :
      (a : Cocone (F ⋙ uliftFunctor.{v, u})) → (F ⋙ uliftFunctor.{v, u}).CoconeTypes)
    (uliftFunctor.{v, u}.mapCocone c))
Tactic: rw [isColimit_iff_coconeTypesIsColimit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasColimitsOfShape.{v₂, u₂, v₁, v₁ + 1} J (Type v₁)
inst_3 : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
X : C
⊢ Eq (α := colimit (F ⋙ obj coyoneda (op (obj yoneda X))) ⟶ obj yoneda X ⟶ colimit F)
    (CategoryStruct.comp (Y := colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}))
      (colimMap (F.whiskerLeft (NatTrans.app (Iso.hom largeCurriedYonedaLemma) (op X))) :
        colimit (F ⋙ obj coyoneda (op (obj yoneda X))) ⟶
          colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X) ⋙ uliftFunctor.{u₁, v₁}))
      (CategoryStruct.comp (Y := ULift.{u₁, v₁} (colimit (F.flip.obj (op X))))
          (Iso.inv (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))))
          ((↾fun (x : ULift.{u₁, v₁} (colimit (F.flip.obj (op X)))) ↦
              {
                down :=
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (colimitObjIsoColimitCompEvaluation F (op X))) :
                        TypeCat.Fun (colimit (F.flip.obj (op X))) ((colimit F).obj (op X))) :
                      (a : colimit (F.flip.obj (op X))) → (colimit F).obj (op X))
                    x.down }) ≫
            (yonedaOpCompYonedaObj (colimit F)).inv.app (op X)) :
        colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}) ⟶ obj yoneda X ⟶ colimit F))
    (colimit.post F (obj coyoneda (op (obj yoneda X))))
have w : ∀ (j : J),
  CategoryStruct.comp (Y := colimit (F ⋙ obj coyoneda (op (obj yoneda X))))
      (colimit.ι (F ⋙ obj coyoneda (op (obj yoneda X))) j)
      (CategoryStruct.comp (Y := colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}))
        (colimMap (F.whiskerLeft (NatTrans.app (Iso.hom largeCurriedYonedaLemma) (op X))) :
          colimit (F ⋙ obj coyoneda (op (obj yoneda X))) ⟶
            colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X) ⋙ uliftFunctor.{u₁, v₁}))
        (CategoryStruct.comp (Y := ULift.{u₁, v₁} (colimit (F.flip.obj (op X))))
            (Iso.inv (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))))
            ((↾fun (x : ULift.{u₁, v₁} (colimit (F.flip.obj (op X)))) ↦
                {
                  down :=
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (colimitObjIsoColimitCompEvaluation F (op X))) :
                          TypeCat.Fun (colimit (F.flip.obj (op X))) ((colimit F).obj (op X))) :
                        (a : colimit (F.flip.obj (op X))) → (colimit F).obj (op X))
                      x.down }) ≫
              (yonedaOpCompYonedaObj (colimit F)).inv.app (op X)) :
          colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}) ⟶ obj yoneda X ⟶ colimit F)) =
    CategoryStruct.comp (Y := colimit (F ⋙ obj coyoneda (op (obj yoneda X))))
      (colimit.ι (F ⋙ obj coyoneda (op (obj yoneda X))) j) (colimit.post F (obj coyoneda (op (obj yoneda X))))
Tactic: apply colimit.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasColimitsOfShape.{v₂, u₂, v₁, v₁ + 1} J (Type v₁)
inst_3 : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
X : C
j : J
⊢ CategoryStruct.comp (Y := colimit (F ⋙ obj coyoneda (op (obj yoneda X))))
      (colimit.ι (F ⋙ obj coyoneda (op (obj yoneda X))) j)
      (CategoryStruct.comp (Y := colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}))
        (colimMap (F.whiskerLeft (NatTrans.app (Iso.hom largeCurriedYonedaLemma) (op X))) :
          colimit (F ⋙ obj coyoneda (op (obj yoneda X))) ⟶
            colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X) ⋙ uliftFunctor.{u₁, v₁}))
        (CategoryStruct.comp (Y := ULift.{u₁, v₁} (colimit (F.flip.obj (op X))))
            (Iso.inv (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))))
            ((↾fun (x : ULift.{u₁, v₁} (colimit (F.flip.obj (op X)))) ↦
                {
                  down :=
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (colimitObjIsoColimitCompEvaluation F (op X))) :
                          TypeCat.Fun (colimit (F.flip.obj (op X))) ((colimit F).obj (op X))) :
                        (a : colimit (F.flip.obj (op X))) → (colimit F).obj (op X))
                      x.down }) ≫
              (yonedaOpCompYonedaObj (colimit F)).inv.app (op X)) :
          colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}) ⟶ obj yoneda X ⟶ colimit F)) =
    CategoryStruct.comp (Y := colimit (F ⋙ obj coyoneda (op (obj yoneda X))))
      (colimit.ι (F ⋙ obj coyoneda (op (obj yoneda X))) j) (colimit.post F (obj coyoneda (op (obj yoneda X))))
have w : Eq (α := (F ⋙ obj coyoneda (op (obj yoneda X))).obj j ⟶ obj yoneda X ⟶ colimit F)
  ((F.whiskerLeft (NatTrans.app (Iso.hom largeCurriedYonedaLemma) (op X))).app j ≫
    CategoryStruct.comp (Y := colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X) ⋙ uliftFunctor.{u₁, v₁}))
      (colimit.ι (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X) ⋙ uliftFunctor.{u₁, v₁}) j :
        (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X) ⋙ uliftFunctor.{u₁, v₁}).obj j ⟶
          colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X) ⋙ uliftFunctor.{u₁, v₁}))
      (CategoryStruct.comp (Y := ULift.{u₁, v₁} (colimit (F.flip.obj (op X))))
          (Iso.inv (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))))
          ((↾fun (x : ULift.{u₁, v₁} (colimit (F.flip.obj (op X)))) ↦
              {
                down :=
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (colimitObjIsoColimitCompEvaluation F (op X))) :
                        TypeCat.Fun (colimit (F.flip.obj (op X))) ((colimit F).obj (op X))) :
                      (a : colimit (F.flip.obj (op X))) → (colimit F).obj (op X))
                    x.down }) ≫
            (yonedaOpCompYonedaObj (colimit F)).inv.app (op X)) :
        colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}) ⟶ obj yoneda X ⟶ colimit F))
  (map (obj coyoneda (op (obj yoneda X))) (colimit.ι F j))
Tactic: rw [colimit.ι_post, ι_colimMap_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasColimitsOfShape.{v₂, u₂, v₁, v₁ + 1} J (Type v₁)
inst_3 : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
X : C
j : J
⊢ Eq (α := (F ⋙ obj coyoneda (op (obj yoneda X))).obj j ⟶ obj yoneda X ⟶ colimit F)
    ((F.whiskerLeft (NatTrans.app (Iso.hom largeCurriedYonedaLemma) (op X))).app j ≫
      CategoryStruct.comp (Y := colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X) ⋙ uliftFunctor.{u₁, v₁}))
        (colimit.ι (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X) ⋙ uliftFunctor.{u₁, v₁}) j :
          (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X) ⋙ uliftFunctor.{u₁, v₁}).obj j ⟶
            colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X) ⋙ uliftFunctor.{u₁, v₁}))
        (CategoryStruct.comp (Y := ULift.{u₁, v₁} (colimit (F.flip.obj (op X))))
            (Iso.inv (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))))
            ((↾fun (x : ULift.{u₁, v₁} (colimit (F.flip.obj (op X)))) ↦
                {
                  down :=
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (colimitObjIsoColimitCompEvaluation F (op X))) :
                          TypeCat.Fun (colimit (F.flip.obj (op X))) ((colimit F).obj (op X))) :
                        (a : colimit (F.flip.obj (op X))) → (colimit F).obj (op X))
                      x.down }) ≫
              (yonedaOpCompYonedaObj (colimit F)).inv.app (op X)) :
          colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}) ⟶ obj yoneda X ⟶ colimit F))
    (map (obj coyoneda (op (obj yoneda X))) (colimit.ι F j))
have w : Eq (α := (F ⋙ obj coyoneda (op (obj yoneda X))).obj j ⟶ obj yoneda X ⟶ colimit F)
  ((F.whiskerLeft (NatTrans.app (Iso.hom largeCurriedYonedaLemma) (op X))).app j ≫
    CategoryStruct.comp (Y := colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}))
      (colimit.ι (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}) j :
        (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}).obj j ⟶ colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}))
      (CategoryStruct.comp (Y := ULift.{u₁, v₁} (colimit (F.flip.obj (op X))))
          (Iso.inv (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))))
          ((↾fun (x : ULift.{u₁, v₁} (colimit (F.flip.obj (op X)))) ↦
              {
                down :=
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (colimitObjIsoColimitCompEvaluation F (op X))) :
                        TypeCat.Fun (colimit (F.flip.obj (op X))) ((colimit F).obj (op X))) :
                      (a : colimit (F.flip.obj (op X))) → (colimit F).obj (op X))
                    x.down }) ≫
            (yonedaOpCompYonedaObj (colimit F)).inv.app (op X)) :
        colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}) ⟶ obj yoneda X ⟶ colimit F))
  (map (obj coyoneda (op (obj yoneda X))) (colimit.ι F j))
Tactic: simp only [← CategoryTheory.Functor.assoc, comp_evaluation]