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₁₀
Y : Type u₁₁
inst_9 : Category.{v₁₀, u₁₀} X
inst_10 : Category.{v₁₁, u₁₁} Y
U : Functor.{v₁₀, v₁₁, u₁₀, u₁₁} X Y
ψ : CatCospanTransform F G F₁ G₁
ψ' : CatCospanTransform F₁ G₁ F₂ G₂
x : CatCommSqOver.{v₁, v₂, v₃, v₁₁, u₁, u₂, u₃, u₁₁} F G Y
x_1 : X
⊢ NatTrans.app
      (Hom.fst
        (NatTrans.app
          (Iso.hom
              (CatCommSq.iso (obj (transform Y) (ψ.comp ψ')) (obj (precompose F G) U) (obj (precompose F₂ G₂) U)
                (obj (transform X) (ψ.comp ψ'))) ≫
            (obj (precompose F G) U).whiskerLeft (Iso.hom (transformObjComp X ψ ψ')))
          x))
      x_1 =
    NatTrans.app
      ((whiskerRight (Iso.hom (transformObjComp Y ψ ψ')) (obj (precompose F₂ G₂) U) ≫
              Iso.hom (associator (obj (transform Y) ψ) (obj (transform Y) ψ') (obj (precompose F₂ G₂) U)) ≫
                whiskerLeft (obj (transform Y) ψ)
                    (Iso.hom
                      (CatCommSq.iso (obj (transform Y) ψ') (obj (precompose F₁ G₁) U) (obj (precompose F₂ G₂) U)
                        (obj (transform X) ψ'))) ≫
                  Iso.inv (associator (obj (transform Y) ψ) (obj (precompose F₁ G₁) U) (obj (transform X) ψ')) ≫
                    whiskerRight
                        (Iso.hom
                          (CatCommSq.iso (obj (transform Y) ψ) (obj (precompose F G) U) (obj (precompose F₁ G₁) U)
                            (obj (transform X) ψ)))
                        (obj (transform X) ψ') ≫
                      ((obj (precompose F G) U).associator (obj (transform X) ψ) (obj (transform X) ψ')).hom).app
          x).fst
      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₁₀
Y : Type u₁₁
inst_9 : Category.{v₁₀, u₁₀} X
inst_10 : Category.{v₁₁, u₁₁} Y
U : Functor.{v₁₀, v₁₁, u₁₀, u₁₁} X Y
ψ : CatCospanTransform F G F₁ G₁
ψ' : CatCospanTransform F₁ G₁ F₂ G₂
x : CatCommSqOver.{v₁, v₂, v₃, v₁₁, u₁, u₂, u₃, u₁₁} F G Y
x_1 : X
⊢ NatTrans.app
      (Hom.snd
        (NatTrans.app
          (Iso.hom
              (CatCommSq.iso (obj (transform Y) (ψ.comp ψ')) (obj (precompose F G) U) (obj (precompose F₂ G₂) U)
                (obj (transform X) (ψ.comp ψ'))) ≫
            (obj (precompose F G) U).whiskerLeft (Iso.hom (transformObjComp X ψ ψ')))
          x))
      x_1 =
    NatTrans.app
      ((whiskerRight (Iso.hom (transformObjComp Y ψ ψ')) (obj (precompose F₂ G₂) U) ≫
              Iso.hom (associator (obj (transform Y) ψ) (obj (transform Y) ψ') (obj (precompose F₂ G₂) U)) ≫
                whiskerLeft (obj (transform Y) ψ)
                    (Iso.hom
                      (CatCommSq.iso (obj (transform Y) ψ') (obj (precompose F₁ G₁) U) (obj (precompose F₂ G₂) U)
                        (obj (transform X) ψ'))) ≫
                  Iso.inv (associator (obj (transform Y) ψ) (obj (precompose F₁ G₁) U) (obj (transform X) ψ')) ≫
                    whiskerRight
                        (Iso.hom
                          (CatCommSq.iso (obj (transform Y) ψ) (obj (precompose F G) U) (obj (precompose F₁ G₁) U)
                            (obj (transform X) ψ)))
                        (obj (transform X) ψ') ≫
                      ((obj (precompose F G) U).associator (obj (transform X) ψ) (obj (transform X) ψ')).hom).app
          x).snd
      x_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
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
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'
ψ ψ' : CatCospanTransform F G F' G'
θ θ' : ψ ⟶ ψ'
hl : θ.left = θ'.left
hr : θ.right = θ'.right
hb : θ.base = θ'.base
left : θ.left = θ'.left
right : θ.right = θ'.right
base : θ.base = θ'.base
⊢ θ = θ'

Tactic:
apply CatCospanTransformMorphism.ext

Premises used: CategoryTheory.Limits.CatCospanTransformMorphism.ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
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
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'
ψ ψ' : CatCospanTransform F G F' G'
θ θ' : ψ ⟶ ψ'
hl : θ.left = θ'.left
hr : θ.right = θ'.right
hb : θ.base = θ'.base
⊢ θ.left = θ'.left

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
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
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'
ψ ψ' : CatCospanTransform F G F' G'
θ θ' : ψ ⟶ ψ'
hl : θ.left = θ'.left
hr : θ.right = θ'.right
hb : θ.base = θ'.base
⊢ θ.right = θ'.right

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
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
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'
ψ ψ' : CatCospanTransform F G F' G'
θ θ' : ψ ⟶ ψ'
hl : θ.left = θ'.left
hr : θ.right = θ'.right
hb : θ.base = θ'.base
⊢ θ.base = θ'.base

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
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
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'
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
x : A
⊢ (CatCommSq.iso F ψ.left ψ.base F').hom.app x ≫ F'.map (α.left.app x) =
    α.base.app (F.obj x) ≫ (CatCommSq.iso F ψ'.left ψ'.base F').hom.app x

Tactic:
congr_app α.left_coherence x

Premises used: CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence, CategoryTheory.congr_app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
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
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'
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
x : C
⊢ (CatCommSq.iso G ψ.right ψ.base G').hom.app x ≫ G'.map (α.right.app x) =
    α.base.app (G.obj x) ≫ (CatCommSq.iso G ψ'.right ψ'.base G').hom.app x

Tactic:
congr_app α.right_coherence x

Premises used: CategoryTheory.congr_app, CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
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'
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''
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
w :
  ∀ (x : A),
    ((CatCommSq.iso F (ψ.comp φ).left (ψ.comp φ).base F'').hom ≫
            Functor.whiskerRight (Functor.whiskerRight α.left φ.left) F'').app
        x =
      (F.whiskerLeft (Functor.whiskerRight α.base φ.base) ≫
            (CatCommSq.iso F (ψ'.comp φ).left (ψ'.comp φ).base F'').hom).app
        x
⊢ (CatCommSq.iso F (ψ.comp φ).left (ψ.comp φ).base F'').hom ≫
      Functor.whiskerRight (Functor.whiskerRight α.left φ.left) F'' =
    F.whiskerLeft (Functor.whiskerRight α.base φ.base) ≫ (CatCommSq.iso F (ψ'.comp φ).left (ψ'.comp φ).base F'').hom

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
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'
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''
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
x : A
w :
  (CatCommSq.iso F (ψ.left ⋙ φ.left) (ψ.base ⋙ φ.base) F'').hom.app x ≫ F''.map (φ.left.map (α.left.app x)) =
    φ.base.map (α.base.app (F.obj x)) ≫ (CatCommSq.iso F (ψ'.left ⋙ φ.left) (ψ'.base ⋙ φ.base) F'').hom.app x
⊢ ((CatCommSq.iso F (ψ.comp φ).left (ψ.comp φ).base F'').hom ≫
          Functor.whiskerRight (Functor.whiskerRight α.left φ.left) F'').app
      x =
    (F.whiskerLeft (Functor.whiskerRight α.base φ.base) ≫
          (CatCommSq.iso F (ψ'.comp φ).left (ψ'.comp φ).base F'').hom).app
      x

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
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'
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''
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
x : A
w :
  φ.base.map ((CatCommSq.iso F ψ.left ψ.base F').hom.app x) ≫
      (CatCommSq.iso F' φ.left φ.base F'').hom.app (ψ.left.obj x) ≫ F''.map (φ.left.map (α.left.app x)) =
    φ.base.map (α.base.app (F.obj x)) ≫
      φ.base.map ((CatCommSq.iso F ψ'.left ψ'.base F').hom.app x) ≫
        (CatCommSq.iso F' φ.left φ.base F'').hom.app (ψ'.left.obj x)
⊢ (CatCommSq.iso F (ψ.left ⋙ φ.left) (ψ.base ⋙ φ.base) F'').hom.app x ≫ F''.map (φ.left.map (α.left.app x)) =
    φ.base.map (α.base.app (F.obj x)) ≫ (CatCommSq.iso F (ψ'.left ⋙ φ.left) (ψ'.base ⋙ φ.base) F'').hom.app x

Tactic:
simp only [CatCommSq.vComp_iso_hom_app, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.CatCommSq.vComp_iso_hom_app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
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'
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''
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
x : A
w :
  φ.base.map ((CatCommSq.iso F ψ.left ψ.base F').hom.app x) ≫
      (CatCommSq.iso F' φ.left φ.base F'').hom.app (ψ.left.obj x) ≫ F''.map (φ.left.map (α.left.app x)) =
    φ.base.map ((CatCommSq.iso F ψ.left ψ.base F').hom.app x) ≫
      φ.base.map (F'.map (α.left.app x)) ≫ (CatCommSq.iso F' φ.left φ.base F'').hom.app (ψ'.left.obj x)
⊢ φ.base.map ((CatCommSq.iso F ψ.left ψ.base F').hom.app x) ≫
      (CatCommSq.iso F' φ.left φ.base F'').hom.app (ψ.left.obj x) ≫ F''.map (φ.left.map (α.left.app x)) =
    φ.base.map (α.base.app (F.obj x)) ≫
      φ.base.map ((CatCommSq.iso F ψ'.left ψ'.base F').hom.app x) ≫
        (CatCommSq.iso F' φ.left φ.base F'').hom.app (ψ'.left.obj x)

Tactic:
rw [← Functor.map_comp_assoc, ← left_coherence_app, Functor.map_comp_assoc]

Premises used: CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence_app, CategoryTheory.Functor.map_comp_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
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'
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''
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
x : A
⊢ φ.base.map ((CatCommSq.iso F ψ.left ψ.base F').hom.app x) ≫
      (CatCommSq.iso F' φ.left φ.base F'').hom.app (ψ.left.obj x) ≫ F''.map (φ.left.map (α.left.app x)) =
    φ.base.map ((CatCommSq.iso F ψ.left ψ.base F').hom.app x) ≫
      φ.base.map (F'.map (α.left.app x)) ≫ (CatCommSq.iso F' φ.left φ.base F'').hom.app (ψ'.left.obj x)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
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'
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''
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
w :
  ∀ (x : C),
    ((CatCommSq.iso G (ψ.comp φ).right (ψ.comp φ).base G'').hom ≫
            Functor.whiskerRight (Functor.whiskerRight α.right φ.right) G'').app
        x =
      (G.whiskerLeft (Functor.whiskerRight α.base φ.base) ≫
            (CatCommSq.iso G (ψ'.comp φ).right (ψ'.comp φ).base G'').hom).app
        x
⊢ (CatCommSq.iso G (ψ.comp φ).right (ψ.comp φ).base G'').hom ≫
      Functor.whiskerRight (Functor.whiskerRight α.right φ.right) G'' =
    G.whiskerLeft (Functor.whiskerRight α.base φ.base) ≫ (CatCommSq.iso G (ψ'.comp φ).right (ψ'.comp φ).base G'').hom

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
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'
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''
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
x : C
w :
  (CatCommSq.iso G (ψ.right ⋙ φ.right) (ψ.base ⋙ φ.base) G'').hom.app x ≫ G''.map (φ.right.map (α.right.app x)) =
    φ.base.map (α.base.app (G.obj x)) ≫ (CatCommSq.iso G (ψ'.right ⋙ φ.right) (ψ'.base ⋙ φ.base) G'').hom.app x
⊢ ((CatCommSq.iso G (ψ.comp φ).right (ψ.comp φ).base G'').hom ≫
          Functor.whiskerRight (Functor.whiskerRight α.right φ.right) G'').app
      x =
    (G.whiskerLeft (Functor.whiskerRight α.base φ.base) ≫
          (CatCommSq.iso G (ψ'.comp φ).right (ψ'.comp φ).base G'').hom).app
      x

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
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'
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''
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
x : C
w :
  φ.base.map ((CatCommSq.iso G ψ.right ψ.base G').hom.app x) ≫
      (CatCommSq.iso G' φ.right φ.base G'').hom.app (ψ.right.obj x) ≫ G''.map (φ.right.map (α.right.app x)) =
    φ.base.map (α.base.app (G.obj x)) ≫
      φ.base.map ((CatCommSq.iso G ψ'.right ψ'.base G').hom.app x) ≫
        (CatCommSq.iso G' φ.right φ.base G'').hom.app (ψ'.right.obj x)
⊢ (CatCommSq.iso G (ψ.right ⋙ φ.right) (ψ.base ⋙ φ.base) G'').hom.app x ≫ G''.map (φ.right.map (α.right.app x)) =
    φ.base.map (α.base.app (G.obj x)) ≫ (CatCommSq.iso G (ψ'.right ⋙ φ.right) (ψ'.base ⋙ φ.base) G'').hom.app x

Tactic:
simp only [CatCommSq.vComp_iso_hom_app, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.CatCommSq.vComp_iso_hom_app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
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'
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''
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
x : C
w :
  φ.base.map ((CatCommSq.iso G ψ.right ψ.base G').hom.app x) ≫
      (CatCommSq.iso G' φ.right φ.base G'').hom.app (ψ.right.obj x) ≫ G''.map (φ.right.map (α.right.app x)) =
    φ.base.map ((CatCommSq.iso G ψ.right ψ.base G').hom.app x) ≫
      φ.base.map (G'.map (α.right.app x)) ≫ (CatCommSq.iso G' φ.right φ.base G'').hom.app (ψ'.right.obj x)
⊢ φ.base.map ((CatCommSq.iso G ψ.right ψ.base G').hom.app x) ≫
      (CatCommSq.iso G' φ.right φ.base G'').hom.app (ψ.right.obj x) ≫ G''.map (φ.right.map (α.right.app x)) =
    φ.base.map (α.base.app (G.obj x)) ≫
      φ.base.map ((CatCommSq.iso G ψ'.right ψ'.base G').hom.app x) ≫
        (CatCommSq.iso G' φ.right φ.base G'').hom.app (ψ'.right.obj x)

Tactic:
rw [← Functor.map_comp_assoc, ← right_coherence_app, Functor.map_comp_assoc]

Premises used: CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence_app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
Goal:
A : Type u₁
B : Type u₂
C : Type u₃
A' : Type u₄
B' : Type u₅
C' : Type u₆
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
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'
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''
ψ ψ' : CatCospanTransform F G F' G'
α : ψ ⟶ ψ'
φ : CatCospanTransform F' G' F'' G''
x : C
⊢ φ.base.map ((CatCommSq.iso G ψ.right ψ.base G').hom.app x) ≫
      (CatCommSq.iso G' φ.right φ.base G'').hom.app (ψ.right.obj x) ≫ G''.map (φ.right.map (α.right.app x)) =
    φ.base.map ((CatCommSq.iso G ψ.right ψ.base G').hom.app x) ≫
      φ.base.map (G'.map (α.right.app x)) ≫ (CatCommSq.iso G' φ.right φ.base G'').hom.app (ψ'.right.obj x)

Tactic:
simp