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
X : Type u₇
Y : Type u₈
inst✝¹ : Category.{v₇, u₇} X
inst✝ : Category.{v₈, u₈} Y
U : X ⥤ Y
F : A ⥤ B
G : C ⥤ B
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((CatCommSq.iso ((transform Y).obj (CatCospanTransform.id F G)) ((precompose F G).obj U) ((precompose F G).obj U)
                    ((transform X).obj (CatCospanTransform.id F G))).hom ≫
                ((precompose F G).obj U).whiskerLeft (transformObjId X F G).hom).app
            x✝¹).fst.app
      x✝ =
    ((whiskerRight (transformObjId Y F G).hom ((precompose F G).obj U) ≫
                ((precompose F G).obj U).leftUnitor.hom ≫ ((precompose F G).obj U).rightUnitor.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
X : Type u₇
Y : Type u₈
inst✝¹ : Category.{v₇, u₇} X
inst✝ : Category.{v₈, u₈} Y
U : X ⥤ Y
F : A ⥤ B
G : C ⥤ B
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((CatCommSq.iso ((transform Y).obj (CatCospanTransform.id F G)) ((precompose F G).obj U) ((precompose F G).obj U)
                    ((transform X).obj (CatCospanTransform.id F G))).hom ≫
                ((precompose F G).obj U).whiskerLeft (transformObjId X F G).hom).app
            x✝¹).snd.app
      x✝ =
    ((whiskerRight (transformObjId Y F G).hom ((precompose F G).obj U) ≫
                ((precompose F G).obj U).leftUnitor.hom ≫ ((precompose F G).obj U).rightUnitor.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
X : Type u₇
Y : Type u₈
inst✝¹ : Category.{v₇, u₇} X
inst✝ : Category.{v₈, u₈} Y
U : X ⥤ Y
F : A ⥤ B
G : C ⥤ B
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((CatCommSq.iso ((transform Y).obj (CatCospanTransform.id F G)) ((precompose F G).obj U) ((precompose F G).obj U)
                    ((transform X).obj (CatCospanTransform.id F G))).hom ≫
                ((precompose F G).obj U).whiskerLeft (transformObjId X F G).hom).app
            x✝¹).fst.app
      x✝ =
    ((whiskerRight (transformObjId Y F G).hom ((precompose F G).obj U) ≫
                ((precompose F G).obj U).leftUnitor.hom ≫ ((precompose F G).obj U).rightUnitor.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
X : Type u₇
Y : Type u₈
inst✝¹ : Category.{v₇, u₇} X
inst✝ : Category.{v₈, u₈} Y
U : X ⥤ Y
F : A ⥤ B
G : C ⥤ B
x✝¹ : CatCommSqOver F G Y
x✝ : X
⊢ (((CatCommSq.iso ((transform Y).obj (CatCospanTransform.id F G)) ((precompose F G).obj U) ((precompose F G).obj U)
                    ((transform X).obj (CatCospanTransform.id F G))).hom ≫
                ((precompose F G).obj U).whiskerLeft (transformObjId X F G).hom).app
            x✝¹).snd.app
      x✝ =
    ((whiskerRight (transformObjId Y F G).hom ((precompose F G).obj U) ≫
                ((precompose F G).obj U).leftUnitor.hom ≫ ((precompose F G).obj U).rightUnitor.inv).app
            x✝¹).snd.app
      x✝