awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic (goal)
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
⊢ 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 ψ' φ))
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic (goal)
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₃
⊢ 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 τ)))
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic (goal)
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
⊢ 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 τ)))
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic (goal)
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₁
⊢ 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) ψ)))
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic (goal)
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
⊢ 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) ψ)))
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic (goal)
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₁
⊢ 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) ψ)))
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic (goal)
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
⊢ 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) ψ)))
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic (goal)
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
⊢ { 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 }
have h₁ : ∀ (x : X),
  NatTrans.app (Hom.fst { fst := U.whiskerLeft (Hom.fst (𝟙 X_1)), snd := U.whiskerLeft (Hom.snd (𝟙 X_1)), w := sorry }) 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: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic (goal)
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
⊢ { 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 }
have h₂ : ∀ (x : X),
  NatTrans.app (Hom.snd { fst := U.whiskerLeft (Hom.fst (𝟙 X_1)), snd := U.whiskerLeft (Hom.snd (𝟙 X_1)), w := sorry }) 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: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic (goal)
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
⊢ 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
have 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: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic (goal)
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
⊢ 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
have 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: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic (goal)
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
⊢ 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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic (goal)
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
⊢ 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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic (goal)
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
⊢ 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
have 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
Tactic: ext