Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst✝³ : Category.{v₄, u₄} A₁
inst✝² : Category.{v₅, u₅} B₁
inst✝¹ : Category.{v₆, u₆} C₁
F₁ : A₁ ⥤ B₁
G₁ : C₁ ⥤ B₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ ψ' : CatCospanTransform F G F₁ G₁
η : ψ ⟶ ψ'
S : CatCommSqOver F G X
t : X
⊢ (whiskerRight { app := fun y ↦ η.left.app (S.fst.obj y), naturality := ⋯ } F₁ ≫
          ({
                    obj := fun S ↦
                      { fst := S.fst ⋙ ψ'.left, snd := S.snd ⋙ ψ'.right,
                        iso :=
                          S.fst.associator ψ'.left F₁ ≪≫
                            S.fst.isoWhiskerLeft (CatCommSq.iso F ψ'.left ψ'.base F₁).symm ≪≫
                              (S.fst.associator F ψ'.base).symm ≪≫
                                isoWhiskerRight S.iso ψ'.base ≪≫
                                  S.snd.associator G ψ'.base ≪≫
                                    S.snd.isoWhiskerLeft (CatCommSq.iso G ψ'.right ψ'.base G₁) ≪≫
                                      (S.snd.associator ψ'.right G₁).symm },
                    map := fun {x y} f ↦
                      { fst := whiskerRight f.fst ψ'.left, snd := whiskerRight f.snd ψ'.right, w := ⋯ },
                    map_id := ⋯, map_comp := ⋯ }.obj
                S).iso.hom).app
      t =
    (({
                    obj := fun S ↦
                      { fst := S.fst ⋙ ψ.left, snd := S.snd ⋙ ψ.right,
                        iso :=
                          S.fst.associator ψ.left F₁ ≪≫
                            S.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                              (S.fst.associator F ψ.base).symm ≪≫
                                isoWhiskerRight S.iso ψ.base ≪≫
                                  S.snd.associator G ψ.base ≪≫
                                    S.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                                      (S.snd.associator ψ.right G₁).symm },
                    map := fun {x y} f ↦
                      { fst := whiskerRight f.fst ψ.left, snd := whiskerRight f.snd ψ.right, w := ⋯ },
                    map_id := ⋯, map_comp := ⋯ }.obj
                S).iso.hom ≫
          whiskerRight { app := fun y ↦ η.right.app (S.snd.obj y), naturality := ⋯ } G₁).app
      t

Tactic:
have := ψ.squareLeft.iso.inv.app (S.fst.obj t) ≫=
            η.left_coherence_app (S.fst.obj t)

Goal state after:
A : Type u₁
B : Type u₂
C : Type u₃
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst✝³ : Category.{v₄, u₄} A₁
inst✝² : Category.{v₅, u₅} B₁
inst✝¹ : Category.{v₆, u₆} C₁
F₁ : A₁ ⥤ B₁
G₁ : C₁ ⥤ B₁
X : Type u₇
inst✝ : Category.{v₇, u₇} X
ψ ψ' : CatCospanTransform F G F₁ G₁
η : ψ ⟶ ψ'
S : CatCommSqOver F G X
t : X
this :
  (CatCommSq.iso F ψ.left ψ.base F₁).inv.app (S.fst.obj t) ≫
      (CatCommSq.iso F ψ.left ψ.base F₁).hom.app (S.fst.obj t) ≫ F₁.map (η.left.app (S.fst.obj t)) =
    (CatCommSq.iso F ψ.left ψ.base F₁).inv.app (S.fst.obj t) ≫
      η.base.app (F.obj (S.fst.obj t)) ≫ (CatCommSq.iso F ψ'.left ψ'.base F₁).hom.app (S.fst.obj t)
⊢ (whiskerRight { app := fun y ↦ η.left.app (S.fst.obj y), naturality := ⋯ } F₁ ≫
          ({
                    obj := fun S ↦
                      { fst := S.fst ⋙ ψ'.left, snd := S.snd ⋙ ψ'.right,
                        iso :=
                          S.fst.associator ψ'.left F₁ ≪≫
                            S.fst.isoWhiskerLeft (CatCommSq.iso F ψ'.left ψ'.base F₁).symm ≪≫
                              (S.fst.associator F ψ'.base).symm ≪≫
                                isoWhiskerRight S.iso ψ'.base ≪≫
                                  S.snd.associator G ψ'.base ≪≫
                                    S.snd.isoWhiskerLeft (CatCommSq.iso G ψ'.right ψ'.base G₁) ≪≫
                                      (S.snd.associator ψ'.right G₁).symm },
                    map := fun {x y} f ↦
                      { fst := whiskerRight f.fst ψ'.left, snd := whiskerRight f.snd ψ'.right, w := ⋯ },
                    map_id := ⋯, map_comp := ⋯ }.obj
                S).iso.hom).app
      t =
    (({
                    obj := fun S ↦
                      { fst := S.fst ⋙ ψ.left, snd := S.snd ⋙ ψ.right,
                        iso :=
                          S.fst.associator ψ.left F₁ ≪≫
                            S.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                              (S.fst.associator F ψ.base).symm ≪≫
                                isoWhiskerRight S.iso ψ.base ≪≫
                                  S.snd.associator G ψ.base ≪≫
                                    S.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                                      (S.snd.associator ψ.right G₁).symm },
                    map := fun {x y} f ↦
                      { fst := whiskerRight f.fst ψ.left, snd := whiskerRight f.snd ψ.right, w := ⋯ },
                    map_id := ⋯, map_comp := ⋯ }.obj
                S).iso.hom ≫
          whiskerRight { app := fun y ↦ η.right.app (S.snd.obj y), naturality := ⋯ } G₁).app
      t