-- Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
lemma isRightKanExtension_iff_postcomp₁ (α : L' ⋙ F' ⟶ F) :
    F'.IsRightKanExtension α ↔ (G ⋙ F').IsRightKanExtension
      ((Functor.associator _ _ _).inv ≫ whiskerRight e.hom F' ≫ α)

Proof state:
case mp
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{u_7, u_1} C
inst✝³ : Category.{u_6, u_3} H
inst✝² : Category.{u_9, u_4} D
inst✝¹ : Category.{u_8, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
F' : D' ⥤ H
α : L' ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk (G ⋙ F') ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)) :=
  (RightExtension.isUniversalPostcomp₁Equiv G e F (RightExtension.mk F' α)).trans
    (IsTerminal.equivOfIso
      (CostructuredArrow.isoMk (Iso.refl ((RightExtension.postcomp₁ G e.hom F).obj (RightExtension.mk F' α)).left) ⋯))
⊢ F'.IsRightKanExtension α → (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)

Tactic:
exact fun _ => ⟨⟨eq (isUniversalOfIsRightKanExtension _ _)⟩⟩

Result:
no goals

Proof state:
case mpr
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{u_7, u_1} C
inst✝³ : Category.{u_6, u_3} H
inst✝² : Category.{u_9, u_4} D
inst✝¹ : Category.{u_8, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
F' : D' ⥤ H
α : L' ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk (G ⋙ F') ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)) :=
  (RightExtension.isUniversalPostcomp₁Equiv G e F (RightExtension.mk F' α)).trans
    (IsTerminal.equivOfIso
      (CostructuredArrow.isoMk (Iso.refl ((RightExtension.postcomp₁ G e.hom F).obj (RightExtension.mk F' α)).left) ⋯))
⊢ (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α) → F'.IsRightKanExtension α

Tactic:
exact fun _ => ⟨⟨eq.symm (isUniversalOfIsRightKanExtension _ _)⟩⟩

Result:
no goals

Proof state:
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{u_7, u_1} C
inst✝³ : Category.{u_6, u_3} H
inst✝² : Category.{u_9, u_4} D
inst✝¹ : Category.{u_8, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
F' : D' ⥤ H
α : L' ⋙ F' ⟶ F
⊢ F'.IsRightKanExtension α ↔ (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)

Tactic:
let eq : (RightExtension.mk _ α).IsUniversal ≃
  (RightExtension.mk _
    ((Functor.associator _ _ _).inv ≫ whiskerRight e.hom F' ≫ α)).IsUniversal :=
(RightExtension.isUniversalPostcomp₁Equiv G e F _).trans
  (IsTerminal.equivOfIso (CostructuredArrow.isoMk (Iso.refl _)))

Result:
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{u_7, u_1} C
inst✝³ : Category.{u_6, u_3} H
inst✝² : Category.{u_9, u_4} D
inst✝¹ : Category.{u_8, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
F' : D' ⥤ H
α : L' ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk (G ⋙ F') ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)) :=
  (RightExtension.isUniversalPostcomp₁Equiv G e F (RightExtension.mk F' α)).trans
    (IsTerminal.equivOfIso
      (CostructuredArrow.isoMk (Iso.refl ((RightExtension.postcomp₁ G e.hom F).obj (RightExtension.mk F' α)).left) ⋯))
⊢ F'.IsRightKanExtension α ↔ (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)

Proof state:
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{u_7, u_1} C
inst✝³ : Category.{u_6, u_3} H
inst✝² : Category.{u_9, u_4} D
inst✝¹ : Category.{u_8, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
F' : D' ⥤ H
α : L' ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk (G ⋙ F') ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)) :=
  (RightExtension.isUniversalPostcomp₁Equiv G e F (RightExtension.mk F' α)).trans
    (IsTerminal.equivOfIso
      (CostructuredArrow.isoMk (Iso.refl ((RightExtension.postcomp₁ G e.hom F).obj (RightExtension.mk F' α)).left) ⋯))
⊢ F'.IsRightKanExtension α ↔ (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)

Tactic:
constructor

Result:
case mp
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{u_7, u_1} C
inst✝³ : Category.{u_6, u_3} H
inst✝² : Category.{u_9, u_4} D
inst✝¹ : Category.{u_8, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
F' : D' ⥤ H
α : L' ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk (G ⋙ F') ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)) :=
  (RightExtension.isUniversalPostcomp₁Equiv G e F (RightExtension.mk F' α)).trans
    (IsTerminal.equivOfIso
      (CostructuredArrow.isoMk (Iso.refl ((RightExtension.postcomp₁ G e.hom F).obj (RightExtension.mk F' α)).left) ⋯))
⊢ F'.IsRightKanExtension α → (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)

case mpr
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{u_7, u_1} C
inst✝³ : Category.{u_6, u_3} H
inst✝² : Category.{u_9, u_4} D
inst✝¹ : Category.{u_8, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
F' : D' ⥤ H
α : L' ⋙ F' ⟶ F
eq : CostructuredArrow.IsUniversal (RightExtension.mk F' α) ≃
  CostructuredArrow.IsUniversal (RightExtension.mk (G ⋙ F') ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α)) :=
  (RightExtension.isUniversalPostcomp₁Equiv G e F (RightExtension.mk F' α)).trans
    (IsTerminal.equivOfIso
      (CostructuredArrow.isoMk (Iso.refl ((RightExtension.postcomp₁ G e.hom F).obj (RightExtension.mk F' α)).left) ⋯))
⊢ (G ⋙ F').IsRightKanExtension ((L.associator G F').inv ≫ whiskerRight e.hom F' ≫ α) → F'.IsRightKanExtension α