-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.KanExtension.Preserves (goal)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_1} A
inst_1 : Category.{v_2, u_2} B
inst_2 : Category.{v_3, u_3} C
inst_3 : Category.{v_4, u_4} D
G : Functor.{v_2, v_4, u_2, u_4} B D
F_1 : Functor.{v_1, v_2, u_1, u_2} A B
L : Functor.{v_1, v_3, u_1, u_3} A C
inst_4 : G.PreservesLeftKanExtensions L
inst_5 : ∀ (F : Functor.{v_1, v_2, u_1, u_2} A B), L.HasLeftKanExtension F
inst_6 : ∀ (F : Functor.{v_1, v_4, u_1, u_4} A D), L.HasLeftKanExtension F
F F' : Functor.{v_1, v_2, u_1, u_2} A B
η : F ⟶ F'
⊢ Eq (α := F ⋙ G ⟶ L ⋙ L.leftKanExtension (F' ⋙ G))
    ((whiskerRight (L.leftKanExtensionUnit F) G ≫ (L.associator (L.leftKanExtension F) G).hom) ≫
        CategoryStruct.comp (Y := L ⋙ L.leftKanExtension F' ⋙ G)
          (L.whiskerLeft
            (whiskerRight
              ((L.leftKanExtension F).descOfIsLeftKanExtension (L.leftKanExtensionUnit F) (L.leftKanExtension F')
                (η ≫ L.leftKanExtensionUnit F'))
              G))
          (L.whiskerLeft (Iso.hom (G.leftKanExtensionCompIsoOfPreserves F' L))) :
      F ⋙ G ⟶ L ⋙ L.leftKanExtension (F' ⋙ G))
    ((whiskerRight (L.leftKanExtensionUnit F) G ≫ (L.associator (L.leftKanExtension F) G).hom) ≫
        CategoryStruct.comp (Y := L ⋙ L.leftKanExtension (F ⋙ G))
          (L.whiskerLeft (Iso.hom (G.leftKanExtensionCompIsoOfPreserves F L)) :
            L ⋙ L.leftKanExtension F ⋙ G ⟶ L ⋙ L.leftKanExtension (F ⋙ G))
          (L.whiskerLeft
              ((L.leftKanExtension (F ⋙ G)).descOfIsLeftKanExtension (L.leftKanExtensionUnit (F ⋙ G))
                (L.leftKanExtension (F' ⋙ G)) (whiskerRight η G ≫ L.leftKanExtensionUnit (F' ⋙ G))) :
            L ⋙ L.leftKanExtension (F ⋙ G) ⟶ L ⋙ L.leftKanExtension (F' ⋙ G)) :
      F ⋙ G ⟶ L ⋙ L.leftKanExtension (F' ⋙ G))
have hγ : ∀ (x : A),
  Eq (α := (F ⋙ G).obj x ⟶ (L ⋙ L.leftKanExtension (F' ⋙ G)).obj x)
    (NatTrans.app
        ((whiskerRight (L.leftKanExtensionUnit F) G ≫ (L.associator (L.leftKanExtension F) G).hom) ≫
          CategoryStruct.comp (Y := L ⋙ L.leftKanExtension F' ⋙ G)
            (L.whiskerLeft
              (whiskerRight
                ((L.leftKanExtension F).descOfIsLeftKanExtension (L.leftKanExtensionUnit F) (L.leftKanExtension F')
                  (η ≫ L.leftKanExtensionUnit F'))
                G))
            (L.whiskerLeft (Iso.hom (G.leftKanExtensionCompIsoOfPreserves F' L))))
        x :
      (F ⋙ G).obj x ⟶ (L ⋙ L.leftKanExtension (F' ⋙ G)).obj x)
    (NatTrans.app
        ((whiskerRight (L.leftKanExtensionUnit F) G ≫ (L.associator (L.leftKanExtension F) G).hom) ≫
          CategoryStruct.comp (Y := L ⋙ L.leftKanExtension (F ⋙ G))
            (L.whiskerLeft (Iso.hom (G.leftKanExtensionCompIsoOfPreserves F L)) :
              L ⋙ L.leftKanExtension F ⋙ G ⟶ L ⋙ L.leftKanExtension (F ⋙ G))
            (L.whiskerLeft
                ((L.leftKanExtension (F ⋙ G)).descOfIsLeftKanExtension (L.leftKanExtensionUnit (F ⋙ G))
                  (L.leftKanExtension (F' ⋙ G)) (whiskerRight η G ≫ L.leftKanExtensionUnit (F' ⋙ G))) :
              L ⋙ L.leftKanExtension (F ⋙ G) ⟶ L ⋙ L.leftKanExtension (F' ⋙ G)))
        x :
      (F ⋙ G).obj x ⟶ (L ⋙ L.leftKanExtension (F' ⋙ G)).obj x)
Tactic: ext