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₇
Y : Type u₈
Z : Type u₉
inst✝² : Category.{v₇, u₇} X
inst✝¹ : Category.{v₈, u₈} Y
inst✝ : Category.{v₉, u₉} Z
ψ : CatCospanTransform F G F₁ G₁
U : X ⥤ Y
V : Y ⥤ Z
⊢ (CatCommSq.iso ((precompose F G).obj (U ⋙ V)) ((transform Z).obj ψ) ((transform X).obj ψ)
          ((precompose F₁ G₁).obj (U ⋙ V))).hom ≫
      ((transform Z).obj ψ).whiskerLeft (precomposeObjComp F₁ G₁ U V).hom =
    whiskerRight (precomposeObjComp F G U V).hom ((transform X).obj ψ) ≫
      (((precompose F G).obj V).associator ((precompose F G).obj U) ((transform X).obj ψ)).hom ≫
        ((precompose F G).obj V).whiskerLeft
            (CatCommSq.iso ((precompose F G).obj U) ((transform Y).obj ψ) ((transform X).obj ψ)
                ((precompose F₁ G₁).obj U)).hom ≫
          (((precompose F G).obj V).associator ((transform Y).obj ψ) ((precompose F₁ G₁).obj U)).inv ≫
            whiskerRight
                (CatCommSq.iso ((precompose F G).obj V) ((transform Z).obj ψ) ((transform Y).obj ψ)
                    ((precompose F₁ G₁).obj V)).hom
                ((precompose F₁ G₁).obj U) ≫
              (((transform Z).obj ψ).associator ((precompose F₁ G₁).obj V) ((precompose F₁ G₁).obj U)).hom

Tactic:
ext

Goal state after:
case h₁
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₇
Y : Type u₈
Z : Type u₉
inst✝² : Category.{v₇, u₇} X
inst✝¹ : Category.{v₈, u₈} Y
inst✝ : Category.{v₉, u₉} Z
ψ : CatCospanTransform F G F₁ G₁
U : X ⥤ Y
V : Y ⥤ Z
x✝¹ : CatCommSqOver F G Z
x✝ : X
⊢ (((CatCommSq.iso ((precompose F G).obj (U ⋙ V)) ((transform Z).obj ψ) ((transform X).obj ψ)
                    ((precompose F₁ G₁).obj (U ⋙ V))).hom ≫
                ((transform Z).obj ψ).whiskerLeft (precomposeObjComp F₁ G₁ U V).hom).app
            x✝¹).fst.app
      x✝ =
    ((whiskerRight (precomposeObjComp F G U V).hom ((transform X).obj ψ) ≫
                (((precompose F G).obj V).associator ((precompose F G).obj U) ((transform X).obj ψ)).hom ≫
                  ((precompose F G).obj V).whiskerLeft
                      (CatCommSq.iso ((precompose F G).obj U) ((transform Y).obj ψ) ((transform X).obj ψ)
                          ((precompose F₁ G₁).obj U)).hom ≫
                    (((precompose F G).obj V).associator ((transform Y).obj ψ) ((precompose F₁ G₁).obj U)).inv ≫
                      whiskerRight
                          (CatCommSq.iso ((precompose F G).obj V) ((transform Z).obj ψ) ((transform Y).obj ψ)
                              ((precompose F₁ G₁).obj V)).hom
                          ((precompose F₁ G₁).obj U) ≫
                        (((transform Z).obj ψ).associator ((precompose F₁ G₁).obj V)
                            ((precompose F₁ G₁).obj U)).hom).app
            x✝¹).fst.app
      x✝

case h₂
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₇
Y : Type u₈
Z : Type u₉
inst✝² : Category.{v₇, u₇} X
inst✝¹ : Category.{v₈, u₈} Y
inst✝ : Category.{v₉, u₉} Z
ψ : CatCospanTransform F G F₁ G₁
U : X ⥤ Y
V : Y ⥤ Z
x✝¹ : CatCommSqOver F G Z
x✝ : X
⊢ (((CatCommSq.iso ((precompose F G).obj (U ⋙ V)) ((transform Z).obj ψ) ((transform X).obj ψ)
                    ((precompose F₁ G₁).obj (U ⋙ V))).hom ≫
                ((transform Z).obj ψ).whiskerLeft (precomposeObjComp F₁ G₁ U V).hom).app
            x✝¹).snd.app
      x✝ =
    ((whiskerRight (precomposeObjComp F G U V).hom ((transform X).obj ψ) ≫
                (((precompose F G).obj V).associator ((precompose F G).obj U) ((transform X).obj ψ)).hom ≫
                  ((precompose F G).obj V).whiskerLeft
                      (CatCommSq.iso ((precompose F G).obj U) ((transform Y).obj ψ) ((transform X).obj ψ)
                          ((precompose F₁ G₁).obj U)).hom ≫
                    (((precompose F G).obj V).associator ((transform Y).obj ψ) ((precompose F₁ G₁).obj U)).inv ≫
                      whiskerRight
                          (CatCommSq.iso ((precompose F G).obj V) ((transform Z).obj ψ) ((transform Y).obj ψ)
                              ((precompose F₁ G₁).obj V)).hom
                          ((precompose F₁ G₁).obj U) ≫
                        (((transform Z).obj ψ).associator ((precompose F₁ G₁).obj V)
                            ((precompose F₁ G₁).obj U)).hom).app
            x✝¹).snd.app
      x✝