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

Goal state before:
pp: 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
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝³ : Category.{v₄, u₄} X
inst✝² : Category.{v₅, u₅} Y
inst✝¹ : Category.{v₆, u₆} Z
T : Type u₇
inst✝ : Category.{v₇, u₇} T
U : X ⥤ Y
V : Y ⥤ Z
W : Z ⥤ T
x✝¹ : CatCommSqOver F G T
x✝ : X
⊢ (((precompose F G).map (U.associator V W).hom).app x✝¹).fst.app x✝ =
    (((precomposeObjComp F G (U ⋙ V) W).hom ≫
                ((precompose F G).obj W).whiskerLeft (precomposeObjComp F G U V).hom ≫
                  (((precompose F G).obj W).associator ((precompose F G).obj V) ((precompose F G).obj U)).inv ≫
                    whiskerRight (precomposeObjComp F G V W).inv ((precompose F G).obj U) ≫
                      (precomposeObjComp F G U (V ⋙ W)).inv).app
            x✝¹).fst.app
      x✝

pp: 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
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝³ : Category.{v₄, u₄} X
inst✝² : Category.{v₅, u₅} Y
inst✝¹ : Category.{v₆, u₆} Z
T : Type u₇
inst✝ : Category.{v₇, u₇} T
U : X ⥤ Y
V : Y ⥤ Z
W : Z ⥤ T
x✝¹ : CatCommSqOver F G T
x✝ : X
⊢ (((precompose F G).map (U.associator V W).hom).app x✝¹).snd.app x✝ =
    (((precomposeObjComp F G (U ⋙ V) W).hom ≫
                ((precompose F G).obj W).whiskerLeft (precomposeObjComp F G U V).hom ≫
                  (((precompose F G).obj W).associator ((precompose F G).obj V) ((precompose F G).obj U)).inv ≫
                    whiskerRight (precomposeObjComp F G V W).inv ((precompose F G).obj U) ≫
                      (precomposeObjComp F G U (V ⋙ W)).inv).app
            x✝¹).snd.app
      x✝

Tactic:
<;>

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
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝³ : Category.{v₄, u₄} X
inst✝² : Category.{v₅, u₅} Y
inst✝¹ : Category.{v₆, u₆} Z
T : Type u₇
inst✝ : Category.{v₇, u₇} T
U : X ⥤ Y
V : Y ⥤ Z
W : Z ⥤ T
x✝¹ : CatCommSqOver F G T
x✝ : X
⊢ (((precompose F G).map (U.associator V W).hom).app x✝¹).fst.app x✝ =
    (((precomposeObjComp F G (U ⋙ V) W).hom ≫
                ((precompose F G).obj W).whiskerLeft (precomposeObjComp F G U V).hom ≫
                  (((precompose F G).obj W).associator ((precompose F G).obj V) ((precompose F G).obj U)).inv ≫
                    whiskerRight (precomposeObjComp F G V W).inv ((precompose F G).obj U) ≫
                      (precomposeObjComp F G U (V ⋙ W)).inv).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
X : Type u₄
Y : Type u₅
Z : Type u₆
inst✝³ : Category.{v₄, u₄} X
inst✝² : Category.{v₅, u₅} Y
inst✝¹ : Category.{v₆, u₆} Z
T : Type u₇
inst✝ : Category.{v₇, u₇} T
U : X ⥤ Y
V : Y ⥤ Z
W : Z ⥤ T
x✝¹ : CatCommSqOver F G T
x✝ : X
⊢ (((precompose F G).map (U.associator V W).hom).app x✝¹).snd.app x✝ =
    (((precomposeObjComp F G (U ⋙ V) W).hom ≫
                ((precompose F G).obj W).whiskerLeft (precomposeObjComp F G U V).hom ≫
                  (((precompose F G).obj W).associator ((precompose F G).obj V) ((precompose F G).obj U)).inv ≫
                    whiskerRight (precomposeObjComp F G V W).inv ((precompose F G).obj U) ≫
                      (precomposeObjComp F G U (V ⋙ W)).inv).app
            x✝¹).snd.app
      x✝