awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
Y : Type u₅
Z : Type u₆
inst_3 : Category.{v₄, u₄} X
inst_4 : Category.{v₅, u₅} Y
inst_5 : Category.{v₆, u₆} Z
U : Functor.{v₄, v₅, u₄, u₅} X Y
V W : Functor.{v₅, v₆, u₅, u₆} Y Z
α : V ⟶ W
x : CatCommSqOver.{v₁, v₂, v₃, v₆, u₁, u₂, u₃, u₆} F G Z
x_1 : X
⊢ NatTrans.app (Hom.fst (NatTrans.app (map (precompose F G) (U.whiskerLeft α)) x)) x_1 =
    (((precomposeObjComp F G U V).hom ≫
                whiskerRight (map (precompose F G) α) (obj (precompose F G) U) ≫ (precomposeObjComp F G U W).inv).app
            x).fst.app
      x_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
Y : Type u₅
Z : Type u₆
inst_3 : Category.{v₄, u₄} X
inst_4 : Category.{v₅, u₅} Y
inst_5 : Category.{v₆, u₆} Z
U : Functor.{v₄, v₅, u₄, u₅} X Y
V W : Functor.{v₅, v₆, u₅, u₆} Y Z
α : V ⟶ W
x : CatCommSqOver.{v₁, v₂, v₃, v₆, u₁, u₂, u₃, u₆} F G Z
x_1 : X
⊢ NatTrans.app (Hom.snd (NatTrans.app (map (precompose F G) (U.whiskerLeft α)) x)) x_1 =
    (((precomposeObjComp F G U V).hom ≫
                whiskerRight (map (precompose F G) α) (obj (precompose F G) U) ≫ (precomposeObjComp F G U W).inv).app
            x).snd.app
      x_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
Y : Type u₅
Z : Type u₆
inst_3 : Category.{v₄, u₄} X
inst_4 : Category.{v₅, u₅} Y
inst_5 : Category.{v₆, u₆} Z
U V : Functor.{v₄, v₅, u₄, u₅} X Y
α : U ⟶ V
W : Functor.{v₅, v₆, u₅, u₆} Y Z
w :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₆, u₁, u₂, u₃, u₆} F G Z) (x_1 : X),
    NatTrans.app (Hom.fst (NatTrans.app (map (precompose F G) (whiskerRight α W)) x)) x_1 =
      (((precomposeObjComp F G U W).hom ≫
                  (obj (precompose F G) W).whiskerLeft (map (precompose F G) α) ≫ (precomposeObjComp F G V W).inv).app
              x).fst.app
        x_1
w₁ :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₆, u₁, u₂, u₃, u₆} F G Z) (x_1 : X),
    NatTrans.app (Hom.snd (NatTrans.app (map (precompose F G) (whiskerRight α W)) x)) x_1 =
      (((precomposeObjComp F G U W).hom ≫
                  (obj (precompose F G) W).whiskerLeft (map (precompose F G) α) ≫ (precomposeObjComp F G V W).inv).app
              x).snd.app
        x_1
⊢ map (precompose F G) (whiskerRight α W) =
    (precomposeObjComp F G U W).hom ≫
      (obj (precompose F G) W).whiskerLeft (map (precompose F G) α) ≫ (precomposeObjComp F G V W).inv

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
Y : Type u₅
Z : Type u₆
inst_3 : Category.{v₄, u₄} X
inst_4 : Category.{v₅, u₅} Y
inst_5 : Category.{v₆, u₆} Z
U V : Functor.{v₄, v₅, u₄, u₅} X Y
α : U ⟶ V
W : Functor.{v₅, v₆, u₅, u₆} Y Z
x : CatCommSqOver.{v₁, v₂, v₃, v₆, u₁, u₂, u₃, u₆} F G Z
x_1 : X
⊢ NatTrans.app (Hom.fst (NatTrans.app (map (precompose F G) (whiskerRight α W)) x)) x_1 =
    (((precomposeObjComp F G U W).hom ≫
                (obj (precompose F G) W).whiskerLeft (map (precompose F G) α) ≫ (precomposeObjComp F G V W).inv).app
            x).fst.app
      x_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
Y : Type u₅
Z : Type u₆
inst_3 : Category.{v₄, u₄} X
inst_4 : Category.{v₅, u₅} Y
inst_5 : Category.{v₆, u₆} Z
U V : Functor.{v₄, v₅, u₄, u₅} X Y
α : U ⟶ V
W : Functor.{v₅, v₆, u₅, u₆} Y Z
x : CatCommSqOver.{v₁, v₂, v₃, v₆, u₁, u₂, u₃, u₆} F G Z
x_1 : X
⊢ NatTrans.app (Hom.snd (NatTrans.app (map (precompose F G) (whiskerRight α W)) x)) x_1 =
    (((precomposeObjComp F G U W).hom ≫
                (obj (precompose F G) W).whiskerLeft (map (precompose F G) α) ≫ (precomposeObjComp F G V W).inv).app
            x).snd.app
      x_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
Y : Type u₅
Z : Type u₆
inst_3 : Category.{v₄, u₄} X
inst_4 : Category.{v₅, u₅} Y
inst_5 : Category.{v₆, u₆} Z
T : Type u₇
inst_6 : Category.{v₇, u₇} T
U : Functor.{v₄, v₅, u₄, u₅} X Y
V : Functor.{v₅, v₆, u₅, u₆} Y Z
W : Functor.{v₆, v₇, u₆, u₇} Z T
w :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G T) (x_1 : X),
    NatTrans.app (Hom.fst (NatTrans.app (map (precompose F G) (U.associator V W).hom) x)) x_1 =
      (((precomposeObjComp F G (U ⋙ V) W).hom ≫
                  (obj (precompose F G) W).whiskerLeft (precomposeObjComp F G U V).hom ≫
                    ((obj (precompose F G) W).associator (obj (precompose F G) V) (obj (precompose F G) U)).inv ≫
                      whiskerRight (precomposeObjComp F G V W).inv (obj (precompose F G) U) ≫
                        (precomposeObjComp F G U (V ⋙ W)).inv).app
              x).fst.app
        x_1
w₁ :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G T) (x_1 : X),
    NatTrans.app (Hom.snd (NatTrans.app (map (precompose F G) (U.associator V W).hom) x)) x_1 =
      (((precomposeObjComp F G (U ⋙ V) W).hom ≫
                  (obj (precompose F G) W).whiskerLeft (precomposeObjComp F G U V).hom ≫
                    ((obj (precompose F G) W).associator (obj (precompose F G) V) (obj (precompose F G) U)).inv ≫
                      whiskerRight (precomposeObjComp F G V W).inv (obj (precompose F G) U) ≫
                        (precomposeObjComp F G U (V ⋙ W)).inv).app
              x).snd.app
        x_1
⊢ map (precompose F G) (U.associator V W).hom =
    (precomposeObjComp F G (U ⋙ V) W).hom ≫
      (obj (precompose F G) W).whiskerLeft (precomposeObjComp F G U V).hom ≫
        ((obj (precompose F G) W).associator (obj (precompose F G) V) (obj (precompose F G) U)).inv ≫
          whiskerRight (precomposeObjComp F G V W).inv (obj (precompose F G) U) ≫ (precomposeObjComp F G U (V ⋙ W)).inv

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
Y : Type u₅
Z : Type u₆
inst_3 : Category.{v₄, u₄} X
inst_4 : Category.{v₅, u₅} Y
inst_5 : Category.{v₆, u₆} Z
T : Type u₇
inst_6 : Category.{v₇, u₇} T
U : Functor.{v₄, v₅, u₄, u₅} X Y
V : Functor.{v₅, v₆, u₅, u₆} Y Z
W : Functor.{v₆, v₇, u₆, u₇} Z T
x : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G T
x_1 : X
⊢ NatTrans.app (Hom.fst (NatTrans.app (map (precompose F G) (U.associator V W).hom) x)) x_1 =
    (((precomposeObjComp F G (U ⋙ V) W).hom ≫
                (obj (precompose F G) W).whiskerLeft (precomposeObjComp F G U V).hom ≫
                  ((obj (precompose F G) W).associator (obj (precompose F G) V) (obj (precompose F G) U)).inv ≫
                    whiskerRight (precomposeObjComp F G V W).inv (obj (precompose F G) U) ≫
                      (precomposeObjComp F G U (V ⋙ W)).inv).app
            x).fst.app
      x_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
Y : Type u₅
Z : Type u₆
inst_3 : Category.{v₄, u₄} X
inst_4 : Category.{v₅, u₅} Y
inst_5 : Category.{v₆, u₆} Z
T : Type u₇
inst_6 : Category.{v₇, u₇} T
U : Functor.{v₄, v₅, u₄, u₅} X Y
V : Functor.{v₅, v₆, u₅, u₆} Y Z
W : Functor.{v₆, v₇, u₆, u₇} Z T
x : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G T
x_1 : X
⊢ NatTrans.app (Hom.snd (NatTrans.app (map (precompose F G) (U.associator V W).hom) x)) x_1 =
    (((precomposeObjComp F G (U ⋙ V) W).hom ≫
                (obj (precompose F G) W).whiskerLeft (precomposeObjComp F G U V).hom ≫
                  ((obj (precompose F G) W).associator (obj (precompose F G) V) (obj (precompose F G) U)).inv ≫
                    whiskerRight (precomposeObjComp F G V W).inv (obj (precompose F G) U) ≫
                      (precomposeObjComp F G U (V ⋙ W)).inv).app
            x).snd.app
      x_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
Y : Type u₅
inst_3 : Category.{v₄, u₄} X
inst_4 : Category.{v₅, u₅} Y
U : Functor.{v₄, v₅, u₄, u₅} X Y
w :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) (x_1 : X),
    NatTrans.app (Hom.fst (NatTrans.app (map (precompose F G) U.leftUnitor.hom) x)) x_1 =
      ((Iso.hom (precomposeObjComp F G (𝟭 X) U) ≫
                  (obj (precompose F G) U).whiskerLeft (Iso.hom (precomposeObjId F G X)) ≫
                    (obj (precompose F G) U).rightUnitor.hom).app
              x).fst.app
        x_1
w₁ :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) (x_1 : X),
    NatTrans.app (Hom.snd (NatTrans.app (map (precompose F G) U.leftUnitor.hom) x)) x_1 =
      ((Iso.hom (precomposeObjComp F G (𝟭 X) U) ≫
                  (obj (precompose F G) U).whiskerLeft (Iso.hom (precomposeObjId F G X)) ≫
                    (obj (precompose F G) U).rightUnitor.hom).app
              x).snd.app
        x_1
⊢ map (precompose F G) U.leftUnitor.hom =
    Iso.hom (precomposeObjComp F G (𝟭 X) U) ≫
      (obj (precompose F G) U).whiskerLeft (Iso.hom (precomposeObjId F G X)) ≫ (obj (precompose F G) U).rightUnitor.hom

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
Y : Type u₅
inst_3 : Category.{v₄, u₄} X
inst_4 : Category.{v₅, u₅} Y
U : Functor.{v₄, v₅, u₄, u₅} X Y
x : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y
x_1 : X
⊢ NatTrans.app (Hom.fst (NatTrans.app (map (precompose F G) U.leftUnitor.hom) x)) x_1 =
    ((Iso.hom (precomposeObjComp F G (𝟭 X) U) ≫
                (obj (precompose F G) U).whiskerLeft (Iso.hom (precomposeObjId F G X)) ≫
                  (obj (precompose F G) U).rightUnitor.hom).app
            x).fst.app
      x_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
Y : Type u₅
inst_3 : Category.{v₄, u₄} X
inst_4 : Category.{v₅, u₅} Y
U : Functor.{v₄, v₅, u₄, u₅} X Y
x : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y
x_1 : X
⊢ NatTrans.app (Hom.snd (NatTrans.app (map (precompose F G) U.leftUnitor.hom) x)) x_1 =
    ((Iso.hom (precomposeObjComp F G (𝟭 X) U) ≫
                (obj (precompose F G) U).whiskerLeft (Iso.hom (precomposeObjId F G X)) ≫
                  (obj (precompose F G) U).rightUnitor.hom).app
            x).snd.app
      x_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
Y : Type u₅
inst_3 : Category.{v₄, u₄} X
inst_4 : Category.{v₅, u₅} Y
U : Functor.{v₄, v₅, u₄, u₅} X Y
w :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) (x_1 : X),
    NatTrans.app (Hom.fst (NatTrans.app (map (precompose F G) U.rightUnitor.hom) x)) x_1 =
      (((precomposeObjComp F G U (𝟭 Y)).hom ≫
                  whiskerRight (Iso.hom (precomposeObjId F G Y)) (obj (precompose F G) U) ≫
                    (obj (precompose F G) U).leftUnitor.hom).app
              x).fst.app
        x_1
w₁ :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y) (x_1 : X),
    NatTrans.app (Hom.snd (NatTrans.app (map (precompose F G) U.rightUnitor.hom) x)) x_1 =
      (((precomposeObjComp F G U (𝟭 Y)).hom ≫
                  whiskerRight (Iso.hom (precomposeObjId F G Y)) (obj (precompose F G) U) ≫
                    (obj (precompose F G) U).leftUnitor.hom).app
              x).snd.app
        x_1
⊢ map (precompose F G) U.rightUnitor.hom =
    (precomposeObjComp F G U (𝟭 Y)).hom ≫
      whiskerRight (Iso.hom (precomposeObjId F G Y)) (obj (precompose F G) U) ≫ (obj (precompose F G) U).leftUnitor.hom

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
Y : Type u₅
inst_3 : Category.{v₄, u₄} X
inst_4 : Category.{v₅, u₅} Y
U : Functor.{v₄, v₅, u₄, u₅} X Y
x : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y
x_1 : X
⊢ NatTrans.app (Hom.fst (NatTrans.app (map (precompose F G) U.rightUnitor.hom) x)) x_1 =
    (((precomposeObjComp F G U (𝟭 Y)).hom ≫
                whiskerRight (Iso.hom (precomposeObjId F G Y)) (obj (precompose F G) U) ≫
                  (obj (precompose F G) U).leftUnitor.hom).app
            x).fst.app
      x_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
X : Type u₄
Y : Type u₅
inst_3 : Category.{v₄, u₄} X
inst_4 : Category.{v₅, u₅} Y
U : Functor.{v₄, v₅, u₄, u₅} X Y
x : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y
x_1 : X
⊢ NatTrans.app (Hom.snd (NatTrans.app (map (precompose F G) U.rightUnitor.hom) x)) x_1 =
    (((precomposeObjComp F G U (𝟭 Y)).hom ≫
                whiskerRight (Iso.hom (precomposeObjId F G Y)) (obj (precompose F G) U) ≫
                  (obj (precompose F G) U).leftUnitor.hom).app
            x).snd.app
      x_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst_3 : Category.{v₄, u₄} A₁
inst_4 : Category.{v₅, u₅} B₁
inst_5 : Category.{v₆, u₆} C₁
F₁ : Functor.{v₄, v₅, u₄, u₅} A₁ B₁
G₁ : Functor.{v₆, v₅, u₆, u₅} C₁ B₁
X : Type u₇
Y : Type u₈
inst_6 : Category.{v₇, u₇} X
inst_7 : Category.{v₈, u₈} Y
ψ : CatCospanTransform F G F₁ G₁
U : Functor.{v₇, v₈, u₇, u₈} X Y
x y : CatCommSqOver.{v₁, v₂, v₃, v₈, u₁, u₂, u₃, u₈} F G Y
f : x ⟶ y
x_1 : X
⊢ NatTrans.app
      (Hom.fst
        ((obj (precompose F G) U ⋙ obj (transform X) ψ).map f ≫
          Iso.hom
            ((fun (x : CatCommSqOver.{v₁, v₂, v₃, v₈, u₁, u₂, u₃, u₈} F G Y) ↦
                (mkIso (U.associator x.fst ψ.left) (U.associator x.snd ψ.right) ⋯ :
                  (obj (precompose F G) U ⋙ obj (transform X) ψ).obj x ≅
                    (obj (transform Y) ψ ⋙ obj (precompose F₁ G₁) U).obj x))
              y)))
      x_1 =
    NatTrans.app
      (Hom.fst
        (Iso.hom
            ((fun (x : CatCommSqOver.{v₁, v₂, v₃, v₈, u₁, u₂, u₃, u₈} F G Y) ↦
                (mkIso (U.associator x.fst ψ.left) (U.associator x.snd ψ.right) ⋯ :
                  (obj (precompose F G) U ⋙ obj (transform X) ψ).obj x ≅
                    (obj (transform Y) ψ ⋙ obj (precompose F₁ G₁) U).obj x))
              x) ≫
          (obj (transform Y) ψ ⋙ obj (precompose F₁ G₁) U).map f))
      x_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst_3 : Category.{v₄, u₄} A₁
inst_4 : Category.{v₅, u₅} B₁
inst_5 : Category.{v₆, u₆} C₁
F₁ : Functor.{v₄, v₅, u₄, u₅} A₁ B₁
G₁ : Functor.{v₆, v₅, u₆, u₅} C₁ B₁
X : Type u₇
Y : Type u₈
inst_6 : Category.{v₇, u₇} X
inst_7 : Category.{v₈, u₈} Y
ψ : CatCospanTransform F G F₁ G₁
U : Functor.{v₇, v₈, u₇, u₈} X Y
x y : CatCommSqOver.{v₁, v₂, v₃, v₈, u₁, u₂, u₃, u₈} F G Y
f : x ⟶ y
x_1 : X
⊢ NatTrans.app
      (Hom.snd
        ((obj (precompose F G) U ⋙ obj (transform X) ψ).map f ≫
          Iso.hom
            ((fun (x : CatCommSqOver.{v₁, v₂, v₃, v₈, u₁, u₂, u₃, u₈} F G Y) ↦
                (mkIso (U.associator x.fst ψ.left) (U.associator x.snd ψ.right) ⋯ :
                  (obj (precompose F G) U ⋙ obj (transform X) ψ).obj x ≅
                    (obj (transform Y) ψ ⋙ obj (precompose F₁ G₁) U).obj x))
              y)))
      x_1 =
    NatTrans.app
      (Hom.snd
        (Iso.hom
            ((fun (x : CatCommSqOver.{v₁, v₂, v₃, v₈, u₁, u₂, u₃, u₈} F G Y) ↦
                (mkIso (U.associator x.fst ψ.left) (U.associator x.snd ψ.right) ⋯ :
                  (obj (precompose F G) U ⋙ obj (transform X) ψ).obj x ≅
                    (obj (transform Y) ψ ⋙ obj (precompose F₁ G₁) U).obj x))
              x) ≫
          (obj (transform Y) ψ ⋙ obj (precompose F₁ G₁) U).map f))
      x_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst_3 : Category.{v₄, u₄} A₁
inst_4 : Category.{v₅, u₅} B₁
inst_5 : Category.{v₆, u₆} C₁
F₁ : Functor.{v₄, v₅, u₄, u₅} A₁ B₁
G₁ : Functor.{v₆, v₅, u₆, u₅} C₁ B₁
X : Type u₇
Y : Type u₈
inst_6 : Category.{v₇, u₇} X
inst_7 : Category.{v₈, u₈} Y
ψ : CatCospanTransform F G F₁ G₁
U V : Functor.{v₇, v₈, u₇, u₈} X Y
α : U ⟶ V
w :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₈, u₁, u₂, u₃, u₈} F G Y) (x_1 : X),
    Eq (α :=
      ((obj (precompose F G) U ⋙ obj (transform X) ψ).obj x).fst.obj x_1 ⟶
        ((obj (transform Y) ψ ⋙ obj (precompose F₁ G₁) V).obj x).fst.obj x_1)
      (NatTrans.app
        (Hom.fst
          (NatTrans.app
            (whiskerRight (map (precompose F G) α) (obj (transform X) ψ) ≫
              Iso.hom
                (CatCommSq.iso (obj (precompose F G) V) (obj (transform Y) ψ) (obj (transform X) ψ)
                  (obj (precompose F₁ G₁) V)))
            x))
        x_1)
      (NatTrans.app
        (Hom.fst
          (NatTrans.app
            (Iso.hom
                (CatCommSq.iso (obj (precompose F G) U) (obj (transform Y) ψ) (obj (transform X) ψ)
                  (obj (precompose F₁ G₁) U)) ≫
              whiskerLeft (obj (transform Y) ψ) (map (precompose F₁ G₁) α))
            x))
        x_1)
w₁ :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₈, u₁, u₂, u₃, u₈} F G Y) (x_1 : X),
    Eq (α :=
      ((obj (precompose F G) U ⋙ obj (transform X) ψ).obj x).snd.obj x_1 ⟶
        ((obj (transform Y) ψ ⋙ obj (precompose F₁ G₁) V).obj x).snd.obj x_1)
      (NatTrans.app
        (Hom.snd
          (NatTrans.app
            (whiskerRight (map (precompose F G) α) (obj (transform X) ψ) ≫
              Iso.hom
                (CatCommSq.iso (obj (precompose F G) V) (obj (transform Y) ψ) (obj (transform X) ψ)
                  (obj (precompose F₁ G₁) V)))
            x))
        x_1)
      (NatTrans.app
        (Hom.snd
          (NatTrans.app
            (Iso.hom
                (CatCommSq.iso (obj (precompose F G) U) (obj (transform Y) ψ) (obj (transform X) ψ)
                  (obj (precompose F₁ G₁) U)) ≫
              whiskerLeft (obj (transform Y) ψ) (map (precompose F₁ G₁) α))
            x))
        x_1)
⊢ Eq (α := obj (precompose F G) U ⋙ obj (transform X) ψ ⟶ obj (transform Y) ψ ⋙ obj (precompose F₁ G₁) V)
    (whiskerRight (map (precompose F G) α) (obj (transform X) ψ) ≫
      Iso.hom
        (CatCommSq.iso (obj (precompose F G) V) (obj (transform Y) ψ) (obj (transform X) ψ) (obj (precompose F₁ G₁) V)))
    (Iso.hom
        (CatCommSq.iso (obj (precompose F G) U) (obj (transform Y) ψ) (obj (transform X) ψ)
          (obj (precompose F₁ G₁) U)) ≫
      whiskerLeft (obj (transform Y) ψ) (map (precompose F₁ G₁) α))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst_3 : Category.{v₄, u₄} A₁
inst_4 : Category.{v₅, u₅} B₁
inst_5 : Category.{v₆, u₆} C₁
F₁ : Functor.{v₄, v₅, u₄, u₅} A₁ B₁
G₁ : Functor.{v₆, v₅, u₆, u₅} C₁ B₁
X : Type u₇
Y : Type u₈
inst_6 : Category.{v₇, u₇} X
inst_7 : Category.{v₈, u₈} Y
ψ : CatCospanTransform F G F₁ G₁
U V : Functor.{v₇, v₈, u₇, u₈} X Y
α : U ⟶ V
x : CatCommSqOver.{v₁, v₂, v₃, v₈, u₁, u₂, u₃, u₈} F G Y
x_1 : X
⊢ Eq (α :=
    ((obj (precompose F G) U ⋙ obj (transform X) ψ).obj x).fst.obj x_1 ⟶
      ((obj (transform Y) ψ ⋙ obj (precompose F₁ G₁) V).obj x).fst.obj x_1)
    (NatTrans.app
      (Hom.fst
        (NatTrans.app
          (whiskerRight (map (precompose F G) α) (obj (transform X) ψ) ≫
            Iso.hom
              (CatCommSq.iso (obj (precompose F G) V) (obj (transform Y) ψ) (obj (transform X) ψ)
                (obj (precompose F₁ G₁) V)))
          x))
      x_1)
    (NatTrans.app
      (Hom.fst
        (NatTrans.app
          (Iso.hom
              (CatCommSq.iso (obj (precompose F G) U) (obj (transform Y) ψ) (obj (transform X) ψ)
                (obj (precompose F₁ G₁) U)) ≫
            whiskerLeft (obj (transform Y) ψ) (map (precompose F₁ G₁) α))
          x))
      x_1)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
inst : Category.{v₁, u₁} A
inst_1 : Category.{v₂, u₂} B
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
A₁ : Type u₄
B₁ : Type u₅
C₁ : Type u₆
inst_3 : Category.{v₄, u₄} A₁
inst_4 : Category.{v₅, u₅} B₁
inst_5 : Category.{v₆, u₆} C₁
F₁ : Functor.{v₄, v₅, u₄, u₅} A₁ B₁
G₁ : Functor.{v₆, v₅, u₆, u₅} C₁ B₁
X : Type u₇
Y : Type u₈
inst_6 : Category.{v₇, u₇} X
inst_7 : Category.{v₈, u₈} Y
ψ : CatCospanTransform F G F₁ G₁
U V : Functor.{v₇, v₈, u₇, u₈} X Y
α : U ⟶ V
x : CatCommSqOver.{v₁, v₂, v₃, v₈, u₁, u₂, u₃, u₈} F G Y
x_1 : X
⊢ Eq (α :=
    ((obj (precompose F G) U ⋙ obj (transform X) ψ).obj x).snd.obj x_1 ⟶
      ((obj (transform Y) ψ ⋙ obj (precompose F₁ G₁) V).obj x).snd.obj x_1)
    (NatTrans.app
      (Hom.snd
        (NatTrans.app
          (whiskerRight (map (precompose F G) α) (obj (transform X) ψ) ≫
            Iso.hom
              (CatCommSq.iso (obj (precompose F G) V) (obj (transform Y) ψ) (obj (transform X) ψ)
                (obj (precompose F₁ G₁) V)))
          x))
      x_1)
    (NatTrans.app
      (Hom.snd
        (NatTrans.app
          (Iso.hom
              (CatCommSq.iso (obj (precompose F G) U) (obj (transform Y) ψ) (obj (transform X) ψ)
                (obj (precompose F₁ G₁) U)) ≫
            whiskerLeft (obj (transform Y) ψ) (map (precompose F₁ G₁) α))
          x))
      x_1)

Tactic:
simp