Module: Mathlib.Topology.Sheaves.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens ↑X
j : CostructuredArrow (Opens.map f).op (op U)
⊢ ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op U)).ι.app
        j ≫
      ((pullback C f).map u).app (op U) ≫
        (Limits.IsColimit.coconePointUniqueUpToIso
            ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit 𝒢 (op U))
            (Limits.colimitOfDiagramTerminal
              { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
              (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ 𝒢))).hom =
    ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op U)).ι.app
        j ≫
      (Limits.IsColimit.coconePointUniqueUpToIso
            ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op U))
            (Limits.colimitOfDiagramTerminal
              { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
              (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ))).hom ≫
        u.app (op (hf.functor.obj U))

Tactic:
have eq : ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ)
      ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt (op U)).ι.app j
      ≫ ((pullback C f).map u).app (op U) = NatTrans.app (Functor.whiskerLeft _ u) j ≫
      ((LeftExtension.mk ((Opens.map f).op.leftKanExtension 𝒢)
      ((Opens.map f).op.leftKanExtensionUnit 𝒢)).coconeAt (op U)).ι.app j := by
    dsimp [pullback]
    simp only [Category.assoc, NatTrans.naturality]
    have := NatTrans.congr_app ((Opens.map f).op.lanUnit.naturality u) j.left
    dsimp [lanUnit] at this
    rw [reassoc_of% this]
    rfl

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasColimits C
X Y : TopCat
f : X ⟶ Y
hf : IsOpenMap ⇑(ConcreteCategory.hom f)
ℱ 𝒢 : TopCat.Presheaf C Y
u : ℱ ⟶ 𝒢
U : Opens ↑X
j : CostructuredArrow (Opens.map f).op (op U)
eq :
  ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op U)).ι.app
        j ≫
      ((pullback C f).map u).app (op U) =
    ((CostructuredArrow.proj (Opens.map f).op (op U)).whiskerLeft u).app j ≫
      ((LeftExtension.mk ((Opens.map f).op.leftKanExtension 𝒢) ((Opens.map f).op.leftKanExtensionUnit 𝒢)).coconeAt
              (op U)).ι.app
        j
⊢ ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op U)).ι.app
        j ≫
      ((pullback C f).map u).app (op U) ≫
        (Limits.IsColimit.coconePointUniqueUpToIso
            ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit 𝒢 (op U))
            (Limits.colimitOfDiagramTerminal
              { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
              (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ 𝒢))).hom =
    ((LeftExtension.mk ((Opens.map f).op.leftKanExtension ℱ) ((Opens.map f).op.leftKanExtensionUnit ℱ)).coconeAt
              (op U)).ι.app
        j ≫
      (Limits.IsColimit.coconePointUniqueUpToIso
            ((Opens.map f).op.isPointwiseLeftKanExtensionLeftKanExtensionUnit ℱ (op U))
            (Limits.colimitOfDiagramTerminal
              { lift := fun s ↦ CostructuredArrow.homMk (homOfLE ⋯).op ⋯, fac := ⋯, uniq := ⋯ }
              (CostructuredArrow.proj (Opens.map f).op (op U) ⋙ ℱ))).hom ≫
        u.app (op (hf.functor.obj U))