awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
inst_4 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
rw :
  Eq (α := X₂ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
      (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄)))
    (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
⊢ Eq (α := X₂ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := Y₂) (pushout.inl g₃ g₄)
      (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄))))
    (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
have rw₁ : Eq (α := X₂ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
  (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄))
  (CategoryStruct.comp (Y := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄) (Iso.hom (pushoutAssoc g₁ g₂ g₃ g₄)))
Tactic: rw [← Category.assoc, Iso.comp_inv_eq, Category.assoc, inr_inl_pushoutAssoc_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
inst_4 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
rw :
  Eq (α := X₂ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
      (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄)))
    (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
rw₁ :
  Eq (α := X₂ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
      (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄) (Iso.hom (pushoutAssoc g₁ g₂ g₃ g₄)))
⊢ Eq (α := X₂ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := Y₂) (pushout.inl g₃ g₄)
      (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄))))
    (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
have rw₂ : Eq (α := X₂ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
  (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄))
  (CategoryStruct.comp (Y := Y₁) (pushout.inr g₁ g₂)
    (CategoryStruct.comp (Y := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄) (pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
      (Iso.hom (pushoutAssoc g₁ g₂ g₃ g₄))))
Tactic: rw [← Category.assoc, Iso.comp_inv_eq, Category.assoc, inr_inl_pushoutAssoc_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst_1 : HasPushout g₁ g₂
inst_2 : HasPushout g₃ g₄
inst_3 : HasPushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄
inst_4 : HasPushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄)
rw :
  Eq (α := X₂ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
      (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄)))
    (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
rw₁ :
  Eq (α := X₂ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
      (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄) (Iso.hom (pushoutAssoc g₁ g₂ g₃ g₄)))
rw₂ :
  Eq (α := X₂ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄))
    (CategoryStruct.comp (Y := Y₁) (pushout.inr g₁ g₂)
      (CategoryStruct.comp (Y := pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄) (Iso.hom (pushoutAssoc g₁ g₂ g₃ g₄))))
⊢ Eq (α := X₂ ⟶ pushout (Y := Y₁) (g₃ ≫ pushout.inr g₁ g₂) g₄)
    (CategoryStruct.comp (Y := Y₂) (pushout.inl g₃ g₄)
      (CategoryStruct.comp (Y := pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) (Iso.inv (pushoutAssoc g₁ g₂ g₃ g₄))))
    (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
have rw₃ : Eq (α := X₂ ⟶ pushout (Z := Y₂) g₁ (g₂ ≫ pushout.inl g₃ g₄))
  (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄))
  (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄))
Tactic: rw [← Category.assoc, Iso.comp_inv_eq, Category.assoc, inr_inl_pushoutAssoc_hom]
-- 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 y : F ⊡ G
f : x ⟶ y
⊢ G.map f.snd ≫ y.iso.inv = x.iso.inv ≫ F.map f.fst
have rw : G.map f.snd = (x.iso.inv ≫ F.map f.fst) ≫ y.iso.hom
Tactic: rw [Iso.comp_inv_eq, Category.assoc, Eq.comm, Iso.inv_comp_eq, f.w]
-- 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 y : F ⊡ G
f : x ⟶ y
rw : G.map f.snd = (x.iso.inv ≫ F.map f.fst) ≫ y.iso.hom
⊢ G.map f.snd ≫ y.iso.inv = x.iso.inv ≫ F.map f.fst
have rw₁ : G.map f.snd = x.iso.inv ≫ F.map f.fst ≫ y.iso.hom
Tactic: rw [Iso.comp_inv_eq, Category.assoc, Eq.comm, Iso.inv_comp_eq, f.w]
-- 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 y : F ⊡ G
f : x ⟶ y
rw : G.map f.snd = (x.iso.inv ≫ F.map f.fst) ≫ y.iso.hom
rw₁ : G.map f.snd = x.iso.inv ≫ F.map f.fst ≫ y.iso.hom
⊢ G.map f.snd ≫ y.iso.inv = x.iso.inv ≫ F.map f.fst
have rw₂ : x.iso.inv ≫ F.map f.fst ≫ y.iso.hom = G.map f.snd
Tactic: rw [Iso.comp_inv_eq, Category.assoc, Eq.comm, Iso.inv_comp_eq, f.w]
-- 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 y : F ⊡ G
f : x ⟶ y
rw : G.map f.snd = (x.iso.inv ≫ F.map f.fst) ≫ y.iso.hom
rw₁ : G.map f.snd = x.iso.inv ≫ F.map f.fst ≫ y.iso.hom
rw₂ : x.iso.inv ≫ F.map f.fst ≫ y.iso.hom = G.map f.snd
⊢ G.map f.snd ≫ y.iso.inv = x.iso.inv ≫ F.map f.fst
have rw₃ : F.map f.fst ≫ y.iso.hom = x.iso.hom ≫ G.map f.snd
Tactic: rw [Iso.comp_inv_eq, Category.assoc, Eq.comm, Iso.inv_comp_eq, f.w]
-- 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 y : F ⊡ G
f : x ⟶ y
rw : G.map f.snd = (x.iso.inv ≫ F.map f.fst) ≫ y.iso.hom
rw₁ : G.map f.snd = x.iso.inv ≫ F.map f.fst ≫ y.iso.hom
rw₂ : x.iso.inv ≫ F.map f.fst ≫ y.iso.hom = G.map f.snd
rw₃ : F.map f.fst ≫ y.iso.hom = x.iso.hom ≫ G.map f.snd
⊢ G.map f.snd ≫ y.iso.inv = x.iso.inv ≫ F.map f.fst
have rw₄ : x.iso.hom ≫ G.map f.snd = x.iso.hom ≫ G.map f.snd
Tactic: rw [Iso.comp_inv_eq, Category.assoc, Eq.comm, Iso.inv_comp_eq, f.w]
-- 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 y : F ⊡ G
f : x ⟶ y
inst_3 : IsIso f
⊢ (inv f).fst = inv f.fst
have symm : inv f.fst = (inv f).fst
Tactic: symm
-- 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 y : F ⊡ G
f : x ⟶ y
inst_3 : IsIso f
⊢ inv f.fst = (inv f).fst
have hom_inv_id : f.fst ≫ (inv f).fst = 𝟙 x.fst
Tactic: apply IsIso.inv_eq_of_hom_inv_id
-- 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 y : F ⊡ G
f : x ⟶ y
inst_3 : IsIso f
⊢ (inv f).snd = inv f.snd
have symm : inv f.snd = (inv f).snd
Tactic: symm
-- 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 y : F ⊡ G
f : x ⟶ y
inst_3 : IsIso f
⊢ inv f.snd = (inv f).snd
have hom_inv_id : f.snd ≫ (inv f).snd = 𝟙 x.snd
Tactic: apply IsIso.inv_eq_of_hom_inv_id
-- 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
S S' : CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X
eₗ : S.fst ≅ S'.fst
eᵣ : S.snd ≅ S'.snd
w : whiskerRight eₗ.hom F ≫ S'.iso.hom = S.iso.hom ≫ whiskerRight eᵣ.hom G
⊢ whiskerRight eₗ.inv F ≫ S.iso.hom = S'.iso.hom ≫ whiskerRight eᵣ.inv G
have w₁ : ∀ (t : X), (whiskerRight eₗ.inv F ≫ S.iso.hom).app t = (S'.iso.hom ≫ whiskerRight eᵣ.inv G).app t
Tactic: ext t
-- 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
X_1 : X ⥤ F ⊡ G
⊢ { fst := whiskerRight (𝟙 X_1) (π₁ F G), snd := whiskerRight (𝟙 X_1) (π₂ F G), w := ⋯ } =
    𝟙
      { fst := X_1 ⋙ π₁ F G, snd := X_1 ⋙ π₂ F G,
        iso :=
          X_1.associator (π₁ F G) F ≪≫
            X_1.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (X_1.associator (π₂ F G) G).symm :
        CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }
have h₁ : ∀ (x : X),
  NatTrans.app
      (CatCommSqOver.Hom.fst { fst := whiskerRight (𝟙 X_1) (π₁ F G), snd := whiskerRight (𝟙 X_1) (π₂ F G), w := sorry }) x =
    (CatCommSqOver.Hom.fst
          (𝟙
            { fst := X_1 ⋙ π₁ F G, snd := X_1 ⋙ π₂ F G,
              iso :=
                X_1.associator (π₁ F G) F ≪≫
                  X_1.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (X_1.associator (π₂ F G) 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₄
inst_3 : Category.{v₄, u₄} X
X_1 : X ⥤ F ⊡ G
h₁ :
  ∀ (x : X),
    NatTrans.app
        (CatCommSqOver.Hom.fst { fst := whiskerRight (𝟙 X_1) (π₁ F G), snd := whiskerRight (𝟙 X_1) (π₂ F G), w := ⋯ })
        x =
      (CatCommSqOver.Hom.fst
            (𝟙
              { fst := X_1 ⋙ π₁ F G, snd := X_1 ⋙ π₂ F G,
                iso :=
                  X_1.associator (π₁ F G) F ≪≫
                    X_1.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (X_1.associator (π₂ F G) G).symm :
                CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X })).app
        x
⊢ { fst := whiskerRight (𝟙 X_1) (π₁ F G), snd := whiskerRight (𝟙 X_1) (π₂ F G), w := ⋯ } =
    𝟙
      { fst := X_1 ⋙ π₁ F G, snd := X_1 ⋙ π₂ F G,
        iso :=
          X_1.associator (π₁ F G) F ≪≫
            X_1.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (X_1.associator (π₂ F G) G).symm :
        CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }
have h₂ : ∀ (x : X),
  NatTrans.app
      (CatCommSqOver.Hom.snd { fst := whiskerRight (𝟙 X_1) (π₁ F G), snd := whiskerRight (𝟙 X_1) (π₂ F G), w := sorry }) x =
    (CatCommSqOver.Hom.snd
          (𝟙
            { fst := X_1 ⋙ π₁ F G, snd := X_1 ⋙ π₂ F G,
              iso :=
                X_1.associator (π₁ F G) F ≪≫
                  X_1.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (X_1.associator (π₂ F G) 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₄
inst_3 : Category.{v₄, u₄} X
X_1 Y Z : X ⥤ F ⊡ G
f : X_1 ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    { fst := X_1 ⋙ π₁ F G, snd := X_1 ⋙ π₂ F G,
        iso :=
          X_1.associator (π₁ F G) F ≪≫
            X_1.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (X_1.associator (π₂ F G) G).symm :
        CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X } ⟶
      { fst := Z ⋙ π₁ F G, snd := Z ⋙ π₂ F G,
        iso :=
          Z.associator (π₁ F G) F ≪≫
            Z.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (Z.associator (π₂ F G) G).symm })
    { fst := whiskerRight (f ≫ g) (π₁ F G), snd := whiskerRight (f ≫ g) (π₂ F G), w := ⋯ }
    (CategoryStruct.comp (Y :=
      { fst := Y ⋙ π₁ F G, snd := Y ⋙ π₂ F G,
        iso :=
          Y.associator (π₁ F G) F ≪≫
            Y.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (Y.associator (π₂ F G) G).symm })
      { fst := whiskerRight f (π₁ F G), snd := whiskerRight f (π₂ F G), w := ⋯ }
      { fst := whiskerRight g (π₁ F G), snd := whiskerRight g (π₂ F G), w := ⋯ })
have h₁ : ∀ (x : X),
  Eq.{v₁ + 1} (α :=
    { fst := X_1 ⋙ π₁ F G, snd := X_1 ⋙ π₂ F G,
              iso :=
                X_1.associator (π₁ F G) F ≪≫
                  X_1.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (X_1.associator (π₂ F G) G).symm :
              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }.fst.obj
        x ⟶
      { fst := Z ⋙ π₁ F G, snd := Z ⋙ π₂ F G,
              iso :=
                Z.associator (π₁ F G) F ≪≫
                  Z.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (Z.associator (π₂ F G) G).symm :
              CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X }.fst.obj
        x)
    (NatTrans.app
      (CatCommSqOver.Hom.fst { fst := whiskerRight (f ≫ g) (π₁ F G), snd := whiskerRight (f ≫ g) (π₂ F G), w := sorry }) x)
    (NatTrans.app
      (CatCommSqOver.Hom.fst
        (CategoryStruct.comp (Y :=
          { fst := Y ⋙ π₁ F G, snd := Y ⋙ π₂ F G,
            iso :=
              Y.associator (π₁ F G) F ≪≫
                Y.isoWhiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G) ≪≫ (Y.associator (π₂ F G) G).symm })
          { fst := whiskerRight f (π₁ F G), snd := whiskerRight f (π₂ F G), w := sorry }
          { fst := whiskerRight g (π₁ F G), snd := whiskerRight g (π₂ F G), w := 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
X_1 Y : X ⥤ F ⊡ G
f : X_1 ⟶ Y
⊢ Eq (α := obj (𝟭 (X ⥤ F ⊡ G)) X_1 ⟶ obj (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X) Y)
    (map (𝟭 (X ⥤ F ⊡ G)) f ≫
      Iso.hom
        ((fun (x : X ⥤ F ⊡ G) ↦
            NatIso.ofComponents
              (fun (x_1 : X) ↦
                mkIso (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).fst) (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).snd)
                  ⋯)
              ⋯)
          Y))
    (Iso.hom
        ((fun (x : X ⥤ F ⊡ G) ↦
            NatIso.ofComponents
              (fun (x_1 : X) ↦
                mkIso (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).fst) (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).snd)
                  ⋯)
              ⋯)
          X_1) ≫
      map (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X) f)
have w : ∀ (x : X),
  Eq (α :=
    ((obj (𝟭 (X ⥤ F ⊡ G)) X_1).obj x).fst ⟶
      ((obj (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X) Y).obj x).fst)
    (Hom.fst
      (NatTrans.app
        (map (𝟭 (X ⥤ F ⊡ G)) f ≫
          Iso.hom
            ((fun (x : X ⥤ F ⊡ G) ↦
                NatIso.ofComponents
                  (fun (x_1 : X) ↦
                    mkIso (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).fst)
                      (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).snd) sorry)
                  sorry)
              Y))
        x))
    (Hom.fst
      (NatTrans.app
        (Iso.hom
            ((fun (x : X ⥤ F ⊡ G) ↦
                NatIso.ofComponents
                  (fun (x_1 : X) ↦
                    mkIso (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).fst)
                      (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).snd) sorry)
                  sorry)
              X_1) ≫
          map (toCatCommSqOver F G X ⋙ CatCommSqOver.toFunctorToCategoricalPullback F G X) f)
        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
x : CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X
⊢ whiskerRight
        (NatIso.ofComponents
            (fun (x_1 : X) ↦
              Iso.refl
                ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).fst.obj x_1))
            ⋯).hom
        F ≫
      (obj (𝟭 (CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X)) x).iso.hom =
    (obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).iso.hom ≫
      whiskerRight
        (NatIso.ofComponents
            (fun (x_1 : X) ↦
              Iso.refl
                ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).snd.obj x_1))
            ⋯).hom
        G
have w : ∀ (x_1 : X),
  (whiskerRight
            (NatIso.ofComponents
                (fun (x_2 : X) ↦
                  Iso.refl
                    ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).fst.obj x_2))
                sorry).hom
            F ≫
          (obj (𝟭 (CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X)) x).iso.hom).app
      x_1 =
    ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).iso.hom ≫
          whiskerRight
            (NatIso.ofComponents
                (fun (x_2 : X) ↦
                  Iso.refl
                    ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).snd.obj x_2))
                sorry).hom
            G).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₄
inst_3 : Category.{v₄, u₄} X
X_1 : X ⥤ F ⊡ G
⊢ map (toCatCommSqOver F G X)
        (NatTrans.app
          (Iso.hom
            (NatIso.ofComponents
              (fun (x : X ⥤ F ⊡ G) ↦
                NatIso.ofComponents
                  (fun (x_1 : X) ↦
                    mkIso (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).fst)
                      (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).snd) ⋯)
                  ⋯)
              ⋯))
          X_1) ≫
      NatTrans.app
        (Iso.hom
          (NatIso.ofComponents
            (fun (x : CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X) ↦
              CatCommSqOver.mkIso
                (NatIso.ofComponents
                  (fun (x_1 : X) ↦
                    Iso.refl
                      ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).fst.obj
                        x_1))
                  ⋯)
                (NatIso.ofComponents
                  (fun (x_1 : X) ↦
                    Iso.refl
                      ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).snd.obj
                        x_1))
                  ⋯)
                ⋯)
            ⋯))
        (obj (toCatCommSqOver F G X) X_1) =
    𝟙 (obj (toCatCommSqOver F G X) X_1)
have h₁ : ∀ (x : X),
  NatTrans.app
      (CatCommSqOver.Hom.fst
        (map (toCatCommSqOver F G X)
            (NatTrans.app
              (Iso.hom
                (NatIso.ofComponents
                  (fun (x : X ⥤ F ⊡ G) ↦
                    NatIso.ofComponents
                      (fun (x_1 : X) ↦
                        mkIso (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).fst)
                          (Iso.refl ((obj (𝟭 (X ⥤ F ⊡ G)) x).obj x_1).snd) sorry)
                      sorry)
                  sorry))
              X_1) ≫
          NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (x : CatCommSqOver.{v₁, v₂, v₃, v₄, u₁, u₂, u₃, u₄} F G X) ↦
                  CatCommSqOver.mkIso
                    (NatIso.ofComponents
                      (fun (x_1 : X) ↦
                        Iso.refl
                          ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).fst.obj
                            x_1))
                      sorry)
                    (NatIso.ofComponents
                      (fun (x_1 : X) ↦
                        Iso.refl
                          ((obj (CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X) x).snd.obj
                            x_1))
                      sorry)
                    sorry)
                sorry))
            (obj (toCatCommSqOver F G X) X_1)))
      x =
    (CatCommSqOver.Hom.fst (𝟙 (obj (toCatCommSqOver F G X) X_1))).app x
Tactic: ext