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
X : Type u₄
inst_3 : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
x x_1 : X
f : x ⟶ x_1
⊢ J.map f ≫ Iso.hom ((fun (x : X) ↦ mkIso (e₁.app x) (e₂.app x) ⋯) x_1) =
    Iso.hom ((fun (x : X) ↦ mkIso (e₁.app x) (e₂.app x) ⋯) x) ≫ K.map f
have hₗ : Hom.fst (J.map f ≫ Iso.hom ((fun (x : X) ↦ mkIso (e₁.app x) (e₂.app x) sorry) x_1)) =
  Hom.fst (Iso.hom ((fun (x : X) ↦ mkIso (e₁.app x) (e₂.app x) sorry) x) ≫ K.map f)
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₄
inst_3 : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
x x_1 : X
f : x ⟶ x_1
hₗ :
  Hom.fst (J.map f ≫ Iso.hom ((fun (x : X) ↦ mkIso (e₁.app x) (e₂.app x) ⋯) x_1)) =
    Hom.fst (Iso.hom ((fun (x : X) ↦ mkIso (e₁.app x) (e₂.app x) ⋯) x) ≫ K.map f)
⊢ J.map f ≫ Iso.hom ((fun (x : X) ↦ mkIso (e₁.app x) (e₂.app x) ⋯) x_1) =
    Iso.hom ((fun (x : X) ↦ mkIso (e₁.app x) (e₂.app x) ⋯) x) ≫ K.map f
have hᵣ : Hom.snd (J.map f ≫ Iso.hom ((fun (x : X) ↦ mkIso (e₁.app x) (e₂.app x) sorry) x_1)) =
  Hom.snd (Iso.hom ((fun (x : X) ↦ mkIso (e₁.app x) (e₂.app x) sorry) x) ≫ K.map f)
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₄
inst_3 : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
α β : J ⟶ K
e₁ : whiskerRight α (π₁ F G) = whiskerRight β (π₁ F G)
e₂ : whiskerRight α (π₂ F G) = whiskerRight β (π₂ F G)
⊢ α = β
have w : ∀ (x : X), (α.app x).fst = (β.app x).fst
Tactic: ext x
-- 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₄
inst_3 : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
α β : J ⟶ K
e₁ : whiskerRight α (π₁ F G) = whiskerRight β (π₁ F G)
e₂ : whiskerRight α (π₂ F G) = whiskerRight β (π₂ F G)
w : ∀ (x : X), (α.app x).fst = (β.app x).fst
⊢ α = β
have w₁ : ∀ (x : X), (α.app x).snd = (β.app x).snd
Tactic: ext x
-- 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₄
inst_3 : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
⊢ Eq (α := obj (toCatCommSqOver F G X) J ≅ obj (toCatCommSqOver F G X) K)
    (mapIso (toCatCommSqOver F G X) (mkNatIso e₁ e₂ coh)) (CatCommSqOver.mkIso e₁ e₂ ⋯)
have w : ∀ (x : X),
  Eq (α := (obj (toCatCommSqOver F G X) J).fst.obj x ⟶ (obj (toCatCommSqOver F G X) K).fst.obj x)
    (NatTrans.app (CatCommSqOver.Hom.fst (Iso.hom (mapIso (toCatCommSqOver F G X) (mkNatIso e₁ e₂ coh)))) x)
    (NatTrans.app (CatCommSqOver.Hom.fst (Iso.hom (CatCommSqOver.mkIso e₁ e₂ sorry))) 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₄
inst_3 : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
w :
  ∀ (x : X),
    Eq (α := (obj (toCatCommSqOver F G X) J).fst.obj x ⟶ (obj (toCatCommSqOver F G X) K).fst.obj x)
      (NatTrans.app (CatCommSqOver.Hom.fst (Iso.hom (mapIso (toCatCommSqOver F G X) (mkNatIso e₁ e₂ coh)))) x)
      (NatTrans.app (CatCommSqOver.Hom.fst (Iso.hom (CatCommSqOver.mkIso e₁ e₂ ⋯))) x)
⊢ Eq (α := obj (toCatCommSqOver F G X) J ≅ obj (toCatCommSqOver F G X) K)
    (mapIso (toCatCommSqOver F G X) (mkNatIso e₁ e₂ coh)) (CatCommSqOver.mkIso e₁ e₂ ⋯)
have w₁ : ∀ (x : X),
  Eq (α := (obj (toCatCommSqOver F G X) J).snd.obj x ⟶ (obj (toCatCommSqOver F G X) K).snd.obj x)
    (NatTrans.app (CatCommSqOver.Hom.snd (Iso.hom (mapIso (toCatCommSqOver F G X) (mkNatIso e₁ e₂ coh)))) x)
    (NatTrans.app (CatCommSqOver.Hom.snd (Iso.hom (CatCommSqOver.mkIso e₁ e₂ sorry))) 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₄
inst_3 : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
⊢ mkNatIso e₁ e₂ coh =
    FullyFaithful.preimageIso (F := Equivalence.functor (functorEquiv F G X))
      (Equivalence.fullyFaithfulFunctor (functorEquiv F G X)) (CatCommSqOver.mkIso e₁ e₂ ⋯)
have rw : mkNatIso e₁ e₂ coh =
  FullyFaithful.preimageIso (F := Equivalence.functor (functorEquiv F G X))
    (Equivalence.fullyFaithfulFunctor (functorEquiv F G X)) (mapIso (toCatCommSqOver F G X) (mkNatIso e₁ e₂ coh))
Tactic: rw [← toCatCommSqOver_mapIso_mkNatIso_eq_mkIso e₁ e₂ coh]
-- 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₄
inst_3 : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
⊢ mkNatIso e₁ e₂ coh =
    FullyFaithful.preimageIso (F := Equivalence.functor (functorEquiv F G X))
      {
        preimage :=
          fun {X_1 Y : X ⥤ F ⊡ G}
            (f :
              obj (Equivalence.functor (functorEquiv F G X)) X_1 ⟶ obj (Equivalence.functor (functorEquiv F G X)) Y) ↦
          NatTrans.app (Iso.hom (Equivalence.unitIso (functorEquiv F G X))) X_1 ≫
            map (Equivalence.inverse (functorEquiv F G X)) f ≫
              NatTrans.app (Iso.inv (Equivalence.unitIso (functorEquiv F G X))) Y,
        map_preimage := ⋯, preimage_map := ⋯ }
      (mapIso (toCatCommSqOver F G X) (mkNatIso e₁ e₂ coh))
have w : ∀ (x : X),
  (whiskerRight (mkNatIso e₁ e₂ coh).hom (π₁ F G)).app x =
    (whiskerRight
          (FullyFaithful.preimageIso (F := Equivalence.functor (functorEquiv F G X))
              {
                preimage :=
                  fun {X_1 Y : X ⥤ F ⊡ G}
                    (f :
                      obj (Equivalence.functor (functorEquiv F G X)) X_1 ⟶
                        obj (Equivalence.functor (functorEquiv F G X)) Y) ↦
                  NatTrans.app (Iso.hom (Equivalence.unitIso (functorEquiv F G X))) X_1 ≫
                    map (Equivalence.inverse (functorEquiv F G X)) f ≫
                      NatTrans.app (Iso.inv (Equivalence.unitIso (functorEquiv F G X))) Y,
                map_preimage := sorry, preimage_map := sorry }
              (mapIso (toCatCommSqOver F G X) (mkNatIso e₁ e₂ coh))).hom
          (π₁ F G)).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₄
inst_3 : Category.{v₄, u₄} X
J K : X ⥤ F ⊡ G
e₁ : J ⋙ π₁ F G ≅ K ⋙ π₁ F G
e₂ : J ⋙ π₂ F G ≅ K ⋙ π₂ F G
coh :
  whiskerRight e₁.hom F ≫
      (K.associator (π₁ F G) F).hom ≫
        K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (K.associator (π₂ F G) G).inv =
    (J.associator (π₁ F G) F).hom ≫
      J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom ≫ (J.associator (π₂ F G) G).inv ≫ whiskerRight e₂.hom G
w :
  ∀ (x : X),
    (whiskerRight (mkNatIso e₁ e₂ coh).hom (π₁ F G)).app x =
      (whiskerRight
            (FullyFaithful.preimageIso (F := Equivalence.functor (functorEquiv F G X))
                {
                  preimage :=
                    fun {X_1 Y : X ⥤ F ⊡ G}
                      (f :
                        obj (Equivalence.functor (functorEquiv F G X)) X_1 ⟶
                          obj (Equivalence.functor (functorEquiv F G X)) Y) ↦
                    NatTrans.app (Iso.hom (Equivalence.unitIso (functorEquiv F G X))) X_1 ≫
                      map (Equivalence.inverse (functorEquiv F G X)) f ≫
                        NatTrans.app (Iso.inv (Equivalence.unitIso (functorEquiv F G X))) Y,
                  map_preimage := ⋯, preimage_map := ⋯ }
                (mapIso (toCatCommSqOver F G X) (mkNatIso e₁ e₂ coh))).hom
            (π₁ F G)).app
        x
⊢ mkNatIso e₁ e₂ coh =
    FullyFaithful.preimageIso (F := Equivalence.functor (functorEquiv F G X))
      {
        preimage :=
          fun {X_1 Y : X ⥤ F ⊡ G}
            (f :
              obj (Equivalence.functor (functorEquiv F G X)) X_1 ⟶ obj (Equivalence.functor (functorEquiv F G X)) Y) ↦
          NatTrans.app (Iso.hom (Equivalence.unitIso (functorEquiv F G X))) X_1 ≫
            map (Equivalence.inverse (functorEquiv F G X)) f ≫
              NatTrans.app (Iso.inv (Equivalence.unitIso (functorEquiv F G X))) Y,
        map_preimage := ⋯, preimage_map := ⋯ }
      (mapIso (toCatCommSqOver F G X) (mkNatIso e₁ e₂ coh))
have w₁ : ∀ (x : X),
  (whiskerRight (mkNatIso e₁ e₂ coh).hom (π₂ F G)).app x =
    (whiskerRight
          (FullyFaithful.preimageIso (F := Equivalence.functor (functorEquiv F G X))
              {
                preimage :=
                  fun {X_1 Y : X ⥤ F ⊡ G}
                    (f :
                      obj (Equivalence.functor (functorEquiv F G X)) X_1 ⟶
                        obj (Equivalence.functor (functorEquiv F G X)) Y) ↦
                  NatTrans.app (Iso.hom (Equivalence.unitIso (functorEquiv F G X))) X_1 ≫
                    map (Equivalence.inverse (functorEquiv F G X)) f ≫
                      NatTrans.app (Iso.inv (Equivalence.unitIso (functorEquiv F G X))) Y,
                map_preimage := sorry, preimage_map := sorry }
              (mapIso (toCatCommSqOver F G X) (mkNatIso e₁ e₂ coh))).hom
          (π₂ F G)).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
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 y : CatCommSqOver.{v₁, v₂, v₃, v₇, u₁, u₂, u₃, u₇} F G X
f : x ⟶ y
⊢ whiskerRight (whiskerRight f.fst ψ.left) F₁ ≫
      { 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 }.iso.hom =
    { fst := x.fst ⋙ ψ.left, snd := x.snd ⋙ ψ.right,
            iso :=
              x.fst.associator ψ.left F₁ ≪≫
                x.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                  (x.fst.associator F ψ.base).symm ≪≫
                    isoWhiskerRight x.iso ψ.base ≪≫
                      x.snd.associator G ψ.base ≪≫
                        x.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫ (x.snd.associator ψ.right G₁).symm :
            CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }.iso.hom ≫
      whiskerRight (whiskerRight f.snd ψ.right) G₁
have w : ∀ (x_1 : X),
  NatTrans.app
      (whiskerRight (whiskerRight f.fst ψ.left) F₁ ≫
        { 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 }.iso.hom)
      x_1 =
    ({ fst := x.fst ⋙ ψ.left, snd := x.snd ⋙ ψ.right,
                iso :=
                  x.fst.associator ψ.left F₁ ≪≫
                    x.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫
                      (x.fst.associator F ψ.base).symm ≪≫
                        isoWhiskerRight x.iso ψ.base ≪≫
                          x.snd.associator G ψ.base ≪≫
                            x.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫
                              (x.snd.associator ψ.right G₁).symm :
                CatCommSqOver.{v₄, v₅, v₆, v₇, u₄, u₅, u₆, u₇} F₁ G₁ X }.iso.hom ≫
          whiskerRight (whiskerRight f.snd ψ.right) G₁).app
      x_1
Tactic: ext x
-- 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₂
x y : CatCommSqOver.{v₁, v₂, v₃, v₁₀, u₁, u₂, u₃, u₁₀} F G X
f : x ⟶ y
⊢ Eq (α := obj (obj (transform X) (ψ.comp ψ')) x ⟶ obj (obj (transform X) ψ ⋙ obj (transform X) ψ') y)
    (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))
    (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)
have h₁ : ∀ (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 sorry :
                  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 sorry :
                  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: 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₂
X : Type u₇
inst_9 : Category.{v₇, u₇} X
ψ : 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 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 ψ φ'))
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) (ψ ◁ α)) 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: 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₂
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
⊢ 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 ψ φ'))
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 ψ φ) ≫
              whiskerLeft (obj (transform X) ψ) (map (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₂
X : Type u₇
inst_9 : Category.{v₇, u₇} X
ψ ψ' : 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 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.fst (NatTrans.app (map (transform X) (α ▷ φ)) x)) x_1 =
    (NatTrans.app
            (Iso.hom (transformObjComp X ψ φ) ≫
              whiskerRight (map (transform X) α) (obj (transform X) φ) ≫ Iso.inv (transformObjComp X ψ' φ))
            x).fst.app
      x_1
Tactic: ext