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

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.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
X₁✝ X₂✝ : C
k₁✝ : X ⟶ F.obj X₁✝
k₂✝ : X ⟶ F.obj X₂✝
f✝ : X₁✝ ⟶ X₂✝
h₁ : k₁✝ ≫ F.map f✝ = k₂✝
h₂ : G.map k₂✝ ≫ c.ι.app X₂✝ = G.map f ≫ c.ι.app Y
⊢ G.map k₁✝ ≫ c.ι.app X₁✝ = G.map f ≫ c.ι.app Y

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

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.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
X₁✝ X₂✝ : C
k₁✝ : X ⟶ F.obj X₁✝
k₂✝ : X ⟶ F.obj X₂✝
f✝ : X₁✝ ⟶ X₂✝
h₁ : k₁✝ ≫ F.map f✝ = k₂✝
h₂ : G.map k₁✝ ≫ c.ι.app X₁✝ = G.map f ≫ c.ι.app Y
⊢ G.map k₂✝ ≫ c.ι.app X₂✝ = G.map f ≫ c.ι.app Y

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.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
⊢ ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ →
      (fun Z g => G.map g ≫ c.ι.app Z = G.map f ≫ c.ι.app Y) X₂ k₂ →
        (fun Z g => G.map g ≫ c.ι.app Z = G.map f ≫ c.ι.app Y) 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.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
X₁✝ X₂✝ : C
k₁✝ : X ⟶ F.obj X₁✝
k₂✝ : X ⟶ F.obj X₂✝
f✝ : X₁✝ ⟶ X₂✝
h₁ : k₁✝ ≫ F.map f✝ = k₂✝
h₂ : G.map k₂✝ ≫ c.ι.app X₂✝ = G.map f ≫ c.ι.app Y
⊢ G.map k₁✝ ≫ c.ι.app X₁✝ = G.map f ≫ c.ι.app Y

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.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
⊢ ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ →
      (fun Z g => G.map g ≫ c.ι.app Z = G.map f ≫ c.ι.app Y) X₁ k₁ →
        (fun Z g => G.map g ≫ c.ι.app Z = G.map f ≫ c.ι.app Y) 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.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
X₁✝ X₂✝ : C
k₁✝ : X ⟶ F.obj X₁✝
k₂✝ : X ⟶ F.obj X₂✝
f✝ : X₁✝ ⟶ X₂✝
h₁ : k₁✝ ≫ F.map f✝ = k₂✝
h₂ : G.map k₁✝ ≫ c.ι.app X₁✝ = G.map f ≫ c.ι.app Y
⊢ G.map k₂✝ ≫ c.ι.app X₂✝ = G.map f ≫ c.ι.app Y

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

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

Result:
case h₁
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
⊢ ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ →
      (fun Z g => G.map g ≫ c.ι.app Z = G.map f ≫ c.ι.app Y) X₁ k₁ →
        (fun Z g => G.map g ≫ c.ι.app Z = G.map f ≫ c.ι.app Y) 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.Final
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
c : Cocone (F ⋙ G)
X : D
Y : C
f : X ⟶ F.obj Y
⊢ ∀ (X₁ X₂ : C) (k₁ : X ⟶ F.obj X₁) (k₂ : X ⟶ F.obj X₂) (f_1 : X₁ ⟶ X₂),
    k₁ ≫ F.map f_1 = k₂ →
      (fun Z g => G.map g ≫ c.ι.app Z = G.map f ≫ c.ι.app Y) X₂ k₂ →
        (fun Z g => G.map g ≫ c.ι.app Z = G.map f ≫ c.ι.app Y) X₁ k₁