-- Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
lemma isLeftKanExtension_iff_of_iso {F' F'' : D ⥤ H} (e : F' ≅ F'')
    {L : C ⥤ D} {F : C ⥤ H} (α : F ⟶ L ⋙ F') (α' : F ⟶ L ⋙ F'')
    (comm : α ≫ whiskerLeft L e.hom = α') :
    F'.IsLeftKanExtension α ↔ F''.IsLeftKanExtension α'

Proof state:
case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{u_8, u_1} C
inst✝¹ : Category.{u_7, u_3} H
inst✝ : Category.{u_6, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ whiskerLeft L e.hom = α'
a✝ : F''.IsLeftKanExtension α'
⊢ α' ≫ whiskerLeft L e.symm.hom = α

Tactic:
rw [← comm, assoc, ← whiskerLeft_comp, Iso.symm_hom, e.hom_inv_id, whiskerLeft_id', comp_id]

Result:
no goals

Proof state:
case mp
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{u_8, u_1} C
inst✝¹ : Category.{u_7, u_3} H
inst✝ : Category.{u_6, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ whiskerLeft L e.hom = α'
⊢ F'.IsLeftKanExtension α → F''.IsLeftKanExtension α'

Tactic:
intro

Result:
case mp
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{u_8, u_1} C
inst✝¹ : Category.{u_7, u_3} H
inst✝ : Category.{u_6, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ whiskerLeft L e.hom = α'
a✝ : F'.IsLeftKanExtension α
⊢ F''.IsLeftKanExtension α'

Proof state:
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{u_8, u_1} C
inst✝¹ : Category.{u_7, u_3} H
inst✝ : Category.{u_6, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ whiskerLeft L e.hom = α'
⊢ F'.IsLeftKanExtension α ↔ F''.IsLeftKanExtension α'

Tactic:
constructor

Result:
case mp
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{u_8, u_1} C
inst✝¹ : Category.{u_7, u_3} H
inst✝ : Category.{u_6, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ whiskerLeft L e.hom = α'
⊢ F'.IsLeftKanExtension α → F''.IsLeftKanExtension α'

case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{u_8, u_1} C
inst✝¹ : Category.{u_7, u_3} H
inst✝ : Category.{u_6, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ whiskerLeft L e.hom = α'
⊢ F''.IsLeftKanExtension α' → F'.IsLeftKanExtension α

Proof state:
case mp
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{u_8, u_1} C
inst✝¹ : Category.{u_7, u_3} H
inst✝ : Category.{u_6, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ whiskerLeft L e.hom = α'
a✝ : F'.IsLeftKanExtension α
⊢ F''.IsLeftKanExtension α'

Tactic:
exact isLeftKanExtension_of_iso e α α' comm

Result:
no goals

Proof state:
case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{u_8, u_1} C
inst✝¹ : Category.{u_7, u_3} H
inst✝ : Category.{u_6, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ whiskerLeft L e.hom = α'
⊢ F''.IsLeftKanExtension α' → F'.IsLeftKanExtension α

Tactic:
intro

Result:
case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{u_8, u_1} C
inst✝¹ : Category.{u_7, u_3} H
inst✝ : Category.{u_6, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ whiskerLeft L e.hom = α'
a✝ : F''.IsLeftKanExtension α'
⊢ F'.IsLeftKanExtension α

Proof state:
case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{u_8, u_1} C
inst✝¹ : Category.{u_7, u_3} H
inst✝ : Category.{u_6, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ whiskerLeft L e.hom = α'
a✝ : F''.IsLeftKanExtension α'
⊢ F'.IsLeftKanExtension α

Tactic:
refine isLeftKanExtension_of_iso e.symm α' α ?_

Result:
case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{u_8, u_1} C
inst✝¹ : Category.{u_7, u_3} H
inst✝ : Category.{u_6, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ whiskerLeft L e.hom = α'
a✝ : F''.IsLeftKanExtension α'
⊢ α' ≫ whiskerLeft L e.symm.hom = α