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₁
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₁
φ : CatCospanTransform F₁ G₁ F₂ G₂
τ : CatCospanTransform F₂ G₂ F₃ G₃
⊢ (transform X).map (α_ ψ φ τ).hom =
    (transformObjComp X (ψ.comp φ) τ).hom ≫
      whiskerRight (transformObjComp X ψ φ).hom ((transform X).obj τ) ≫
        (((transform X).obj ψ).associator ((transform X).obj φ) ((transform X).obj τ)).hom ≫
          ((transform X).obj ψ).whiskerLeft (transformObjComp X φ τ).inv ≫ (transformObjComp X ψ (φ.comp τ)).inv

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₁
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₁
φ : CatCospanTransform F₁ G₁ F₂ G₂
τ : CatCospanTransform F₂ G₂ F₃ G₃
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ (((transform X).map (α_ ψ φ τ).hom).app x✝¹).fst.app x✝ =
    (((transformObjComp X (ψ.comp φ) τ).hom ≫
                whiskerRight (transformObjComp X ψ φ).hom ((transform X).obj τ) ≫
                  (((transform X).obj ψ).associator ((transform X).obj φ) ((transform X).obj τ)).hom ≫
                    ((transform X).obj ψ).whiskerLeft (transformObjComp X φ τ).inv ≫
                      (transformObjComp X ψ (φ.comp τ)).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
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₁₃
inst✝ : Category.{v₁₃, u₁₃} X
ψ : CatCospanTransform F G F₁ G₁
φ : CatCospanTransform F₁ G₁ F₂ G₂
τ : CatCospanTransform F₂ G₂ F₃ G₃
x✝¹ : CatCommSqOver F G X
x✝ : X
⊢ (((transform X).map (α_ ψ φ τ).hom).app x✝¹).snd.app x✝ =
    (((transformObjComp X (ψ.comp φ) τ).hom ≫
                whiskerRight (transformObjComp X ψ φ).hom ((transform X).obj τ) ≫
                  (((transform X).obj ψ).associator ((transform X).obj φ) ((transform X).obj τ)).hom ≫
                    ((transform X).obj ψ).whiskerLeft (transformObjComp X φ τ).inv ≫
                      (transformObjComp X ψ (φ.comp τ)).inv).app
            x✝¹).snd.app
      x✝