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

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
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L e.hom ≫ α' = α
⊢ F''.IsRightKanExtension α' → F'.IsRightKanExtension α

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
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L e.hom ≫ α' = α
a✝ : F''.IsRightKanExtension α'
⊢ F'.IsRightKanExtension α

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
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L e.hom ≫ α' = α
a✝ : F''.IsRightKanExtension α'
⊢ F'.IsRightKanExtension α

Tactic:
refine isRightKanExtension_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
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L e.hom ≫ α' = α
a✝ : F''.IsRightKanExtension α'
⊢ whiskerLeft L e.symm.hom ≫ α = α'

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
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L e.hom ≫ α' = α
a✝ : F''.IsRightKanExtension α'
⊢ whiskerLeft L e.symm.hom ≫ α = α'

Tactic:
rw [← comm, ← whiskerLeft_comp_assoc, Iso.symm_hom, e.inv_hom_id, whiskerLeft_id', id_comp]

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
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L e.hom ≫ α' = α
a✝ : F'.IsRightKanExtension α
⊢ F''.IsRightKanExtension α'

Tactic:
exact isRightKanExtension_of_iso e α α' comm

Result:
no goals

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
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L e.hom ≫ α' = α
⊢ F'.IsRightKanExtension α ↔ F''.IsRightKanExtension α'

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
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L e.hom ≫ α' = α
⊢ F'.IsRightKanExtension α → F''.IsRightKanExtension α'

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
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L e.hom ≫ α' = α
⊢ F''.IsRightKanExtension α' → F'.IsRightKanExtension α

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
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L e.hom ≫ α' = α
⊢ F'.IsRightKanExtension α → F''.IsRightKanExtension α'

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
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L e.hom ≫ α' = α
a✝ : F'.IsRightKanExtension α
⊢ F''.IsRightKanExtension α'