awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v, u₂, u} J C
inst_2 : HasLimit F
inst_3 : HasProduct.{u₂, v, u} F.obj
Z : C
x x_1 : Z ⟶ limit F
h : Eq (α := Z ⟶ piObj.{u₂, v, u} F.obj) (x ≫ Pi.lift (limit.π F)) (x_1 ≫ Pi.lift (limit.π F))
⊢ x = x_1
have refine : ∀ (j : J), x ≫ limit.π F j = x_1 ≫ limit.π F j
Tactic: refine limit.hom_ext fun j => ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v, u₂, u} J C
inst_2 : HasColimit F
inst_3 : HasCoproduct.{u₂, v, u} F.obj
Z : C
x x_1 : colimit F ⟶ Z
h : Eq (α := sigmaObj.{u₂, v, u} F.obj ⟶ Z) (Sigma.desc (colimit.ι F) ≫ x) (Sigma.desc (colimit.ι F) ≫ x_1)
⊢ x = x_1
have refine : ∀ (j : J), colimit.ι F j ≫ x = colimit.ι F j ≫ x_1
Tactic: refine colimit.hom_ext fun j => ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Fan.{u_2, v, u} (C := C) fun (j : ι') ↦ X i j
hc : (i : ι) → IsLimit (c i)
c' : Fan.{u_1, v, u} (C := C) fun (i : ι) ↦ (c i).pt
hc' : IsLimit c'
⊢ IsLimit (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
    (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2)
have refine_1 : (t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) →
  t.pt ⟶
    Cone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
      (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2)
Tactic: refine Fan.IsLimit.mk _ (fun t ↦ ?_) ?_ fun t m hm ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Fan.{u_2, v, u} (C := C) fun (j : ι') ↦ X i j
hc : (i : ι) → IsLimit (c i)
c' : Fan.{u_1, v, u} (C := C) fun (i : ι) ↦ (c i).pt
hc' : IsLimit c'
refine_1 :
  (t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) →
    t.pt ⟶
      Cone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
        (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2)
⊢ IsLimit (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
    (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2)
have refine_2 : ∀ (s : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) (j : ι × ι'),
  CategoryStruct.comp (Y :=
      Cone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
        (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2))
      ((fun (t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
          (lift hc' fun (i : ι) ↦ lift (hc i) fun (j : ι') ↦ t.proj (i, j) : t.pt ⟶ c'.pt))
        s)
      (proj (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2) j) =
    s.proj j
Tactic: refine Fan.IsLimit.mk _ (fun t ↦ ?_) ?_ fun t m hm ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Fan.{u_2, v, u} (C := C) fun (j : ι') ↦ X i j
hc : (i : ι) → IsLimit (c i)
c' : Fan.{u_1, v, u} (C := C) fun (i : ι) ↦ (c i).pt
hc' : IsLimit c'
refine_1 :
  (t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) →
    t.pt ⟶
      Cone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
        (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2)
refine_2 :
  ∀ (s : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) (j : ι × ι'),
    CategoryStruct.comp (Y :=
        Cone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
          (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2))
        ((fun (t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
            (lift hc' fun (i : ι) ↦ lift (hc i) fun (j : ι') ↦ t.proj (i, j) : t.pt ⟶ c'.pt))
          s)
        (proj (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2) j) =
      s.proj j
⊢ IsLimit (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
    (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2)
have refine_3 : ∀ (t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2)
  (m :
    t.pt ⟶
      Cone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
        (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2))
  (hm : ∀ (j : ι × ι'), m ≫ proj (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2) j = t.proj j),
  m =
    (fun (t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
        (lift hc' fun (i : ι) ↦ lift (hc i) fun (j : ι') ↦ t.proj (i, j) : t.pt ⟶ c'.pt))
      t
Tactic: refine Fan.IsLimit.mk _ (fun t ↦ ?_) ?_ fun t m hm ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Fan.{u_2, v, u} (C := C) fun (j : ι') ↦ X i j
hc : (i : ι) → IsLimit (c i)
c' : Fan.{u_1, v, u} (C := C) fun (i : ι) ↦ (c i).pt
hc' : IsLimit c'
t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2
m :
  t.pt ⟶
    Cone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
      (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2)
hm : ∀ (j : ι × ι'), m ≫ proj (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2) j = t.proj j
⊢ m =
    (fun (t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
        (lift hc' fun (i : ι) ↦ lift (hc i) fun (j : ι') ↦ t.proj (i, j) : t.pt ⟶ c'.pt))
      t
have refine_3 : ∀ (i : ι),
  m ≫ c'.proj i =
    (fun (t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
          (lift hc' fun (i : ι) ↦ lift (hc i) fun (j : ι') ↦ t.proj (i, j) : t.pt ⟶ c'.pt))
        t ≫
      c'.proj i
Tactic: refine Fan.IsLimit.hom_ext hc' _ _ fun i ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Cofan.{u_2, v, u} (C := C) fun (j : ι') ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan.{u_1, v, u} (C := C) fun (i : ι) ↦ (c i).pt
hc' : IsColimit c'
⊢ IsColimit (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
    (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1)
have refine_1 : (t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) →
  Cocone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
      (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1) ⟶
    t.pt
Tactic: refine Cofan.IsColimit.mk _ (fun t ↦ ?_) ?_ fun t m hm ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Cofan.{u_2, v, u} (C := C) fun (j : ι') ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan.{u_1, v, u} (C := C) fun (i : ι) ↦ (c i).pt
hc' : IsColimit c'
refine_1 :
  (t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) →
    Cocone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
        (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1) ⟶
      t.pt
⊢ IsColimit (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
    (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1)
have refine_2 : ∀ (t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) (j : ι × ι'),
  CategoryStruct.comp (Y :=
      Cocone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
        (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1))
      (inj (f := fun (p : ι × ι') ↦ X p.1 p.2) (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1) j)
      ((fun (t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
          (desc hc' fun (i : ι) ↦ desc (hc i) fun (j : ι') ↦ t.inj (i, j) : c'.pt ⟶ t.pt))
        t) =
    t.inj j
Tactic: refine Cofan.IsColimit.mk _ (fun t ↦ ?_) ?_ fun t m hm ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Cofan.{u_2, v, u} (C := C) fun (j : ι') ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan.{u_1, v, u} (C := C) fun (i : ι) ↦ (c i).pt
hc' : IsColimit c'
refine_1 :
  (t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) →
    Cocone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
        (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1) ⟶
      t.pt
refine_2 :
  ∀ (t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) (j : ι × ι'),
    CategoryStruct.comp (Y :=
        Cocone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
          (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1))
        (inj (f := fun (p : ι × ι') ↦ X p.1 p.2) (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1) j)
        ((fun (t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
            (desc hc' fun (i : ι) ↦ desc (hc i) fun (j : ι') ↦ t.inj (i, j) : c'.pt ⟶ t.pt))
          t) =
      t.inj j
⊢ IsColimit (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
    (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1)
have refine_3 : ∀ (t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2)
  (m :
    Cocone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
        (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1) ⟶
      t.pt)
  (hm :
    ∀ (j : ι × ι'),
      inj (f := fun (p : ι × ι') ↦ X p.1 p.2) (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1) j ≫ m =
        t.inj j),
  m =
    (fun (t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
        (desc hc' fun (i : ι) ↦ desc (hc i) fun (j : ι') ↦ t.inj (i, j) : c'.pt ⟶ t.pt))
      t
Tactic: refine Cofan.IsColimit.mk _ (fun t ↦ ?_) ?_ fun t m hm ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Cofan.{u_2, v, u} (C := C) fun (j : ι') ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan.{u_1, v, u} (C := C) fun (i : ι) ↦ (c i).pt
hc' : IsColimit c'
t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2
m :
  Cocone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
      (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1) ⟶
    t.pt
hm :
  ∀ (j : ι × ι'),
    inj (f := fun (p : ι × ι') ↦ X p.1 p.2) (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1) j ≫ m =
      t.inj j
⊢ m =
    (fun (t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
        (desc hc' fun (i : ι) ↦ desc (hc i) fun (j : ι') ↦ t.inj (i, j) : c'.pt ⟶ t.pt))
      t
have refine_3 : ∀ (i : ι),
  c'.inj i ≫ m =
    c'.inj i ≫
      (fun (t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
          (desc hc' fun (i : ι) ↦ desc (hc i) fun (j : ι') ↦ t.inj (i, j) : c'.pt ⟶ t.pt))
        t
Tactic: refine Cofan.IsColimit.hom_ext hc' _ _ fun i ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
⊢ IsLimit (F := cospan (X := Z₁) (Y := Z₂) (pullback.snd f₁ f₂) (pullback.fst f₃ f₄))
    (PullbackCone.mk («W» := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄)
      (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄)
      (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)
      ⋯)
have apply : IsLimit (F := cospan (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄)
  ((PullbackCone.mk («W» := Z₂) (pullback.fst f₃ f₄) (pullback.snd f₃ f₄) sorry).pasteHoriz (i₂ :=
    (PullbackCone.mk («W» := Z₂) (pullback.fst f₃ f₄) (pullback.snd f₃ f₄) sorry).fst)
    (PullbackCone.mk («W» := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄)
      (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄)
      (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) sorry)
      sorry)
    sorry)
Tactic: apply leftSquareIsPullback _ rfl (pullbackIsPullback f₃ f₄)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
⊢ Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ Y₁)
    ((pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂) ≫ f₁)
    (CategoryStruct.comp (Y := Z₂)
      (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)
      (pullback.fst f₃ f₄ ≫ f₂))
have rw : Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ Y₁)
  ((pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂) ≫ f₁)
  ((pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂) ≫ f₂)
Tactic: rw [pullback.lift_fst_assoc, Category.assoc, Category.assoc, pullback.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
rw :
  Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ Y₁)
    ((pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂) ≫ f₁)
    ((pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂) ≫ f₂)
⊢ Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ Y₁)
    ((pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂) ≫ f₁)
    (CategoryStruct.comp (Y := Z₂)
      (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)
      (pullback.fst f₃ f₄ ≫ f₂))
have rw₁ : Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ Y₁)
  (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂ ≫ f₁)
  ((pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂) ≫ f₂)
Tactic: rw [pullback.lift_fst_assoc, Category.assoc, Category.assoc, pullback.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
rw :
  Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ Y₁)
    ((pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂) ≫ f₁)
    ((pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂) ≫ f₂)
rw₁ :
  Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ Y₁)
    (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂ ≫ f₁)
    ((pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂) ≫ f₂)
⊢ Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ Y₁)
    ((pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂) ≫ f₁)
    (CategoryStruct.comp (Y := Z₂)
      (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)
      (pullback.fst f₃ f₄ ≫ f₂))
have rw₂ : Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ Y₁)
  (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂ ≫ f₁)
  (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂ ≫ f₂)
Tactic: rw [pullback.lift_fst_assoc, Category.assoc, Category.assoc, pullback.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
rw :
  Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ Y₁)
    ((pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂) ≫ f₁)
    ((pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂) ≫ f₂)
rw₁ :
  Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ Y₁)
    (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂ ≫ f₁)
    ((pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂) ≫ f₂)
rw₂ :
  Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ Y₁)
    (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂ ≫ f₁)
    (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂ ≫ f₂)
⊢ Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ Y₁)
    ((pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂) ≫ f₁)
    (CategoryStruct.comp (Y := Z₂)
      (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)
      (pullback.fst f₃ f₄ ≫ f₂))
have rw₃ : Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ Y₁)
  (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂ ≫ f₂)
  (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂ ≫ f₂)
Tactic: rw [pullback.lift_fst_assoc, Category.assoc, Category.assoc, pullback.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ IsLimit (F := cospan (X := Z₁) (Y := Z₂) (pullback.snd f₁ f₂) (pullback.fst f₃ f₄))
    (PullbackCone.mk («W» := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂))
      (pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯)
      (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂)) ⋯)
have apply : IsLimit (F := cospan (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂))
  ((PullbackCone.mk («W» := Z₁) (pullback.fst f₁ f₂) (pullback.snd f₁ f₂) sorry).pasteVert (i₂ :=
    (PullbackCone.mk («W» := Z₁) (pullback.fst f₁ f₂) (pullback.snd f₁ f₂) sorry).snd)
    (PullbackCone.mk («W» := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂))
      (pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) sorry)
      (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂)) sorry)
    sorry)
Tactic: apply topSquareIsPullback _ rfl (pullbackIsPullback f₁ f₂)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ Y₂)
    (CategoryStruct.comp (Y := Z₁)
      (pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯)
      (pullback.snd f₁ f₂ ≫ f₃))
    ((pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄) ≫ f₄)
have rw : Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ Y₂)
  ((pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ≫ f₃)
  ((pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄) ≫ f₄)
Tactic: rw [pullback.lift_snd_assoc, Category.assoc, Category.assoc, pullback.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
rw :
  Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ Y₂)
    ((pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ≫ f₃)
    ((pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄) ≫ f₄)
⊢ Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ Y₂)
    (CategoryStruct.comp (Y := Z₁)
      (pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯)
      (pullback.snd f₁ f₂ ≫ f₃))
    ((pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄) ≫ f₄)
have rw₁ : Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ Y₂)
  (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄ ≫ f₃)
  ((pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄) ≫ f₄)
Tactic: rw [pullback.lift_snd_assoc, Category.assoc, Category.assoc, pullback.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
rw :
  Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ Y₂)
    ((pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ≫ f₃)
    ((pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄) ≫ f₄)
rw₁ :
  Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ Y₂)
    (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄ ≫ f₃)
    ((pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄) ≫ f₄)
⊢ Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ Y₂)
    (CategoryStruct.comp (Y := Z₁)
      (pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯)
      (pullback.snd f₁ f₂ ≫ f₃))
    ((pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄) ≫ f₄)
have rw₂ : Eq (α := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂) ⟶ Y₂)
  (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄ ≫ f₃)
  (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄ ≫ f₄)
Tactic: rw [pullback.lift_snd_assoc, Category.assoc, Category.assoc, pullback.condition]