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
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₁
A₂ : Type u₇
B₂ : Type u₈
C₂ : Type u₉
inst_6 : Category.{v₇, u₇} A₂
inst_7 : Category.{v₈, u₈} B₂
inst_8 : Category.{v₉, u₉} C₂
F₂ : Functor.{v₇, v₈, u₇, u₈} A₂ B₂
G₂ : Functor.{v₉, v₈, u₉, u₈} C₂ B₂
X : Type u₇
inst_9 : Category.{v₇, u₇} X
ψ ψ' : CatCospanTransform F G F₁ G₁
α : ψ ⟶ ψ'
φ : CatCospanTransform F₁ G₁ F₂ G₂
x : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X
x_1 : X
⊢ NatTrans.app (Hom.fst (NatTrans.app (map (transform X) (α ▷ φ)) x)) x_1 =
    (NatTrans.app
            (Iso.hom (transformObjComp X ψ φ) ≫
              whiskerRight (map (transform X) α) (obj (transform X) φ) ≫ Iso.inv (transformObjComp X ψ' φ))
            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
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₁
A₂ : Type u₇
B₂ : Type u₈
C₂ : Type u₉
inst_6 : Category.{v₇, u₇} A₂
inst_7 : Category.{v₈, u₈} B₂
inst_8 : Category.{v₉, u₉} C₂
F₂ : Functor.{v₇, v₈, u₇, u₈} A₂ B₂
G₂ : Functor.{v₉, v₈, u₉, u₈} C₂ B₂
X : Type u₇
inst_9 : Category.{v₇, u₇} X
ψ ψ' : CatCospanTransform F G F₁ G₁
α : ψ ⟶ ψ'
φ : CatCospanTransform F₁ G₁ F₂ G₂
x : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X
x_1 : X
⊢ NatTrans.app (Hom.snd (NatTrans.app (map (transform X) (α ▷ φ)) x)) x_1 =
    (NatTrans.app
            (Iso.hom (transformObjComp X ψ φ) ≫
              whiskerRight (map (transform X) α) (obj (transform X) φ) ≫ Iso.inv (transformObjComp X ψ' φ))
            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₁
A₂ : Type u₇
B₂ : Type u₈
C₂ : Type u₉
inst_6 : Category.{v₇, u₇} A₂
inst_7 : Category.{v₈, u₈} B₂
inst_8 : 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_9 : Category.{v₁₀, u₁₀} A₃
inst_10 : Category.{v₁₁, u₁₁} B₃
inst_11 : Category.{v₁₂, u₁₂} C₃
F₃ : Functor.{v₁₀, v₁₁, u₁₀, u₁₁} A₃ B₃
G₃ : Functor.{v₁₂, v₁₁, u₁₂, u₁₁} C₃ B₃
X : Type u₁₃
inst_12 : Category.{v₁₃, u₁₃} X
ψ : CatCospanTransform F G F₁ G₁
φ : CatCospanTransform F₁ G₁ F₂ G₂
τ : CatCospanTransform F₂ G₂ F₃ G₃
w :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₁₃, u₁, u₂, u₃, u₁₃} F G X) (x_1 : X),
    NatTrans.app (Hom.fst (NatTrans.app (map (transform X) (α_ ψ φ τ).hom) x)) x_1 =
      (NatTrans.app
              (Iso.hom (transformObjComp X (ψ.comp φ) τ) ≫
                whiskerRight (Iso.hom (transformObjComp X ψ φ)) (obj (transform X) τ) ≫
                  Iso.hom (associator (obj (transform X) ψ) (obj (transform X) φ) (obj (transform X) τ)) ≫
                    whiskerLeft (obj (transform X) ψ) (Iso.inv (transformObjComp X φ τ)) ≫
                      Iso.inv (transformObjComp X ψ (φ.comp τ)))
              x).fst.app
        x_1
w₁ :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₁₃, u₁, u₂, u₃, u₁₃} F G X) (x_1 : X),
    NatTrans.app (Hom.snd (NatTrans.app (map (transform X) (α_ ψ φ τ).hom) x)) x_1 =
      (NatTrans.app
              (Iso.hom (transformObjComp X (ψ.comp φ) τ) ≫
                whiskerRight (Iso.hom (transformObjComp X ψ φ)) (obj (transform X) τ) ≫
                  Iso.hom (associator (obj (transform X) ψ) (obj (transform X) φ) (obj (transform X) τ)) ≫
                    whiskerLeft (obj (transform X) ψ) (Iso.inv (transformObjComp X φ τ)) ≫
                      Iso.inv (transformObjComp X ψ (φ.comp τ)))
              x).snd.app
        x_1
⊢ Eq (α :=
    Quiver.Hom (V :=
      CatCommSqOver.{v₁, v₂, v₃, v₁₃, u₁, u₂, u₃, u₁₃} F G X ⥤
        CatCommSqOver.{v₁₀, v₁₁, v₁₂, v₁₃, u₁₀, u₁₁, u₁₂, u₁₃} F₃ G₃ X)
      (obj (transform X) ((ψ.comp φ).comp τ)) (obj (transform X) (ψ.comp (φ.comp τ))))
    (map (transform X) (α_ ψ φ τ).hom)
    (Iso.hom (transformObjComp X (ψ.comp φ) τ) ≫
      whiskerRight (Iso.hom (transformObjComp X ψ φ)) (obj (transform X) τ) ≫
        Iso.hom (associator (obj (transform X) ψ) (obj (transform X) φ) (obj (transform X) τ)) ≫
          whiskerLeft (obj (transform X) ψ) (Iso.inv (transformObjComp X φ τ)) ≫
            Iso.inv (transformObjComp X ψ (φ.comp τ)))

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₁
A₂ : Type u₇
B₂ : Type u₈
C₂ : Type u₉
inst_6 : Category.{v₇, u₇} A₂
inst_7 : Category.{v₈, u₈} B₂
inst_8 : 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_9 : Category.{v₁₀, u₁₀} A₃
inst_10 : Category.{v₁₁, u₁₁} B₃
inst_11 : Category.{v₁₂, u₁₂} C₃
F₃ : Functor.{v₁₀, v₁₁, u₁₀, u₁₁} A₃ B₃
G₃ : Functor.{v₁₂, v₁₁, u₁₂, u₁₁} C₃ B₃
X : Type u₁₃
inst_12 : Category.{v₁₃, u₁₃} X
ψ : CatCospanTransform F G F₁ G₁
φ : CatCospanTransform F₁ G₁ F₂ G₂
τ : CatCospanTransform F₂ G₂ F₃ G₃
x : CatCommSqOver.{v₁, v₂, v₃, v₁₃, u₁, u₂, u₃, u₁₃} F G X
x_1 : X
⊢ NatTrans.app (Hom.fst (NatTrans.app (map (transform X) (α_ ψ φ τ).hom) x)) x_1 =
    (NatTrans.app
            (Iso.hom (transformObjComp X (ψ.comp φ) τ) ≫
              whiskerRight (Iso.hom (transformObjComp X ψ φ)) (obj (transform X) τ) ≫
                Iso.hom (associator (obj (transform X) ψ) (obj (transform X) φ) (obj (transform X) τ)) ≫
                  whiskerLeft (obj (transform X) ψ) (Iso.inv (transformObjComp X φ τ)) ≫
                    Iso.inv (transformObjComp X ψ (φ.comp τ)))
            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
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₁
A₂ : Type u₇
B₂ : Type u₈
C₂ : Type u₉
inst_6 : Category.{v₇, u₇} A₂
inst_7 : Category.{v₈, u₈} B₂
inst_8 : 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_9 : Category.{v₁₀, u₁₀} A₃
inst_10 : Category.{v₁₁, u₁₁} B₃
inst_11 : Category.{v₁₂, u₁₂} C₃
F₃ : Functor.{v₁₀, v₁₁, u₁₀, u₁₁} A₃ B₃
G₃ : Functor.{v₁₂, v₁₁, u₁₂, u₁₁} C₃ B₃
X : Type u₁₃
inst_12 : Category.{v₁₃, u₁₃} X
ψ : CatCospanTransform F G F₁ G₁
φ : CatCospanTransform F₁ G₁ F₂ G₂
τ : CatCospanTransform F₂ G₂ F₃ G₃
x : CatCommSqOver.{v₁, v₂, v₃, v₁₃, u₁, u₂, u₃, u₁₃} F G X
x_1 : X
⊢ NatTrans.app (Hom.snd (NatTrans.app (map (transform X) (α_ ψ φ τ).hom) x)) x_1 =
    (NatTrans.app
            (Iso.hom (transformObjComp X (ψ.comp φ) τ) ≫
              whiskerRight (Iso.hom (transformObjComp X ψ φ)) (obj (transform X) τ) ≫
                Iso.hom (associator (obj (transform X) ψ) (obj (transform X) φ) (obj (transform X) τ)) ≫
                  whiskerLeft (obj (transform X) ψ) (Iso.inv (transformObjComp X φ τ)) ≫
                    Iso.inv (transformObjComp X ψ (φ.comp τ)))
            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₇
inst_6 : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
w :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) (x_1 : X),
    NatTrans.app (Hom.fst (NatTrans.app (map (transform X) (λ_ ψ).hom) x)) x_1 =
      (NatTrans.app
              (Iso.hom (transformObjComp X (CatCospanTransform.id F G) ψ) ≫
                whiskerRight (Iso.hom (transformObjId X F G)) (obj (transform X) ψ) ≫
                  Iso.hom (leftUnitor (obj (transform X) ψ)))
              x).fst.app
        x_1
w₁ :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) (x_1 : X),
    NatTrans.app (Hom.snd (NatTrans.app (map (transform X) (λ_ ψ).hom) x)) x_1 =
      (NatTrans.app
              (Iso.hom (transformObjComp X (CatCospanTransform.id F G) ψ) ≫
                whiskerRight (Iso.hom (transformObjId X F G)) (obj (transform X) ψ) ≫
                  Iso.hom (leftUnitor (obj (transform X) ψ)))
              x).snd.app
        x_1
⊢ Eq (α :=
    Quiver.Hom (V :=
      CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X ⥤ CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X)
      (obj (transform X) ((CatCospanTransform.id F G).comp ψ)) (obj (transform X) ψ))
    (map (transform X) (λ_ ψ).hom)
    (Iso.hom (transformObjComp X (CatCospanTransform.id F G) ψ) ≫
      whiskerRight (Iso.hom (transformObjId X F G)) (obj (transform X) ψ) ≫ Iso.hom (leftUnitor (obj (transform X) ψ)))

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₇
inst_6 : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
x : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X
x_1 : X
⊢ NatTrans.app (Hom.fst (NatTrans.app (map (transform X) (λ_ ψ).hom) x)) x_1 =
    (NatTrans.app
            (Iso.hom (transformObjComp X (CatCospanTransform.id F G) ψ) ≫
              whiskerRight (Iso.hom (transformObjId X F G)) (obj (transform X) ψ) ≫
                Iso.hom (leftUnitor (obj (transform X) ψ)))
            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
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₇
inst_6 : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
x : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X
x_1 : X
⊢ NatTrans.app (Hom.snd (NatTrans.app (map (transform X) (λ_ ψ).hom) x)) x_1 =
    (NatTrans.app
            (Iso.hom (transformObjComp X (CatCospanTransform.id F G) ψ) ≫
              whiskerRight (Iso.hom (transformObjId X F G)) (obj (transform X) ψ) ≫
                Iso.hom (leftUnitor (obj (transform X) ψ)))
            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₇
inst_6 : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
w :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) (x_1 : X),
    NatTrans.app (Hom.fst (NatTrans.app (map (transform X) (ρ_ ψ).hom) x)) x_1 =
      (NatTrans.app
              (Iso.hom (transformObjComp X ψ (CatCospanTransform.id F₁ G₁)) ≫
                whiskerLeft (obj (transform X) ψ) (Iso.hom (transformObjId X F₁ G₁)) ≫
                  Iso.hom (rightUnitor (obj (transform X) ψ)))
              x).fst.app
        x_1
w₁ :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X) (x_1 : X),
    NatTrans.app (Hom.snd (NatTrans.app (map (transform X) (ρ_ ψ).hom) x)) x_1 =
      (NatTrans.app
              (Iso.hom (transformObjComp X ψ (CatCospanTransform.id F₁ G₁)) ≫
                whiskerLeft (obj (transform X) ψ) (Iso.hom (transformObjId X F₁ G₁)) ≫
                  Iso.hom (rightUnitor (obj (transform X) ψ)))
              x).snd.app
        x_1
⊢ Eq (α :=
    Quiver.Hom (V :=
      CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X ⥤ CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X)
      (obj (transform X) (ψ.comp (CatCospanTransform.id F₁ G₁))) (obj (transform X) ψ))
    (map (transform X) (ρ_ ψ).hom)
    (Iso.hom (transformObjComp X ψ (CatCospanTransform.id F₁ G₁)) ≫
      whiskerLeft (obj (transform X) ψ) (Iso.hom (transformObjId X F₁ G₁)) ≫
        Iso.hom (rightUnitor (obj (transform X) ψ)))

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₇
inst_6 : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
x : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X
x_1 : X
⊢ NatTrans.app (Hom.fst (NatTrans.app (map (transform X) (ρ_ ψ).hom) x)) x_1 =
    (NatTrans.app
            (Iso.hom (transformObjComp X ψ (CatCospanTransform.id F₁ G₁)) ≫
              whiskerLeft (obj (transform X) ψ) (Iso.hom (transformObjId X F₁ G₁)) ≫
                Iso.hom (rightUnitor (obj (transform X) ψ)))
            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
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₇
inst_6 : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
x : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X
x_1 : X
⊢ NatTrans.app (Hom.snd (NatTrans.app (map (transform X) (ρ_ ψ).hom) x)) x_1 =
    (NatTrans.app
            (Iso.hom (transformObjComp X ψ (CatCospanTransform.id F₁ G₁)) ≫
              whiskerLeft (obj (transform X) ψ) (Iso.hom (transformObjId X F₁ G₁)) ≫
                Iso.hom (rightUnitor (obj (transform X) ψ)))
            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 : Functor.{v₄, v₅, u₄, u₅} X Y
X_1 : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y
h₁ :
  ∀ (x : X),
    NatTrans.app (Hom.fst { fst := U.whiskerLeft (Hom.fst (𝟙 X_1)), snd := U.whiskerLeft (Hom.snd (𝟙 X_1)), w := ⋯ })
        x =
      (Hom.fst
            (𝟙
              { fst := U ⋙ X_1.fst, snd := U ⋙ X_1.snd,
                iso := U.associator X_1.fst F ≪≫ U.isoWhiskerLeft X_1.iso ≪≫ (U.associator X_1.snd G).symm :
                CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X })).app
        x
h₂ :
  ∀ (x : X),
    NatTrans.app (Hom.snd { fst := U.whiskerLeft (Hom.fst (𝟙 X_1)), snd := U.whiskerLeft (Hom.snd (𝟙 X_1)), w := ⋯ })
        x =
      (Hom.snd
            (𝟙
              { fst := U ⋙ X_1.fst, snd := U ⋙ X_1.snd,
                iso := U.associator X_1.fst F ≪≫ U.isoWhiskerLeft X_1.iso ≪≫ (U.associator X_1.snd G).symm :
                CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X })).app
        x
⊢ { fst := U.whiskerLeft (Hom.fst (𝟙 X_1)), snd := U.whiskerLeft (Hom.snd (𝟙 X_1)), w := ⋯ } =
    𝟙
      { fst := U ⋙ X_1.fst, snd := U ⋙ X_1.snd,
        iso := U.associator X_1.fst F ≪≫ U.isoWhiskerLeft X_1.iso ≪≫ (U.associator X_1.snd G).symm :
        CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }

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 : Functor.{v₄, v₅, u₄, u₅} X Y
X_1 : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y
x : X
⊢ NatTrans.app (Hom.fst { fst := U.whiskerLeft (Hom.fst (𝟙 X_1)), snd := U.whiskerLeft (Hom.snd (𝟙 X_1)), w := ⋯ }) x =
    (Hom.fst
          (𝟙
            { fst := U ⋙ X_1.fst, snd := U ⋙ X_1.snd,
              iso := U.associator X_1.fst F ≪≫ U.isoWhiskerLeft X_1.iso ≪≫ (U.associator X_1.snd G).symm :
              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X })).app
      x

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
X_1 : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y
x : X
⊢ NatTrans.app (Hom.snd { fst := U.whiskerLeft (Hom.fst (𝟙 X_1)), snd := U.whiskerLeft (Hom.snd (𝟙 X_1)), w := ⋯ }) x =
    (Hom.snd
          (𝟙
            { fst := U ⋙ X_1.fst, snd := U ⋙ X_1.snd,
              iso := U.associator X_1.fst F ≪≫ U.isoWhiskerLeft X_1.iso ≪≫ (U.associator X_1.snd G).symm :
              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X })).app
      x

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
X_1 Y_1 Z_1 : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y
f : X_1 ⟶ Y_1
g : Y_1 ⟶ Z_1
x : X
⊢ Eq.{v₁ + 1} (α :=
    { fst := U ⋙ X_1.fst, snd := U ⋙ X_1.snd,
              iso := U.associator X_1.fst F ≪≫ U.isoWhiskerLeft X_1.iso ≪≫ (U.associator X_1.snd G).symm :
              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }.fst.obj
        x ⟶
      { fst := U ⋙ Z_1.fst, snd := U ⋙ Z_1.snd,
              iso := U.associator Z_1.fst F ≪≫ U.isoWhiskerLeft Z_1.iso ≪≫ (U.associator Z_1.snd G).symm :
              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }.fst.obj
        x)
    (NatTrans.app (Hom.fst { fst := U.whiskerLeft (f ≫ g).fst, snd := U.whiskerLeft (f ≫ g).snd, w := ⋯ }) x)
    (NatTrans.app
      (Hom.fst
        (CategoryStruct.comp (Y :=
          { fst := U ⋙ Y_1.fst, snd := U ⋙ Y_1.snd,
            iso := U.associator Y_1.fst F ≪≫ U.isoWhiskerLeft Y_1.iso ≪≫ (U.associator Y_1.snd G).symm })
          { fst := U.whiskerLeft f.fst, snd := U.whiskerLeft f.snd, w := ⋯ }
          { fst := U.whiskerLeft g.fst, snd := U.whiskerLeft g.snd, w := ⋯ }))
      x)

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
X_1 Y_1 Z_1 : CatCommSqOver.{v₁, v₂, v₃, v₅, u₁, u₂, u₃, u₅} F G Y
f : X_1 ⟶ Y_1
g : Y_1 ⟶ Z_1
x : X
⊢ Eq.{v₃ + 1} (α :=
    { fst := U ⋙ X_1.fst, snd := U ⋙ X_1.snd,
              iso := U.associator X_1.fst F ≪≫ U.isoWhiskerLeft X_1.iso ≪≫ (U.associator X_1.snd G).symm :
              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }.snd.obj
        x ⟶
      { fst := U ⋙ Z_1.fst, snd := U ⋙ Z_1.snd,
              iso := U.associator Z_1.fst F ≪≫ U.isoWhiskerLeft Z_1.iso ≪≫ (U.associator Z_1.snd G).symm :
              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }.snd.obj
        x)
    (NatTrans.app (Hom.snd { fst := U.whiskerLeft (f ≫ g).fst, snd := U.whiskerLeft (f ≫ g).snd, w := ⋯ }) x)
    (NatTrans.app
      (Hom.snd
        (CategoryStruct.comp (Y :=
          { fst := U ⋙ Y_1.fst, snd := U ⋙ Y_1.snd,
            iso := U.associator Y_1.fst F ≪≫ U.isoWhiskerLeft Y_1.iso ≪≫ (U.associator Y_1.snd G).symm })
          { fst := U.whiskerLeft f.fst, snd := U.whiskerLeft f.snd, w := ⋯ }
          { fst := U.whiskerLeft g.fst, snd := U.whiskerLeft g.snd, w := ⋯ }))
      x)

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
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
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
⊢ map (precompose F G) (U.whiskerLeft α) =
    (precomposeObjComp F G U V).hom ≫
      whiskerRight (map (precompose F G) α) (obj (precompose F G) U) ≫ (precomposeObjComp F G U W).inv

Tactic:
ext