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
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₁₁
inst✝¹ : Category.{v₁₀, u₁₀} X
inst✝ : Category.{v₁₁, u₁₁} Y
U : X ⥤ Y
ψ : CatCospanTransform F G F₁ G₁
ψ' : CatCospanTransform F₁ G₁ F₂ G₂
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((CatCommSq.iso ((transform Y).obj (ψ.comp ψ')) ((precompose F G).obj U) ((precompose F₂ G₂).obj U)
                    ((transform X).obj (ψ.comp ψ'))).hom ≫
                ((precompose F G).obj U).whiskerLeft (transformObjComp X ψ ψ').hom).app
            x✝¹).fst.app
      x✝ =
    ((whiskerRight (transformObjComp Y ψ ψ').hom ((precompose F₂ G₂).obj U) ≫
                (((transform Y).obj ψ).associator ((transform Y).obj ψ') ((precompose F₂ G₂).obj U)).hom ≫
                  ((transform Y).obj ψ).whiskerLeft
                      (CatCommSq.iso ((transform Y).obj ψ') ((precompose F₁ G₁).obj U) ((precompose F₂ G₂).obj U)
                          ((transform X).obj ψ')).hom ≫
                    (((transform Y).obj ψ).associator ((precompose F₁ G₁).obj U) ((transform X).obj ψ')).inv ≫
                      whiskerRight
                          (CatCommSq.iso ((transform Y).obj ψ) ((precompose F G).obj U) ((precompose F₁ G₁).obj U)
                              ((transform X).obj ψ)).hom
                          ((transform X).obj ψ') ≫
                        (((precompose F G).obj U).associator ((transform X).obj ψ) ((transform X).obj ψ')).hom).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
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₁₁
inst✝¹ : Category.{v₁₀, u₁₀} X
inst✝ : Category.{v₁₁, u₁₁} Y
U : X ⥤ Y
ψ : CatCospanTransform F G F₁ G₁
ψ' : CatCospanTransform F₁ G₁ F₂ G₂
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((CatCommSq.iso ((transform Y).obj (ψ.comp ψ')) ((precompose F G).obj U) ((precompose F₂ G₂).obj U)
                    ((transform X).obj (ψ.comp ψ'))).hom ≫
                ((precompose F G).obj U).whiskerLeft (transformObjComp X ψ ψ').hom).app
            x✝¹).snd.app
      x✝ =
    ((whiskerRight (transformObjComp Y ψ ψ').hom ((precompose F₂ G₂).obj U) ≫
                (((transform Y).obj ψ).associator ((transform Y).obj ψ') ((precompose F₂ G₂).obj U)).hom ≫
                  ((transform Y).obj ψ).whiskerLeft
                      (CatCommSq.iso ((transform Y).obj ψ') ((precompose F₁ G₁).obj U) ((precompose F₂ G₂).obj U)
                          ((transform X).obj ψ')).hom ≫
                    (((transform Y).obj ψ).associator ((precompose F₁ G₁).obj U) ((transform X).obj ψ')).inv ≫
                      whiskerRight
                          (CatCommSq.iso ((transform Y).obj ψ) ((precompose F G).obj U) ((precompose F₁ G₁).obj U)
                              ((transform X).obj ψ)).hom
                          ((transform X).obj ψ') ≫
                        (((precompose F G).obj U).associator ((transform X).obj ψ) ((transform X).obj ψ')).hom).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
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₁₁
inst✝¹ : Category.{v₁₀, u₁₀} X
inst✝ : Category.{v₁₁, u₁₁} Y
U : X ⥤ Y
ψ : CatCospanTransform F G F₁ G₁
ψ' : CatCospanTransform F₁ G₁ F₂ G₂
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((CatCommSq.iso ((transform Y).obj (ψ.comp ψ')) ((precompose F G).obj U) ((precompose F₂ G₂).obj U)
                    ((transform X).obj (ψ.comp ψ'))).hom ≫
                ((precompose F G).obj U).whiskerLeft (transformObjComp X ψ ψ').hom).app
            x✝¹).fst.app
      x✝ =
    ((whiskerRight (transformObjComp Y ψ ψ').hom ((precompose F₂ G₂).obj U) ≫
                (((transform Y).obj ψ).associator ((transform Y).obj ψ') ((precompose F₂ G₂).obj U)).hom ≫
                  ((transform Y).obj ψ).whiskerLeft
                      (CatCommSq.iso ((transform Y).obj ψ') ((precompose F₁ G₁).obj U) ((precompose F₂ G₂).obj U)
                          ((transform X).obj ψ')).hom ≫
                    (((transform Y).obj ψ).associator ((precompose F₁ G₁).obj U) ((transform X).obj ψ')).inv ≫
                      whiskerRight
                          (CatCommSq.iso ((transform Y).obj ψ) ((precompose F G).obj U) ((precompose F₁ G₁).obj U)
                              ((transform X).obj ψ)).hom
                          ((transform X).obj ψ') ≫
                        (((precompose F G).obj U).associator ((transform X).obj ψ) ((transform X).obj ψ')).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₁
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₁₁
inst✝¹ : Category.{v₁₀, u₁₀} X
inst✝ : Category.{v₁₁, u₁₁} Y
U : X ⥤ Y
ψ : CatCospanTransform F G F₁ G₁
ψ' : CatCospanTransform F₁ G₁ F₂ G₂
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((CatCommSq.iso ((transform Y).obj (ψ.comp ψ')) ((precompose F G).obj U) ((precompose F₂ G₂).obj U)
                    ((transform X).obj (ψ.comp ψ'))).hom ≫
                ((precompose F G).obj U).whiskerLeft (transformObjComp X ψ ψ').hom).app
            x✝¹).snd.app
      x✝ =
    ((whiskerRight (transformObjComp Y ψ ψ').hom ((precompose F₂ G₂).obj U) ≫
                (((transform Y).obj ψ).associator ((transform Y).obj ψ') ((precompose F₂ G₂).obj U)).hom ≫
                  ((transform Y).obj ψ).whiskerLeft
                      (CatCommSq.iso ((transform Y).obj ψ') ((precompose F₁ G₁).obj U) ((precompose F₂ G₂).obj U)
                          ((transform X).obj ψ')).hom ≫
                    (((transform Y).obj ψ).associator ((precompose F₁ G₁).obj U) ((transform X).obj ψ')).inv ≫
                      whiskerRight
                          (CatCommSq.iso ((transform Y).obj ψ) ((precompose F G).obj U) ((precompose F₁ G₁).obj U)
                              ((transform X).obj ψ)).hom
                          ((transform X).obj ψ') ≫
                        (((precompose F G).obj U).associator ((transform X).obj ψ) ((transform X).obj ψ')).hom).app
            x✝¹).snd.app
      x✝