-- Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
lemma isRightKanExtension_iff_isIso {F' : D ⥤ H} {F'' : D ⥤ H} (φ : F'' ⟶ F')
    {L : C ⥤ D} {F : C ⥤ H} (α : L ⋙ F' ⟶ F) (α' : L ⋙ F'' ⟶ F)
    (comm : whiskerLeft L φ ≫ α = α') [F'.IsRightKanExtension α] :
    F''.IsRightKanExtension α' ↔ IsIso φ

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
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
⊢ F''.IsRightKanExtension α' ↔ IsIso φ

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
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
⊢ F''.IsRightKanExtension α' → IsIso φ

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
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
⊢ IsIso φ → 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
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
a✝ : IsIso φ
⊢ F'.IsRightKanExtension α

Tactic:
infer_instance

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
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
a✝ : F''.IsRightKanExtension α'
⊢ IsIso (F''.rightKanExtensionUnique α' F' α).hom

Tactic:
infer_instance

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
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
a✝ : F''.IsRightKanExtension α'
⊢ whiskerLeft L φ ≫ α = whiskerLeft L (F''.rightKanExtensionUnique α' F' α).hom ≫ α

Tactic:
simp [comm]

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
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
a✝ : F''.IsRightKanExtension α'
⊢ IsIso φ

Tactic:
rw [F'.hom_ext_of_isRightKanExtension α φ (rightKanExtensionUnique _ α' _ α).hom
  (by simp [comm])]

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
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
a✝ : F''.IsRightKanExtension α'
⊢ IsIso (F''.rightKanExtensionUnique α' F' α).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
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
a✝ : IsIso φ
⊢ F''.IsRightKanExtension α'

Tactic:
rw [isRightKanExtension_iff_of_iso (asIso φ) α' α comm]

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
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
a✝ : IsIso φ
⊢ 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
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
⊢ F''.IsRightKanExtension α' → IsIso φ

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
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
a✝ : F''.IsRightKanExtension α'
⊢ IsIso φ

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
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
⊢ IsIso φ → 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
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : whiskerLeft L φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
a✝ : IsIso φ
⊢ F''.IsRightKanExtension α'