awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ obj coyoneda (op d)) ≅ PUnit.{v + 1}
d : D
⊢ Nonempty.{v + 1} (StructuredArrow d F)
have have : ∀ (this : (fun (X : Type v) ↦ X) (colimit (F ⋙ obj coyoneda (op d)))), Nonempty.{v + 1} (StructuredArrow d F)
Tactic: have := (I d).inv PUnit.unit
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ obj coyoneda (op d)) ≅ PUnit.{v + 1}
d : D
this : (fun (X : Type v) ↦ X) (colimit (F ⋙ obj coyoneda (op d)))
⊢ Nonempty.{v + 1} (StructuredArrow d F)
have obtain : ∀ (j : C) (y : (F ⋙ obj coyoneda (op d)).obj j), Nonempty.{v + 1} (StructuredArrow d F)
Tactic: obtain ⟨j, y, rfl⟩ := Limits.Types.jointly_surjective'.{v, v} this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (hypothesis)
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ obj coyoneda (op d)) ≅ PUnit.{v + 1}
d : D
⊢ IsConnected.{v, v} (StructuredArrow d F)
have this : Nonempty.{v + 1} (StructuredArrow d F)
Tactic: have : Nonempty (StructuredArrow d F) := by
      have := (I d).inv PUnit.unit
      obtain ⟨j, y, rfl⟩ := Limits.Types.jointly_surjective'.{v, v} this
      exact ⟨StructuredArrow.mk y⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ obj coyoneda (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty.{v + 1} (StructuredArrow d F)
⊢ IsConnected.{v, v} (StructuredArrow d F)
have h : ∀ (j₁ j₂ : StructuredArrow d F), Zigzag j₁ j₂
Tactic: apply zigzag_isConnected
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ obj coyoneda (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty.{v + 1} (StructuredArrow d F)
X₁ : C
f₁ : obj.{0, v, 0, u₁} (fromPUnit d) { as := PUnit.unit : Discrete PUnit.{1} } ⟶ F.obj X₁
X₂ : C
f₂ : obj.{0, v, 0, u₁} (fromPUnit d) { as := PUnit.unit : Discrete PUnit.{1} } ⟶ F.obj X₂
y₁ : (fun (X : Type v) ↦ X) (colimit (F ⋙ obj coyoneda (op d))) :=
  (ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) X₁) :
      (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj X₁)) →
        (fun (X : Type v) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
    f₁
y₂ : (fun (X : Type v) ↦ X) (colimit (F ⋙ obj coyoneda (op d))) :=
  (ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) X₂) :
      (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj X₂)) →
        (fun (X : Type v) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
    f₂
⊢ y₁ = y₂
have a : Eq (α := PUnit.{v + 1}) (((I d).toEquiv : (a : colimit (F ⋙ coyoneda.obj (op d))) → PUnit.{v + 1}) y₁ : PUnit.{v + 1})
  (((I d).toEquiv : (a : colimit (F ⋙ coyoneda.obj (op d))) → PUnit.{v + 1}) y₂ : PUnit.{v + 1})
Tactic: apply (I d).toEquiv.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (hypothesis)
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ obj coyoneda (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty.{v + 1} (StructuredArrow d F)
X₁ : C
f₁ : obj.{0, v, 0, u₁} (fromPUnit d) { as := PUnit.unit : Discrete PUnit.{1} } ⟶ F.obj X₁
X₂ : C
f₂ : obj.{0, v, 0, u₁} (fromPUnit d) { as := PUnit.unit : Discrete PUnit.{1} } ⟶ F.obj X₂
y₁ : (fun (X : Type v) ↦ X) (colimit (F ⋙ obj coyoneda (op d))) :=
  (ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) X₁) :
      (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj X₁)) →
        (fun (X : Type v) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
    f₁
y₂ : (fun (X : Type v) ↦ X) (colimit (F ⋙ obj coyoneda (op d))) :=
  (ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) X₂) :
      (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj X₂)) →
        (fun (X : Type v) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
    f₂
⊢ Zigzag { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := X₁, hom := f₁ : Comma (fromPUnit d) F }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }
have e : y₁ = y₂
Tactic: have e : y₁ = y₂ := by
      apply (I d).toEquiv.injective
      ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (hypothesis)
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
I : (d : D) → colimit (F ⋙ obj coyoneda (op d)) ≅ PUnit.{v + 1}
d : D
this : Nonempty.{v + 1} (StructuredArrow d F)
X₁ : C
f₁ : obj.{0, v, 0, u₁} (fromPUnit d) { as := PUnit.unit : Discrete PUnit.{1} } ⟶ F.obj X₁
X₂ : C
f₂ : obj.{0, v, 0, u₁} (fromPUnit d) { as := PUnit.unit : Discrete PUnit.{1} } ⟶ F.obj X₂
y₁ : (fun (X : Type v) ↦ X) (colimit (F ⋙ obj coyoneda (op d))) :=
  (ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) X₁) :
      (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj X₁)) →
        (fun (X : Type v) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
    f₁
y₂ : (fun (X : Type v) ↦ X) (colimit (F ⋙ obj coyoneda (op d))) :=
  (ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj coyoneda (op d)) X₂) :
      (a : (fun (X : Type v) ↦ X) ((F ⋙ coyoneda.obj (op d)).obj X₂)) →
        (fun (X : Type v) ↦ X) (colimit (F ⋙ coyoneda.obj (op d))))
    f₂
e : y₁ = y₂
⊢ Zigzag { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := X₁, hom := f₁ : Comma (fromPUnit d) F }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }
have t : Relation.EqvGen (F ⋙ obj coyoneda (op d)).ColimitTypeRel
  (Sigma.mk (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j) X₁ f₁)
  (Sigma.mk (β := fun (j : C) ↦ (F ⋙ obj coyoneda (op d)).obj j) X₂ f₂)
Tactic: have t := Types.colimit_eq.{v, v} e
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
h : IsTerminal (colimit (F ⋙ yoneda))
⊢ F.Final
have refine : (d : D) → colimit (F ⋙ obj coyoneda (op d)) ≅ PUnit.{v + 1}
Tactic: refine final_of_colimit_comp_coyoneda_iso_pUnit _ (fun d => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type v
inst : Category.{v, v} C
D : Type u₁
inst_1 : Category.{v, u₁} D
F : C ⥤ D
h : IsTerminal (colimit (F ⋙ yoneda))
d : D
⊢ colimit (F ⋙ obj coyoneda (op d)) ≅ PUnit.{v + 1}
have refine : IsTerminal (colimit (F ⋙ obj coyoneda (op d)))
Tactic: refine Types.isTerminalEquivIsoPUnit _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
d : D
Z : (X : C) → (F.obj X ⟶ d) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : F.obj X₀ ⟶ d
z : Z X₀ k₀
⊢ Z (lift F d) (homToLift F d)
have h : Nonempty.{u_1} (Z (lift F d) (homToLift F d))
Tactic: apply Nonempty.some
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
d : D
Z : (X : C) → (F.obj X ⟶ d) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : F.obj X₀ ⟶ d
z : Z X₀ k₀
⊢ Nonempty.{u_1} (Z (lift F d) (homToLift F d))
have _ : {j₁ j₂ : CostructuredArrow F d} →
  (j₁ ⟶ j₂) →
    (fun (Y : CostructuredArrow F d) ↦ Z Y.left Y.hom) j₁ → (fun (Y : CostructuredArrow F d) ↦ Z Y.left Y.hom) j₂
Tactic: apply
    @isPreconnected_induction _ _ _ (fun Y : CostructuredArrow F d => Z Y.left Y.hom) _ _
      (CostructuredArrow.mk k₀) z
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
d : D
Z : (X : C) → (F.obj X ⟶ d) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : F.obj X₀ ⟶ d
z : Z X₀ k₀
_ :
  {j₁ j₂ : CostructuredArrow F d} →
    (j₁ ⟶ j₂) →
      (fun (Y : CostructuredArrow F d) ↦ Z Y.left Y.hom) j₁ → (fun (Y : CostructuredArrow F d) ↦ Z Y.left Y.hom) j₂
⊢ Nonempty.{u_1} (Z (lift F d) (homToLift F d))
have _₁ : {j₁ j₂ : CostructuredArrow F d} →
  (j₁ ⟶ j₂) →
    (fun (Y : CostructuredArrow F d) ↦ Z Y.left Y.hom) j₂ → (fun (Y : CostructuredArrow F d) ↦ Z Y.left Y.hom) j₁
Tactic: apply
    @isPreconnected_induction _ _ _ (fun Y : CostructuredArrow F d => Z Y.left Y.hom) _ _
      (CostructuredArrow.mk k₀) z
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
d : D
Z : (X : C) → (F.obj X ⟶ d) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : F.obj X₀ ⟶ d
z : Z X₀ k₀
j₁ j₂ : CostructuredArrow F d
f : j₁ ⟶ j₂
a : Z j₁.left j₁.hom
⊢ Z j₂.left j₂.hom
have fapply : F.map f.left ≫ j₂.hom = j₁.hom
Tactic: fapply h₁ _ _ _ _ f.left _ a
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
d : D
Z : (X : C) → (F.obj X ⟶ d) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : F.obj X₀ ⟶ d
z : Z X₀ k₀
j₁ j₂ : CostructuredArrow F d
f : j₁ ⟶ j₂
a : Z j₁.left j₁.hom
⊢ F.map f.left ≫ j₂.hom = j₁.hom
have h : (F.obj j₁.left ⟶ d) = (F.obj j₁.left ⟶ obj.{0, v₂, 0, u₂} (fromPUnit d) j₂.right) →
  j₁.hom = j₁.hom ≫ map (fromPUnit d) f.right
Tactic: convert! f.w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
d : D
Z : (X : C) → (F.obj X ⟶ d) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : F.obj X₀ ⟶ d
z : Z X₀ k₀
j₁ j₂ : CostructuredArrow F d
f : j₁ ⟶ j₂
a : Z j₂.left j₂.hom
⊢ Z j₁.left j₁.hom
have fapply : F.map f.left ≫ j₂.hom = j₁.hom
Tactic: fapply h₂ _ _ _ _ f.left _ a
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
d : D
Z : (X : C) → (F.obj X ⟶ d) → Sort u_1
h₁ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₁ k₁ → Z X₂ k₂
h₂ : (X₁ X₂ : C) → (k₁ : F.obj X₁ ⟶ d) → (k₂ : F.obj X₂ ⟶ d) → (f : X₁ ⟶ X₂) → F.map f ≫ k₂ = k₁ → Z X₂ k₂ → Z X₁ k₁
X₀ : C
k₀ : F.obj X₀ ⟶ d
z : Z X₀ k₀
j₁ j₂ : CostructuredArrow F d
f : j₁ ⟶ j₂
a : Z j₂.left j₂.hom
⊢ F.map f.left ≫ j₂.hom = j₁.hom
have h : (F.obj j₁.left ⟶ d) = (F.obj j₁.left ⟶ obj.{0, v₂, 0, u₂} (fromPUnit d) j₂.right) →
  j₁.hom = j₁.hom ≫ map (fromPUnit d) f.right
Tactic: convert! f.w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ Eq.{v₃ + 1} (α := obj.{v₂, v₃, u₂, u₃} (obj (const D) c.pt) X ⟶ G.obj Y)
    (map (obj (const D) c.pt) f ≫
      CategoryStruct.comp (Y := (F ⋙ G).obj (lift F Y)) (c.π.app (lift F Y)) (G.map (homToLift F Y)))
    (CategoryStruct.comp (Y := (F ⋙ G).obj (lift F X)) (c.π.app (lift F X)) (G.map (homToLift F X)) ≫ G.map f)
have dsimp : 𝟙 c.pt ≫ CategoryStruct.comp (Y := G.obj (F.obj (lift F Y))) (c.π.app (lift F Y)) (G.map (homToLift F Y)) =
  CategoryStruct.comp (Y := G.obj (F.obj (lift F X))) (c.π.app (lift F X)) (G.map (homToLift F X)) ≫ G.map f
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ 𝟙 c.pt ≫ CategoryStruct.comp (Y := G.obj (F.obj (lift F Y))) (c.π.app (lift F Y)) (G.map (homToLift F Y)) =
    CategoryStruct.comp (Y := G.obj (F.obj (lift F X))) (c.π.app (lift F X)) (G.map (homToLift F X)) ≫ G.map f
have simp : Eq (α := c.pt ⟶ G.obj Y)
  (CategoryStruct.comp (Y := G.obj (F.obj (lift F Y))) (c.π.app (lift F Y)) (G.map (homToLift F Y)) : c.pt ⟶ G.obj Y)
  (CategoryStruct.comp (Y := G.obj (F.obj (lift F X))) (c.π.app (lift F X)) (G.map (homToLift F X) ≫ G.map f) :
    c.pt ⟶ G.obj Y)
Tactic: simp only [Category.id_comp, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
⊢ Eq (α := c.pt ⟶ G.obj Y)
    (CategoryStruct.comp (Y := G.obj (F.obj (lift F Y))) (c.π.app (lift F Y)) (G.map (homToLift F Y)) : c.pt ⟶ G.obj Y)
    (CategoryStruct.comp (Y := G.obj (F.obj (lift F X))) (c.π.app (lift F X)) (G.map (homToLift F X) ≫ G.map f) :
      c.pt ⟶ G.obj Y)
have h₁ : ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ Y) (k₂ : F.obj X₂ ⟶ Y) (f_1 : X₁ ⟶ X₂),
  F.map f_1 ≫ k₂ = k₁ →
    c.π.app X₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f →
      c.π.app X₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
Tactic: apply
              induction F fun Z k =>
                (c.π.app Z ≫ G.map k : c.pt ⟶ _) =
                  c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
h₁ :
  ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ Y) (k₂ : F.obj X₂ ⟶ Y) (f_1 : X₁ ⟶ X₂),
    F.map f_1 ≫ k₂ = k₁ →
      c.π.app X₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f →
        c.π.app X₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
⊢ Eq (α := c.pt ⟶ G.obj Y)
    (CategoryStruct.comp (Y := G.obj (F.obj (lift F Y))) (c.π.app (lift F Y)) (G.map (homToLift F Y)) : c.pt ⟶ G.obj Y)
    (CategoryStruct.comp (Y := G.obj (F.obj (lift F X))) (c.π.app (lift F X)) (G.map (homToLift F X) ≫ G.map f) :
      c.pt ⟶ G.obj Y)
have h₂ : ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ Y) (k₂ : F.obj X₂ ⟶ Y) (f_1 : X₁ ⟶ X₂),
  F.map f_1 ≫ k₂ = k₁ →
    c.π.app X₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f →
      c.π.app X₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
Tactic: apply
              induction F fun Z k =>
                (c.π.app Z ≫ G.map k : c.pt ⟶ _) =
                  c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
h₁ :
  ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ Y) (k₂ : F.obj X₂ ⟶ Y) (f_1 : X₁ ⟶ X₂),
    F.map f_1 ≫ k₂ = k₁ →
      c.π.app X₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f →
        c.π.app X₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₂ :
  ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ Y) (k₂ : F.obj X₂ ⟶ Y) (f_1 : X₁ ⟶ X₂),
    F.map f_1 ≫ k₂ = k₁ →
      c.π.app X₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f →
        c.π.app X₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
⊢ Eq (α := c.pt ⟶ G.obj Y)
    (CategoryStruct.comp (Y := G.obj (F.obj (lift F Y))) (c.π.app (lift F Y)) (G.map (homToLift F Y)) : c.pt ⟶ G.obj Y)
    (CategoryStruct.comp (Y := G.obj (F.obj (lift F X))) (c.π.app (lift F X)) (G.map (homToLift F X) ≫ G.map f) :
      c.pt ⟶ G.obj Y)
have z : Eq (α := c.pt ⟶ G.obj Y)
  (CategoryStruct.comp (Y := (F ⋙ G).obj (lift F X)) (c.π.app (lift F X)) (G.map (homToLift F X ≫ f)) : c.pt ⟶ G.obj Y)
  (c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f :
    obj.{v₁, v₃, u₁, u₃} (obj (const C) c.pt) (lift F X) ⟶ G.obj Y)
Tactic: apply
              induction F fun Z k =>
                (c.π.app Z ≫ G.map k : c.pt ⟶ _) =
                  c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
h₁ :
  ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ Y) (k₂ : F.obj X₂ ⟶ Y) (f_1 : X₁ ⟶ X₂),
    F.map f_1 ≫ k₂ = k₁ →
      c.π.app X₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f →
        c.π.app X₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₂ :
  ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ Y) (k₂ : F.obj X₂ ⟶ Y) (f_1 : X₁ ⟶ X₂),
    F.map f_1 ≫ k₂ = k₁ →
      c.π.app X₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f →
        c.π.app X₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
z :
  Eq (α := c.pt ⟶ G.obj Y)
    (CategoryStruct.comp (Y := (F ⋙ G).obj (lift F X)) (c.π.app (lift F X)) (G.map (homToLift F X ≫ f)) :
      c.pt ⟶ G.obj Y)
    (c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f :
      obj.{v₁, v₃, u₁, u₃} (obj (const C) c.pt) (lift F X) ⟶ G.obj Y)
⊢ Eq (α := c.pt ⟶ G.obj Y)
    (CategoryStruct.comp (Y := G.obj (F.obj (lift F Y))) (c.π.app (lift F Y)) (G.map (homToLift F Y)) : c.pt ⟶ G.obj Y)
    (CategoryStruct.comp (Y := G.obj (F.obj (lift F X))) (c.π.app (lift F X)) (G.map (homToLift F X) ≫ G.map f) :
      c.pt ⟶ G.obj Y)
have X₀ : C
Tactic: apply
              induction F fun Z k =>
                (c.π.app Z ≫ G.map k : c.pt ⟶ _) =
                  c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
h₁ :
  ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ Y) (k₂ : F.obj X₂ ⟶ Y) (f_1 : X₁ ⟶ X₂),
    F.map f_1 ≫ k₂ = k₁ →
      c.π.app X₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f →
        c.π.app X₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
h₂ :
  ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ Y) (k₂ : F.obj X₂ ⟶ Y) (f_1 : X₁ ⟶ X₂),
    F.map f_1 ≫ k₂ = k₁ →
      c.π.app X₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f →
        c.π.app X₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
z :
  Eq (α := c.pt ⟶ G.obj Y)
    (CategoryStruct.comp (Y := (F ⋙ G).obj (lift F X)) (c.π.app (lift F X)) (G.map (homToLift F X ≫ f)) :
      c.pt ⟶ G.obj Y)
    (c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f :
      obj.{v₁, v₃, u₁, u₃} (obj (const C) c.pt) (lift F X) ⟶ G.obj Y)
X₀ : C
⊢ Eq (α := c.pt ⟶ G.obj Y)
    (CategoryStruct.comp (Y := G.obj (F.obj (lift F Y))) (c.π.app (lift F Y)) (G.map (homToLift F Y)) : c.pt ⟶ G.obj Y)
    (CategoryStruct.comp (Y := G.obj (F.obj (lift F X))) (c.π.app (lift F X)) (G.map (homToLift F X) ≫ G.map f) :
      c.pt ⟶ G.obj Y)
have k₀ : F.obj (lift F X) ⟶ Y
Tactic: apply
              induction F fun Z k =>
                (c.π.app Z ≫ G.map k : c.pt ⟶ _) =
                  c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : F.obj Z₁ ⟶ Y
k₂ : F.obj Z₂ ⟶ Y
g : Z₁ ⟶ Z₂
a : F.map g ≫ k₂ = k₁
z : c.π.app Z₁ ≫ G.map k₁ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
⊢ c.π.app Z₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
have z₁ : c.π.app Z₂ ≫ G.map k₂ = (c.π.app (lift F X) ≫ G.map (homToLift F X)) ≫ G.map f
Tactic: rw [← a, Functor.map_comp, ← Functor.comp_map, ← Category.assoc, ← Category.assoc,
                c.w] at z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Final (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Initial
E : Type u₃
inst_3 : Category.{v₃, u₃} E
G : Functor.{v₂, v₃, u₂, u₃} D E
c : Cone (F ⋙ G)
X Y : D
f : X ⟶ Y
Z₁ Z₂ : C
k₁ : F.obj Z₁ ⟶ Y
k₂ : F.obj Z₂ ⟶ Y
g : Z₁ ⟶ Z₂
a : F.map g ≫ k₂ = k₁
z : c.π.app Z₂ ≫ G.map k₂ = (c.π.app (lift F X) ≫ G.map (homToLift F X)) ≫ G.map f
⊢ c.π.app Z₂ ≫ G.map k₂ = c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f
have h₁ : Eq (α := c.pt ⟶ G.obj Y)
  ((c.π.app (lift F X) ≫ G.map (homToLift F X)) ≫ G.map f :
    obj.{v₁, v₃, u₁, u₃} (obj (const C) c.pt) (lift F X) ⟶ G.obj Y)
  (c.π.app (lift F X) ≫ G.map (homToLift F X) ≫ G.map f)
Tactic: rw [z, Category.assoc]