awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Final
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)

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⟩
-- Module: Mathlib.CategoryTheory.Limits.Final
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)
h : ∀ (j₁ j₂ : StructuredArrow d F), Zigzag j₁ j₂
⊢ IsConnected.{v, v} (StructuredArrow d F)

Tactic:
apply zigzag_isConnected

Premises used: CategoryTheory.zigzag_isConnected
-- Module: Mathlib.CategoryTheory.Limits.Final
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₂
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})
⊢ y₁ = y₂

Tactic:
apply (I d).toEquiv.injective

Premises used: CategoryTheory.Iso.toEquiv, Equiv.injective
-- Module: Mathlib.CategoryTheory.Limits.Final
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₂
⊢ 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:
ext
-- Module: Mathlib.CategoryTheory.Limits.Final
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₂

Tactic:
have e : y₁ = y₂ := by
      apply (I d).toEquiv.injective
      ext
-- Module: Mathlib.CategoryTheory.Limits.Final
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₂
⊢ 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
-- Module: Mathlib.CategoryTheory.Limits.Final
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₂
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₂)
⊢ Zigzag { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := X₁, hom := f₁ : Comma (fromPUnit d) F }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }

Tactic:
Final.zigzag_of_eqvGen_colimitTypeRel t

Premises used: CategoryTheory.Functor.Final.zigzag_of_eqvGen_colimitTypeRel, CategoryTheory.StructuredArrow.mk
-- Module: Mathlib.CategoryTheory.Limits.Final
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₂
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₂)
⊢ Zigzag { left := { as := PUnit.unit : Discrete PUnit.{1} }, right := X₁, hom := f₁ : Comma (fromPUnit d) F }
    { left := { as := PUnit.unit }, right := X₂, hom := f₂ }

Tactic:
exact Final.zigzag_of_eqvGen_colimitTypeRel t

Premises used: CategoryTheory.Functor.Final.zigzag_of_eqvGen_colimitTypeRel
-- Module: Mathlib.CategoryTheory.Limits.Final
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

Tactic:
final_of_colimit_comp_coyoneda_iso_pUnit _ (fun d => ?_)

Premises used: CategoryTheory.Functor.final_of_colimit_comp_coyoneda_iso_pUnit
-- Module: Mathlib.CategoryTheory.Limits.Final
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))
refine : (d : D) → colimit (F ⋙ obj coyoneda (op d)) ≅ PUnit.{v + 1}
⊢ F.Final

Tactic:
refine final_of_colimit_comp_coyoneda_iso_pUnit _ (fun d => ?_)

Premises used: CategoryTheory.Functor.final_of_colimit_comp_coyoneda_iso_pUnit
-- Module: Mathlib.CategoryTheory.Limits.Final
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
refine : IsTerminal (colimit (F ⋙ obj coyoneda (op d)))
⊢ colimit (F ⋙ obj coyoneda (op d)) ≅ PUnit.{v + 1}

Tactic:
refine Types.isTerminalEquivIsoPUnit _ ?_

Premises used: CategoryTheory.Limits.Types.isTerminalEquivIsoPUnit, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Limits.Final
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
b : IsTerminal (obj (obj (evaluation Dᵒᵖ (Type v)) (op d)) (colimit (F ⋙ yoneda))) :=
  IsTerminal.isTerminalObj (obj (evaluation Dᵒᵖ (Type v)) (op d)) (colimit (F ⋙ yoneda)) h
⊢ IsTerminal (colimit (F ⋙ obj coyoneda (op d)))

Tactic:
exact b.ofIso <| preservesColimitIso ((evaluation _ _).obj (Opposite.op d)) (F ⋙ yoneda)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.yoneda, CategoryTheory.preservesColimitIso, Opposite.op, CategoryTheory.evaluation, CategoryTheory.Limits.IsTerminal.ofIso, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.Final
Goal:
C : Type v
inst : Category.{v, v} C
D : Type v
inst_1 : Category.{v, v} D
F : C ⥤ D
⊢ F.Final ↔ ∀ (G : D ⥤ Type v), IsIso (X := colimit (F ⋙ G)) (Y := colimit G) (colimit.pre G F)

Tactic:
⟨fun _ => inferInstance,
   fun _ => final_of_colimit_comp_coyoneda_iso_pUnit _ fun _ => Final.colimitCompCoyonedaIso _ _⟩

Premises used: CategoryTheory.Functor.final_of_colimit_comp_coyoneda_iso_pUnit, inferInstance, Iff.intro, CategoryTheory.Functor.Final.colimitCompCoyonedaIso
-- Module: Mathlib.CategoryTheory.Limits.Final
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
d : D
⊢ Nonempty (CostructuredArrow F d)

Tactic:
IsConnected.is_nonempty

Premises used: CategoryTheory.IsConnected.is_nonempty
-- Module: Mathlib.CategoryTheory.Limits.Final
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₀
h : Nonempty.{u_1} (Z (lift F d) (homToLift F d))
⊢ Z (lift F d) (homToLift F d)

Tactic:
apply Nonempty.some

Premises used: Nonempty.some
-- Module: Mathlib.CategoryTheory.Limits.Final
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₂
_₁ :
  {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))

Tactic:
apply
    @isPreconnected_induction _ _ _ (fun Y : CostructuredArrow F d => Z Y.left Y.hom) _ _
      (CostructuredArrow.mk k₀) z

Premises used: CategoryTheory.CostructuredArrow.hom, CategoryTheory.isPreconnected_induction, CategoryTheory.CostructuredArrow.left
-- Module: Mathlib.CategoryTheory.Limits.Final
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
fapply : F.map f.left ≫ j₂.hom = j₁.hom
⊢ Z j₂.left j₂.hom

Tactic:
fapply h₁ _ _ _ _ f.left _ a

Premises used: CategoryTheory.CommaMorphism.left
-- Module: Mathlib.CategoryTheory.Limits.Final
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 ≫ map (fromPUnit d) f.right

Tactic:
f.w

Premises used: CategoryTheory.CommaMorphism.w
-- Module: Mathlib.CategoryTheory.Limits.Final
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
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
⊢ F.map f.left ≫ j₂.hom = j₁.hom

Tactic:
convert! f.w

Premises used: CategoryTheory.CommaMorphism.w
-- Module: Mathlib.CategoryTheory.Limits.Final
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
e_1 : (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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Final
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
fapply : F.map f.left ≫ j₂.hom = j₁.hom
⊢ Z j₁.left j₁.hom

Tactic:
fapply h₂ _ _ _ _ f.left _ a

Premises used: CategoryTheory.CommaMorphism.left
-- Module: Mathlib.CategoryTheory.Limits.Final
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 ≫ map (fromPUnit d) f.right

Tactic:
f.w

Premises used: CategoryTheory.CommaMorphism.w
-- Module: Mathlib.CategoryTheory.Limits.Final
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
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
⊢ F.map f.left ≫ j₂.hom = j₁.hom

Tactic:
convert! f.w

Premises used: CategoryTheory.CommaMorphism.w
-- Module: Mathlib.CategoryTheory.Limits.Final
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
e_1 : (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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Final
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
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
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Final
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
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)
⊢ 𝟙 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:
simp only [Category.id_comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Final
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
k₀ : F.obj (lift 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)

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

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.Functor.Initial.lift, CategoryTheory.Functor.map, CategoryTheory.Functor.Initial.induction, CategoryTheory.Functor.Initial.homToLift, CategoryTheory.CategoryStruct.comp, Eq, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Final
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

Tactic:
rw [← a, Functor.map_comp, ← Functor.comp_map, ← Category.assoc, ← Category.assoc,
                c.w] at z

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.Cone.w, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.comp_map