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₁
X : Type u₇
inst_6 : Category.{v₇, u₇} X
ψ : CatCospanTransform F G F₁ G₁
X_1 : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X
x : X
⊢ Eq (α :=
    { fst := X_1.fst ⋙ ψ.left, snd := X_1.snd ⋙ ψ.right,
              iso :=
                X_1.fst.associator ψ.left F₁ ≪≫
                  X_1.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                    (X_1.fst.associator F ψ.base).symm ≪≫
                      isoWhiskerRight X_1.iso ψ.base ≪≫
                        X_1.snd.associator G ψ.base ≪≫
                          X_1.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                            (X_1.snd.associator ψ.right G₁).symm :
              CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }.fst.obj
        x ⟶
      { fst := X_1.fst ⋙ ψ.left, snd := X_1.snd ⋙ ψ.right,
              iso :=
                X_1.fst.associator ψ.left F₁ ≪≫
                  X_1.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                    (X_1.fst.associator F ψ.base).symm ≪≫
                      isoWhiskerRight X_1.iso ψ.base ≪≫
                        X_1.snd.associator G ψ.base ≪≫
                          X_1.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                            (X_1.snd.associator ψ.right G₁).symm :
              CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }.fst.obj
        x)
    (NatTrans.app
      (Hom.fst { fst := whiskerRight (Hom.fst (𝟙 X_1)) ψ.left, snd := whiskerRight (Hom.snd (𝟙 X_1)) ψ.right, w := ⋯ })
      x)
    (NatTrans.app
      (Hom.fst
        (𝟙
          { fst := X_1.fst ⋙ ψ.left, snd := X_1.snd ⋙ ψ.right,
            iso :=
              X_1.fst.associator ψ.left F₁ ≪≫
                X_1.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                  (X_1.fst.associator F ψ.base).symm ≪≫
                    isoWhiskerRight X_1.iso ψ.base ≪≫
                      X_1.snd.associator G ψ.base ≪≫
                        X_1.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                          (X_1.snd.associator ψ.right G₁).symm }))
      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
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_1 : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X
x : X
⊢ Eq (α :=
    { fst := X_1.fst ⋙ ψ.left, snd := X_1.snd ⋙ ψ.right,
              iso :=
                X_1.fst.associator ψ.left F₁ ≪≫
                  X_1.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                    (X_1.fst.associator F ψ.base).symm ≪≫
                      isoWhiskerRight X_1.iso ψ.base ≪≫
                        X_1.snd.associator G ψ.base ≪≫
                          X_1.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                            (X_1.snd.associator ψ.right G₁).symm :
              CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }.snd.obj
        x ⟶
      { fst := X_1.fst ⋙ ψ.left, snd := X_1.snd ⋙ ψ.right,
              iso :=
                X_1.fst.associator ψ.left F₁ ≪≫
                  X_1.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                    (X_1.fst.associator F ψ.base).symm ≪≫
                      isoWhiskerRight X_1.iso ψ.base ≪≫
                        X_1.snd.associator G ψ.base ≪≫
                          X_1.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                            (X_1.snd.associator ψ.right G₁).symm :
              CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }.snd.obj
        x)
    (NatTrans.app
      (Hom.snd { fst := whiskerRight (Hom.fst (𝟙 X_1)) ψ.left, snd := whiskerRight (Hom.snd (𝟙 X_1)) ψ.right, w := ⋯ })
      x)
    (NatTrans.app
      (Hom.snd
        (𝟙
          { fst := X_1.fst ⋙ ψ.left, snd := X_1.snd ⋙ ψ.right,
            iso :=
              X_1.fst.associator ψ.left F₁ ≪≫
                X_1.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                  (X_1.fst.associator F ψ.base).symm ≪≫
                    isoWhiskerRight X_1.iso ψ.base ≪≫
                      X_1.snd.associator G ψ.base ≪≫
                        X_1.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                          (X_1.snd.associator ψ.right G₁).symm }))
      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
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_1 Y Z : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X
f : X_1 ⟶ Y
g : Y ⟶ Z
x : X
⊢ Eq.{v₄ + 1} (α :=
    { fst := X_1.fst ⋙ ψ.left, snd := X_1.snd ⋙ ψ.right,
              iso :=
                X_1.fst.associator ψ.left F₁ ≪≫
                  X_1.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                    (X_1.fst.associator F ψ.base).symm ≪≫
                      isoWhiskerRight X_1.iso ψ.base ≪≫
                        X_1.snd.associator G ψ.base ≪≫
                          X_1.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                            (X_1.snd.associator ψ.right G₁).symm :
              CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }.fst.obj
        x ⟶
      { fst := Z.fst ⋙ ψ.left, snd := Z.snd ⋙ ψ.right,
              iso :=
                Z.fst.associator ψ.left F₁ ≪≫
                  Z.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                    (Z.fst.associator F ψ.base).symm ≪≫
                      isoWhiskerRight Z.iso ψ.base ≪≫
                        Z.snd.associator G ψ.base ≪≫
                          Z.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                            (Z.snd.associator ψ.right G₁).symm :
              CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }.fst.obj
        x)
    (NatTrans.app (Hom.fst { fst := whiskerRight (f ≫ g).fst ψ.left, snd := whiskerRight (f ≫ g).snd ψ.right, w := ⋯ })
      x)
    (NatTrans.app
      (Hom.fst
        (CategoryStruct.comp (Y :=
          { fst := Y.fst ⋙ ψ.left, snd := Y.snd ⋙ ψ.right,
            iso :=
              Y.fst.associator ψ.left F₁ ≪≫
                Y.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                  (Y.fst.associator F ψ.base).symm ≪≫
                    isoWhiskerRight Y.iso ψ.base ≪≫
                      Y.snd.associator G ψ.base ≪≫
                        Y.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                          (Y.snd.associator ψ.right G₁).symm })
          { fst := whiskerRight f.fst ψ.left, snd := whiskerRight f.snd ψ.right, w := ⋯ }
          { fst := whiskerRight g.fst ψ.left, snd := whiskerRight g.snd ψ.right, 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
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_1 Y Z : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X
f : X_1 ⟶ Y
g : Y ⟶ Z
x : X
⊢ Eq.{v₆ + 1} (α :=
    { fst := X_1.fst ⋙ ψ.left, snd := X_1.snd ⋙ ψ.right,
              iso :=
                X_1.fst.associator ψ.left F₁ ≪≫
                  X_1.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                    (X_1.fst.associator F ψ.base).symm ≪≫
                      isoWhiskerRight X_1.iso ψ.base ≪≫
                        X_1.snd.associator G ψ.base ≪≫
                          X_1.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                            (X_1.snd.associator ψ.right G₁).symm :
              CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }.snd.obj
        x ⟶
      { fst := Z.fst ⋙ ψ.left, snd := Z.snd ⋙ ψ.right,
              iso :=
                Z.fst.associator ψ.left F₁ ≪≫
                  Z.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                    (Z.fst.associator F ψ.base).symm ≪≫
                      isoWhiskerRight Z.iso ψ.base ≪≫
                        Z.snd.associator G ψ.base ≪≫
                          Z.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                            (Z.snd.associator ψ.right G₁).symm :
              CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }.snd.obj
        x)
    (NatTrans.app (Hom.snd { fst := whiskerRight (f ≫ g).fst ψ.left, snd := whiskerRight (f ≫ g).snd ψ.right, w := ⋯ })
      x)
    (NatTrans.app
      (Hom.snd
        (CategoryStruct.comp (Y :=
          { fst := Y.fst ⋙ ψ.left, snd := Y.snd ⋙ ψ.right,
            iso :=
              Y.fst.associator ψ.left F₁ ≪≫
                Y.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                  (Y.fst.associator F ψ.base).symm ≪≫
                    isoWhiskerRight Y.iso ψ.base ≪≫
                      Y.snd.associator G ψ.base ≪≫
                        Y.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                          (Y.snd.associator ψ.right G₁).symm })
          { fst := whiskerRight f.fst ψ.left, snd := whiskerRight f.snd ψ.right, w := ⋯ }
          { fst := whiskerRight g.fst ψ.left, snd := whiskerRight g.snd ψ.right, 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
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₁
η : ψ ⟶ ψ'
S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X
t : X
⊢ Eq (α := (ψ.left ⋙ F₁).obj (S.fst.obj t) ⟶ F₁.obj (ψ'.left.obj (S.fst.obj t)))
    ((CatCommSq.iso F ψ.left ψ.base F₁).inv.app (S.fst.obj t) ≫
      (CatCommSq.iso F ψ.left ψ.base F₁).hom.app (S.fst.obj t) ≫ F₁.map (η.left.app (S.fst.obj t)))
    ((CatCommSq.iso F ψ.left ψ.base F₁).inv.app (S.fst.obj t) ≫
      η.base.app (F.obj (S.fst.obj t)) ≫ (CatCommSq.iso F ψ'.left ψ'.base F₁).hom.app (S.fst.obj t))

Tactic:
have := ψ.squareLeft.iso.inv.app (S.fst.obj t) ≫=
            η.left_coherence_app (S.fst.obj t)
-- 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₁
η : ψ ⟶ ψ'
S : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X
t : X
this :
  Eq (α := (ψ.left ⋙ F₁).obj (S.fst.obj t) ⟶ F₁.obj (ψ'.left.obj (S.fst.obj t)))
    ((CatCommSq.iso F ψ.left ψ.base F₁).inv.app (S.fst.obj t) ≫
      (CatCommSq.iso F ψ.left ψ.base F₁).hom.app (S.fst.obj t) ≫ F₁.map (η.left.app (S.fst.obj t)))
    ((CatCommSq.iso F ψ.left ψ.base F₁).inv.app (S.fst.obj t) ≫
      η.base.app (F.obj (S.fst.obj t)) ≫ (CatCommSq.iso F ψ'.left ψ'.base F₁).hom.app (S.fst.obj t))
⊢ Eq (α := (ψ.left ⋙ F₁).obj (S.fst.obj t) ⟶ F₁.obj (ψ'.left.obj (S.fst.obj t))) (F₁.map (η.left.app (S.fst.obj t)))
    ((CatCommSq.iso F ψ.left ψ.base F₁).inv.app (S.fst.obj t) ≫
      η.base.app (F.obj (S.fst.obj t)) ≫ (CatCommSq.iso F ψ'.left ψ'.base F₁).hom.app (S.fst.obj t))

Tactic:
simp only [Iso.inv_hom_id_app_assoc] at this

Premises used: CategoryTheory.Iso.inv_hom_id_app_assoc
-- 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
X_1 Y Z : CatCospanTransform F G F₁ G₁
f : X_1 ⟶ Y
g : Y ⟶ Z
x : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X
x_1 : X
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

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 y : CatCommSqOver.{v₁, v₂, v₃, v₁₀, u₁, u₂, u₃, u₁₀} F G X
f : x ⟶ y
x_1 : X
⊢ Eq (α :=
    (obj (obj (transform X) (ψ.comp ψ')) x).fst.obj x_1 ⟶
      (obj (obj (transform X) ψ ⋙ obj (transform X) ψ') y).fst.obj x_1)
    (NatTrans.app
      (Hom.fst
        (map (obj (transform X) (ψ.comp ψ')) f ≫
          Iso.hom
            ((fun (x : CatCommSqOver.{v₁, v₂, v₃, v₁₀, u₁, u₂, u₃, u₁₀} F G X) ↦
                (mkIso (x.fst.associator ψ.left ψ'.left).symm (x.snd.associator ψ.right ψ'.right).symm ⋯ :
                  obj (obj (transform X) (ψ.comp ψ')) x ≅ obj (obj (transform X) ψ ⋙ obj (transform X) ψ') x))
              y)))
      x_1)
    (NatTrans.app
      (Hom.fst
        (Iso.hom
            ((fun (x : CatCommSqOver.{v₁, v₂, v₃, v₁₀, u₁, u₂, u₃, u₁₀} F G X) ↦
                (mkIso (x.fst.associator ψ.left ψ'.left).symm (x.snd.associator ψ.right ψ'.right).symm ⋯ :
                  obj (obj (transform X) (ψ.comp ψ')) x ≅ obj (obj (transform X) ψ ⋙ obj (transform X) ψ') x))
              x) ≫
          map (obj (transform X) ψ ⋙ obj (transform X) ψ') 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₁
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 y : CatCommSqOver.{v₁, v₂, v₃, v₁₀, u₁, u₂, u₃, u₁₀} F G X
f : x ⟶ y
x_1 : X
⊢ Eq (α :=
    (obj (obj (transform X) (ψ.comp ψ')) x).snd.obj x_1 ⟶
      (obj (obj (transform X) ψ ⋙ obj (transform X) ψ') y).snd.obj x_1)
    (NatTrans.app
      (Hom.snd
        (map (obj (transform X) (ψ.comp ψ')) f ≫
          Iso.hom
            ((fun (x : CatCommSqOver.{v₁, v₂, v₃, v₁₀, u₁, u₂, u₃, u₁₀} F G X) ↦
                (mkIso (x.fst.associator ψ.left ψ'.left).symm (x.snd.associator ψ.right ψ'.right).symm ⋯ :
                  obj (obj (transform X) (ψ.comp ψ')) x ≅ obj (obj (transform X) ψ ⋙ obj (transform X) ψ') x))
              y)))
      x_1)
    (NatTrans.app
      (Hom.snd
        (Iso.hom
            ((fun (x : CatCommSqOver.{v₁, v₂, v₃, v₁₀, u₁, u₂, u₃, u₁₀} F G X) ↦
                (mkIso (x.fst.associator ψ.left ψ'.left).symm (x.snd.associator ψ.right ψ'.right).symm ⋯ :
                  obj (obj (transform X) (ψ.comp ψ')) x ≅ obj (obj (transform X) ψ ⋙ obj (transform X) ψ') x))
              x) ≫
          map (obj (transform X) ψ ⋙ obj (transform X) ψ') 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₁
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₂
α : φ ⟶ φ'
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) (ψ ◁ α)) x)) x_1 =
      (NatTrans.app
              (Iso.hom (transformObjComp X ψ φ) ≫
                whiskerLeft (obj (transform X) ψ) (map (transform X) α) ≫ Iso.inv (transformObjComp 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) (ψ ◁ α)) x)) x_1 =
      (NatTrans.app
              (Iso.hom (transformObjComp X ψ φ) ≫
                whiskerLeft (obj (transform X) ψ) (map (transform X) α) ≫ Iso.inv (transformObjComp X ψ φ'))
              x).snd.app
        x_1
⊢ Eq (α :=
    Quiver.Hom (V := CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X ⥤ CatCommSqOver F₂ G₂ X)
      (obj (transform X) (ψ.comp φ)) (obj (transform X) (ψ.comp φ')))
    (map (transform X) (ψ ◁ α))
    (Iso.hom (transformObjComp X ψ φ) ≫
      whiskerLeft (obj (transform X) ψ) (map (transform X) α) ≫ Iso.inv (transformObjComp 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₁
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 ψ φ) ≫
              whiskerLeft (obj (transform X) ψ) (map (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 ψ φ) ≫
              whiskerLeft (obj (transform X) ψ) (map (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₂
X : Type u₇
inst_9 : Category.{v₇, u₇} X
ψ ψ' : 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) (α ▷ φ)) 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
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) (α ▷ φ)) 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
⊢ Eq (α :=
    Quiver.Hom (V := CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X ⥤ CatCommSqOver F₂ G₂ X)
      (obj (transform X) (ψ.comp φ)) (obj (transform X) (ψ'.comp φ)))
    (map (transform X) (α ▷ φ))
    (Iso.hom (transformObjComp X ψ φ) ≫
      whiskerRight (map (transform X) α) (obj (transform X) φ) ≫ Iso.inv (transformObjComp X ψ' φ))

Tactic:
ext