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₁
X : Type u₇
Y : Type u₈
inst_6 : Category.{v₇, u₇} X
inst_7 : Category.{v₈, u₈} Y
U : Functor.{v₇, v₈, u₇, u₈} X Y
ψ ψ' : CatCospanTransform F G F₁ G₁
η : ψ ⟶ ψ'
w :
  ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₈, u₁, u₂, u₃, u₈} F G Y) (x_1 : X),
    Eq (α :=
      ((obj (transform Y) ψ ⋙ obj (precompose F₁ G₁) U).obj x).fst.obj x_1 ⟶
        ((obj (precompose F G) U ⋙ obj (transform X) ψ').obj x).fst.obj x_1)
      (NatTrans.app
        (Hom.fst
          (NatTrans.app
            (whiskerRight (map (transform Y) η) (obj (precompose F₁ G₁) U) ≫
              Iso.hom
                (CatCommSq.iso (obj (transform Y) ψ') (obj (precompose F G) U) (obj (precompose F₁ G₁) U)
                  (obj (transform X) ψ')))
            x))
        x_1)
      (NatTrans.app
        (Hom.fst
          (NatTrans.app
            (Iso.hom
                (CatCommSq.iso (obj (transform Y) ψ) (obj (precompose F G) U) (obj (precompose F₁ G₁) U)
                  (obj (transform X) ψ)) ≫
              (obj (precompose F G) U).whiskerLeft (map (transform X) η))
            x))
        x_1)
⊢ Eq (α := obj (transform Y) ψ ⋙ obj (precompose F₁ G₁) U ⟶ obj (precompose F G) U ⋙ obj (transform X) ψ')
    (whiskerRight (map (transform Y) η) (obj (precompose F₁ G₁) U) ≫
      Iso.hom
        (CatCommSq.iso (obj (transform Y) ψ') (obj (precompose F G) U) (obj (precompose F₁ G₁) U)
          (obj (transform X) ψ')))
    (Iso.hom
        (CatCommSq.iso (obj (transform Y) ψ) (obj (precompose F G) U) (obj (precompose F₁ G₁) U)
          (obj (transform X) ψ)) ≫
      (obj (precompose F G) U).whiskerLeft (map (transform X) η))
have w₁ : ∀ (x : CatCommSqOver.{v₁, v₂, v₃, v₈, u₁, u₂, u₃, u₈} F G Y) (x_1 : X),
  Eq (α :=
    ((obj (transform Y) ψ ⋙ obj (precompose F₁ G₁) U).obj x).snd.obj x_1 ⟶
      ((obj (precompose F G) U ⋙ obj (transform X) ψ').obj x).snd.obj x_1)
    (NatTrans.app
      (Hom.snd
        (NatTrans.app
          (whiskerRight (map (transform Y) η) (obj (precompose F₁ G₁) U) ≫
            Iso.hom
              (CatCommSq.iso (obj (transform Y) ψ') (obj (precompose F G) U) (obj (precompose F₁ G₁) U)
                (obj (transform X) ψ')))
          x))
      x_1)
    (NatTrans.app
      (Hom.snd
        (NatTrans.app
          (Iso.hom
              (CatCommSq.iso (obj (transform Y) ψ) (obj (precompose F G) U) (obj (precompose F₁ G₁) U)
                (obj (transform X) ψ)) ≫
            (obj (precompose F G) U).whiskerLeft (map (transform X) η))
          x))
      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
X : Type u₇
Y : Type u₈
inst_3 : Category.{v₇, u₇} X
inst_4 : Category.{v₈, u₈} Y
U : Functor.{v₇, v₈, u₇, u₈} X Y
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
⊢ Iso.hom
        (CatCommSq.iso (obj (transform Y) (CatCospanTransform.id F G)) (obj (precompose F G) U) (obj (precompose F G) U)
          (obj (transform X) (CatCospanTransform.id F G))) ≫
      (obj (precompose F G) U).whiskerLeft (Iso.hom (transformObjId X F G)) =
    whiskerRight (Iso.hom (transformObjId Y F G)) (obj (precompose F G) U) ≫
      (obj (precompose F G) U).leftUnitor.hom ≫ (obj (precompose F G) U).rightUnitor.inv
have w : ∀ (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) (CatCospanTransform.id F G)) (obj (precompose F G) U)
                (obj (precompose F G) U) (obj (transform X) (CatCospanTransform.id F G))) ≫
            (obj (precompose F G) U).whiskerLeft (Iso.hom (transformObjId X F G)))
          x))
      x_1 =
    ((whiskerRight (Iso.hom (transformObjId Y F G)) (obj (precompose F G) U) ≫
                (obj (precompose F G) U).leftUnitor.hom ≫ (obj (precompose F G) U).rightUnitor.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
X : Type u₇
Y : Type u₈
inst_3 : Category.{v₇, u₇} X
inst_4 : Category.{v₈, u₈} Y
U : Functor.{v₇, v₈, u₇, u₈} X Y
F : Functor.{v₁, v₂, u₁, u₂} A B
G : Functor.{v₃, v₂, u₃, u₂} C B
w :
  ∀ (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) (CatCospanTransform.id F G)) (obj (precompose F G) U)
                  (obj (precompose F G) U) (obj (transform X) (CatCospanTransform.id F G))) ≫
              (obj (precompose F G) U).whiskerLeft (Iso.hom (transformObjId X F G)))
            x))
        x_1 =
      ((whiskerRight (Iso.hom (transformObjId Y F G)) (obj (precompose F G) U) ≫
                  (obj (precompose F G) U).leftUnitor.hom ≫ (obj (precompose F G) U).rightUnitor.inv).app
              x).fst.app
        x_1
⊢ Iso.hom
        (CatCommSq.iso (obj (transform Y) (CatCospanTransform.id F G)) (obj (precompose F G) U) (obj (precompose F G) U)
          (obj (transform X) (CatCospanTransform.id F G))) ≫
      (obj (precompose F G) U).whiskerLeft (Iso.hom (transformObjId X F G)) =
    whiskerRight (Iso.hom (transformObjId Y F G)) (obj (precompose F G) U) ≫
      (obj (precompose F G) U).leftUnitor.hom ≫ (obj (precompose F G) U).rightUnitor.inv
have w₁ : ∀ (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) (CatCospanTransform.id F G)) (obj (precompose F G) U)
                (obj (precompose F G) U) (obj (transform X) (CatCospanTransform.id F G))) ≫
            (obj (precompose F G) U).whiskerLeft (Iso.hom (transformObjId X F G)))
          x))
      x_1 =
    ((whiskerRight (Iso.hom (transformObjId Y F G)) (obj (precompose F G) U) ≫
                (obj (precompose F G) U).leftUnitor.hom ≫ (obj (precompose F G) U).rightUnitor.inv).app
            x).snd.app
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform (goal)
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''
⊢ (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
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform (goal)
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
⊢ ((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
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform (goal)
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
⊢ (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
have 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)
Tactic: simp only [CatCommSq.vComp_iso_hom_app, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform (goal)
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 (α.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)
have 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)
Tactic: rw [← Functor.map_comp_assoc, ← left_coherence_app, Functor.map_comp_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform (goal)
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''
⊢ (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
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform (goal)
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
⊢ ((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
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform (goal)
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
⊢ (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
have 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)
Tactic: simp only [CatCommSq.vComp_iso_hom_app, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform (goal)
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 (α.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)
have 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)
Tactic: rw [← Functor.map_comp_assoc, ← right_coherence_app, Functor.map_comp_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform (goal)
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'
f : ψ' ⟶ ψ'
inst_6 : IsIso f
⊢ inv f.left = (inv f).left
have symm : (inv f).left = inv f.left
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform (goal)
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'
f : ψ' ⟶ ψ'
inst_6 : IsIso f
⊢ (inv f).left = inv f.left
have hom_inv_id : (inv f).left ≫ f.left = 𝟙 ψ'.left
Tactic: apply IsIso.eq_inv_of_inv_hom_id
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform (goal)
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'
f : ψ' ⟶ ψ'
inst_6 : IsIso f
⊢ inv f.right = (inv f).right
have symm : (inv f).right = inv f.right
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform (goal)
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'
f : ψ' ⟶ ψ'
inst_6 : IsIso f
⊢ (inv f).right = inv f.right
have hom_inv_id : (inv f).right ≫ f.right = 𝟙 ψ'.right
Tactic: apply IsIso.eq_inv_of_inv_hom_id
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform (goal)
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'
f : ψ' ⟶ ψ'
inst_6 : IsIso f
⊢ inv f.base = (inv f).base
have symm : (inv f).base = inv f.base
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform (goal)
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'
f : ψ' ⟶ ψ'
inst_6 : IsIso f
⊢ (inv f).base = inv f.base
have hom_inv_id : (inv f).base ≫ f.base = 𝟙 ψ'.base
Tactic: apply IsIso.eq_inv_of_inv_hom_id
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform (hypothesis)
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'
f : ψ' ⟶ ψ'
h : IsIso f.left ∧ IsIso f.base ∧ IsIso f.right
⊢ IsIso f
have left : IsIso f.left
Tactic: obtain ⟨_, _, _⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform (hypothesis)
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'
f : ψ' ⟶ ψ'
h : IsIso f.left ∧ IsIso f.base ∧ IsIso f.right
left : IsIso f.left
⊢ IsIso f
have left₁ : IsIso f.base
Tactic: obtain ⟨_, _, _⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform (hypothesis)
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'
f : ψ' ⟶ ψ'
h : IsIso f.left ∧ IsIso f.base ∧ IsIso f.right
left : IsIso f.left
left₁ : IsIso f.base
⊢ IsIso f
have right : IsIso f.right
Tactic: obtain ⟨_, _, _⟩ := h
Cleared hypotheses: h