-- Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
lemma isLeftKanExtension_iff_of_iso₂ {F₁' F₂' : D ⥤ H} (α₁ : F₁ ⟶ L ⋙ F₁') (α₂ : F₂ ⟶ L ⋙ F₂')
    (e : F₁ ≅ F₂) (e' : F₁' ≅ F₂') (h : α₁ ≫ whiskerLeft L e'.hom = e.hom ≫ α₂) :
    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
L : C ⥤ D
F₁ F₂ : C ⥤ H
F₁' F₂' : D ⥤ H
α₁ : F₁ ⟶ L ⋙ F₁'
α₂ : F₂ ⟶ L ⋙ F₂'
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : α₁ ≫ whiskerLeft L e'.hom = e.hom ≫ α₂
⊢ F₁'.IsLeftKanExtension α₁ ↔ F₂'.IsLeftKanExtension α₂

Tactic:
let eq := LeftExtension.isUniversalEquivOfIso₂ (LeftExtension.mk _ α₁)
  (LeftExtension.mk _ α₂) e e' h

Result:
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
L : C ⥤ D
F₁ F₂ : C ⥤ H
F₁' F₂' : D ⥤ H
α₁ : F₁ ⟶ L ⋙ F₁'
α₂ : F₂ ⟶ L ⋙ F₂'
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : α₁ ≫ whiskerLeft L e'.hom = e.hom ≫ α₂
eq : StructuredArrow.IsUniversal (LeftExtension.mk F₁' α₁) ≃ StructuredArrow.IsUniversal (LeftExtension.mk F₂' α₂) :=
  (LeftExtension.mk F₁' α₁).isUniversalEquivOfIso₂ (LeftExtension.mk F₂' α₂) e e' h
⊢ 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
L : C ⥤ D
F₁ F₂ : C ⥤ H
F₁' F₂' : D ⥤ H
α₁ : F₁ ⟶ L ⋙ F₁'
α₂ : F₂ ⟶ L ⋙ F₂'
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : α₁ ≫ whiskerLeft L e'.hom = e.hom ≫ α₂
eq : StructuredArrow.IsUniversal (LeftExtension.mk F₁' α₁) ≃ StructuredArrow.IsUniversal (LeftExtension.mk F₂' α₂) :=
  (LeftExtension.mk F₁' α₁).isUniversalEquivOfIso₂ (LeftExtension.mk F₂' α₂) e e' h
⊢ F₁'.IsLeftKanExtension α₁ → F₂'.IsLeftKanExtension α₂

Tactic:
exact fun _ => ⟨⟨eq.1 (isUniversalOfIsLeftKanExtension F₁' α₁)⟩⟩

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
L : C ⥤ D
F₁ F₂ : C ⥤ H
F₁' F₂' : D ⥤ H
α₁ : F₁ ⟶ L ⋙ F₁'
α₂ : F₂ ⟶ L ⋙ F₂'
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : α₁ ≫ whiskerLeft L e'.hom = e.hom ≫ α₂
eq : StructuredArrow.IsUniversal (LeftExtension.mk F₁' α₁) ≃ StructuredArrow.IsUniversal (LeftExtension.mk F₂' α₂) :=
  (LeftExtension.mk F₁' α₁).isUniversalEquivOfIso₂ (LeftExtension.mk F₂' α₂) e e' h
⊢ 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
L : C ⥤ D
F₁ F₂ : C ⥤ H
F₁' F₂' : D ⥤ H
α₁ : F₁ ⟶ L ⋙ F₁'
α₂ : F₂ ⟶ L ⋙ F₂'
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : α₁ ≫ whiskerLeft L e'.hom = e.hom ≫ α₂
eq : StructuredArrow.IsUniversal (LeftExtension.mk F₁' α₁) ≃ StructuredArrow.IsUniversal (LeftExtension.mk F₂' α₂) :=
  (LeftExtension.mk F₁' α₁).isUniversalEquivOfIso₂ (LeftExtension.mk F₂' α₂) e e' h
⊢ 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
L : C ⥤ D
F₁ F₂ : C ⥤ H
F₁' F₂' : D ⥤ H
α₁ : F₁ ⟶ L ⋙ F₁'
α₂ : F₂ ⟶ L ⋙ F₂'
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : α₁ ≫ whiskerLeft L e'.hom = e.hom ≫ α₂
eq : StructuredArrow.IsUniversal (LeftExtension.mk F₁' α₁) ≃ StructuredArrow.IsUniversal (LeftExtension.mk F₂' α₂) :=
  (LeftExtension.mk F₁' α₁).isUniversalEquivOfIso₂ (LeftExtension.mk F₂' α₂) e e' h
⊢ 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
L : C ⥤ D
F₁ F₂ : C ⥤ H
F₁' F₂' : D ⥤ H
α₁ : F₁ ⟶ L ⋙ F₁'
α₂ : F₂ ⟶ L ⋙ F₂'
e : F₁ ≅ F₂
e' : F₁' ≅ F₂'
h : α₁ ≫ whiskerLeft L e'.hom = e.hom ≫ α₂
eq : StructuredArrow.IsUniversal (LeftExtension.mk F₁' α₁) ≃ StructuredArrow.IsUniversal (LeftExtension.mk F₂' α₂) :=
  (LeftExtension.mk F₁' α₁).isUniversalEquivOfIso₂ (LeftExtension.mk F₂' α₂) e e' h
⊢ F₂'.IsLeftKanExtension α₂ → F₁'.IsLeftKanExtension α₁

Tactic:
exact fun _ => ⟨⟨eq.2 (isUniversalOfIsLeftKanExtension F₂' α₂)⟩⟩

Result:
no goals