-- Mathlib/CategoryTheory/Limits/Final.lean
/-- Alternative equational lemma for `(extendCone c).π.app` in case a lift of the object
is given explicitly. -/
lemma extendCone_obj_π_app' (c : Cone (F ⋙ G)) {X : C} {Y : D} (f : F.obj X ⟶ Y) :
    (extendCone.obj c).π.app Y = c.π.app X ≫ G.map f

Proof state:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X : C
Y : D
f : F.obj X ⟶ Y
⊢ ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ Y) (k₂ : F.obj X₂ ⟶ Y) (f_1 : X₁ ⟶ X₂),
    F.map f_1 ≫ k₂ = k₁ →
      (fun Z g => c.π.app Z ≫ G.map g = c.π.app X ≫ G.map f) X₁ k₁ →
        (fun Z g => c.π.app Z ≫ G.map g = c.π.app X ≫ G.map f) X₂ k₂

Tactic:
intro _ _ _ _ _ h₁ h₂

Result:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X : C
Y : D
f : F.obj X ⟶ Y
X₁✝ X₂✝ : C
k₁✝ : F.obj X₁✝ ⟶ Y
k₂✝ : F.obj X₂✝ ⟶ Y
f✝ : X₁✝ ⟶ X₂✝
h₁ : F.map f✝ ≫ k₂✝ = k₁✝
h₂ : c.π.app X₁✝ ≫ G.map k₁✝ = c.π.app X ≫ G.map f
⊢ c.π.app X₂✝ ≫ G.map k₂✝ = c.π.app X ≫ G.map f

Proof state:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X : C
Y : D
f : F.obj X ⟶ Y
X₁✝ X₂✝ : C
k₁✝ : F.obj X₁✝ ⟶ Y
k₂✝ : F.obj X₂✝ ⟶ Y
f✝ : X₁✝ ⟶ X₂✝
h₁ : F.map f✝ ≫ k₂✝ = k₁✝
h₂ : c.π.app X₂✝ ≫ G.map k₂✝ = c.π.app X ≫ G.map f
⊢ c.π.app X₁✝ ≫ G.map k₁✝ = c.π.app X ≫ G.map f

Tactic:
simp [← h₁, ← Functor.comp_map, c.π.naturality, h₂]

Result:
no goals

Proof state:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X : C
Y : D
f : F.obj X ⟶ Y
⊢ ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ Y) (k₂ : F.obj X₂ ⟶ Y) (f_1 : X₁ ⟶ X₂),
    F.map f_1 ≫ k₂ = k₁ →
      (fun Z g => c.π.app Z ≫ G.map g = c.π.app X ≫ G.map f) X₂ k₂ →
        (fun Z g => c.π.app Z ≫ G.map g = c.π.app X ≫ G.map f) X₁ k₁

Tactic:
intro _ _ _ _ _ h₁ h₂

Result:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X : C
Y : D
f : F.obj X ⟶ Y
X₁✝ X₂✝ : C
k₁✝ : F.obj X₁✝ ⟶ Y
k₂✝ : F.obj X₂✝ ⟶ Y
f✝ : X₁✝ ⟶ X₂✝
h₁ : F.map f✝ ≫ k₂✝ = k₁✝
h₂ : c.π.app X₂✝ ≫ G.map k₂✝ = c.π.app X ≫ G.map f
⊢ c.π.app X₁✝ ≫ G.map k₁✝ = c.π.app X ≫ G.map f

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X : C
Y : D
f : F.obj X ⟶ Y
⊢ (extendCone.obj c).π.app Y = c.π.app X ≫ G.map f

Tactic:
apply induction (k₀ := f) (z := rfl) F fun Z g =>
  c.π.app Z ≫ G.map g = c.π.app X ≫ G.map f

Result:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X : C
Y : D
f : F.obj X ⟶ Y
⊢ ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ Y) (k₂ : F.obj X₂ ⟶ Y) (f_1 : X₁ ⟶ X₂),
    F.map f_1 ≫ k₂ = k₁ →
      (fun Z g => c.π.app Z ≫ G.map g = c.π.app X ≫ G.map f) X₁ k₁ →
        (fun Z g => c.π.app Z ≫ G.map g = c.π.app X ≫ G.map f) X₂ k₂

case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X : C
Y : D
f : F.obj X ⟶ Y
⊢ ∀ (X₁ X₂ : C) (k₁ : F.obj X₁ ⟶ Y) (k₂ : F.obj X₂ ⟶ Y) (f_1 : X₁ ⟶ X₂),
    F.map f_1 ≫ k₂ = k₁ →
      (fun Z g => c.π.app Z ≫ G.map g = c.π.app X ≫ G.map f) X₂ k₂ →
        (fun Z g => c.π.app Z ≫ G.map g = c.π.app X ≫ G.map f) X₁ k₁

Proof state:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Initial
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cone (F ⋙ G)
X : C
Y : D
f : F.obj X ⟶ Y
X₁✝ X₂✝ : C
k₁✝ : F.obj X₁✝ ⟶ Y
k₂✝ : F.obj X₂✝ ⟶ Y
f✝ : X₁✝ ⟶ X₂✝
h₁ : F.map f✝ ≫ k₂✝ = k₁✝
h₂ : c.π.app X₁✝ ≫ G.map k₁✝ = c.π.app X ≫ G.map f
⊢ c.π.app X₂✝ ≫ G.map k₂✝ = c.π.app X ≫ G.map f

Tactic:
simp [← h₂, ← h₁, ← Functor.comp_map, c.π.naturality]

Result:
no goals