awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{w, v, w, u} J C
c₁ : Cofan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
c₂ : Cofan.{w, v, u} F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    c₁.ι.app { as := f } ≫ s =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 : Discrete J }
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
        c₂.pt)
      (c₁.ι.app { as := f } ≫ t) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 })
i : Cofork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
reassoced :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)) {W : C} {h : c₂.pt ⟶ W},
    c₁.ι.app { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ s ≫ h =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 } ≫ h
rw : F.map f ≫ c₂.ι.app { as := j₂ : Discrete J } ≫ i.π = c₂.ι.app { as := j₁ } ≫ i.π
rw₁ :
  c₁.ι.app { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫
      s ≫ i.π =
    c₂.ι.app { as := j₁ } ≫ i.π
⊢ F.map f ≫ c₂.ι.app { as := j₂ : Discrete J } ≫ i.π = (c₂.ι.app { as := j₁ : Discrete J } ≫ i.π) ≫ 𝟙 i.pt
have rw₂ : Eq (α := F.obj j₁ ⟶ i.pt)
  (c₁.ι.app { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f } ≫ t ≫ i.π :
    Functor.obj.{w, v, w, u} (C := Discrete ((p : J × J) × (p.1 ⟶ p.2)))
        (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
        { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f } ⟶
      i.pt)
  (c₂.ι.app { as := j₁ } ≫ i.π)
Tactic: rw [Category.comp_id, ← reassoced ⟨⟨_, _⟩, f⟩, i.condition, ← Category.assoc, ht]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{w, v, w, u} J C
c₁ : Cofan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
c₂ : Cofan.{w, v, u} F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    c₁.ι.app { as := f } ≫ s =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 : Discrete J }
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
        c₂.pt)
      (c₁.ι.app { as := f } ≫ t) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 })
i : Cofork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
reassoced :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)) {W : C} {h : c₂.pt ⟶ W},
    c₁.ι.app { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ s ≫ h =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 } ≫ h
rw : F.map f ≫ c₂.ι.app { as := j₂ : Discrete J } ≫ i.π = c₂.ι.app { as := j₁ } ≫ i.π
rw₁ :
  c₁.ι.app { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫
      s ≫ i.π =
    c₂.ι.app { as := j₁ } ≫ i.π
rw₂ :
  Eq (α := F.obj j₁ ⟶ i.pt)
    (c₁.ι.app { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f } ≫ t ≫ i.π :
      Functor.obj.{w, v, w, u} (C := Discrete ((p : J × J) × (p.1 ⟶ p.2)))
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
          { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f } ⟶
        i.pt)
    (c₂.ι.app { as := j₁ } ≫ i.π)
⊢ F.map f ≫ c₂.ι.app { as := j₂ : Discrete J } ≫ i.π = (c₂.ι.app { as := j₁ : Discrete J } ≫ i.π) ≫ 𝟙 i.pt
have rw₃ : Eq (α := F.obj j₁ ⟶ i.pt)
  ((c₁.ι.app { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f } ≫ t) ≫ i.π :
    Functor.obj.{w, v, w, u} (C := Discrete ((p : J × J) × (p.1 ⟶ p.2)))
        (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
        { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f } ⟶
      i.pt)
  (c₂.ι.app { as := j₁ } ≫ i.π)
Tactic: rw [Category.comp_id, ← reassoced ⟨⟨_, _⟩, f⟩, i.condition, ← Category.assoc, ht]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{w, v, w, u} J C
c₁ : Cofan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
c₂ : Cofan.{w, v, u} F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    c₁.ι.app { as := f } ≫ s =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 : Discrete J }
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
        c₂.pt)
      (c₁.ι.app { as := f } ≫ t) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 })
i : Cofork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
reassoced :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)) {W : C} {h : c₂.pt ⟶ W},
    c₁.ι.app { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ s ≫ h =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 } ≫ h
rw : F.map f ≫ c₂.ι.app { as := j₂ : Discrete J } ≫ i.π = c₂.ι.app { as := j₁ } ≫ i.π
rw₁ :
  c₁.ι.app { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫
      s ≫ i.π =
    c₂.ι.app { as := j₁ } ≫ i.π
rw₂ :
  Eq (α := F.obj j₁ ⟶ i.pt)
    (c₁.ι.app { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f } ≫ t ≫ i.π :
      Functor.obj.{w, v, w, u} (C := Discrete ((p : J × J) × (p.1 ⟶ p.2)))
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
          { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f } ⟶
        i.pt)
    (c₂.ι.app { as := j₁ } ≫ i.π)
rw₃ :
  Eq (α := F.obj j₁ ⟶ i.pt)
    ((c₁.ι.app { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f } ≫ t) ≫ i.π :
      Functor.obj.{w, v, w, u} (C := Discrete ((p : J × J) × (p.1 ⟶ p.2)))
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
          { as := Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f } ⟶
        i.pt)
    (c₂.ι.app { as := j₁ } ≫ i.π)
⊢ F.map f ≫ c₂.ι.app { as := j₂ : Discrete J } ≫ i.π = (c₂.ι.app { as := j₁ : Discrete J } ≫ i.π) ≫ 𝟙 i.pt
have rw₄ : Eq (α := F.obj j₁ ⟶ i.pt)
  (c₂.ι.app
      {
        as :=
          (Sigma.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (Sigma.mk (β := fun (p : J × J) ↦ p.1 ⟶ p.2) (j₁, j₂) f)).1 } ≫
    i.π)
  (c₂.ι.app { as := j₁ } ≫ i.π)
Tactic: rw [Category.comp_id, ← reassoced ⟨⟨_, _⟩, f⟩, i.condition, ← Category.assoc, ht]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{w, v, w, u} J C
c₁ : Cofan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
c₂ : Cofan.{w, v, u} F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    c₁.ι.app { as := f } ≫ s =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 : Discrete J }
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
        c₂.pt)
      (c₁.ι.app { as := f } ≫ t) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 })
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
⊢ (buildColimit s t hs ht i).pt ⟶ q.pt
have refine_1 : c₂.pt ⟶ q.1
Tactic: refine hi.desc (Cofork.ofπ ?_ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{w, v, w, u} J C
c₁ : Cofan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
c₂ : Cofan.{w, v, u} F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    c₁.ι.app { as := f } ≫ s =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 : Discrete J }
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
        c₂.pt)
      (c₁.ι.app { as := f } ≫ t) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 })
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
refine_1 : c₂.pt ⟶ q.1
⊢ (buildColimit s t hs ht i).pt ⟶ q.pt
have refine_2 : Eq (α := c₁.pt ⟶ q.1) (s ≫ t₂.desc (Cofan.mk q.1 fun (j : J) ↦ q.ι.app j) : c₁.pt ⟶ q.1)
  (t ≫ t₂.desc (Cofan.mk q.1 fun (j : J) ↦ q.ι.app j) : c₁.pt ⟶ q.1)
Tactic: refine hi.desc (Cofork.ofπ ?_ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{w, v, w, u} J C
c₁ : Cofan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
c₂ : Cofan.{w, v, u} F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    c₁.ι.app { as := f } ≫ s =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 : Discrete J }
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
        c₂.pt)
      (c₁.ι.app { as := f } ≫ t) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 })
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
⊢ c₂.pt ⟶ q.1
have refine_1 : (j : J) → F.obj j ⟶ q.1
Tactic: refine t₂.desc (Cofan.mk _ fun j => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{w, v, w, u} J C
c₁ : Cofan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
c₂ : Cofan.{w, v, u} F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    c₁.ι.app { as := f } ≫ s =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 : Discrete J }
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
        c₂.pt)
      (c₁.ι.app { as := f } ≫ t) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 })
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
⊢ Eq (α := c₁.pt ⟶ q.1) (s ≫ t₂.desc (Cofan.mk q.1 fun (j : J) ↦ q.ι.app j) : c₁.pt ⟶ q.1)
    (t ≫ t₂.desc (Cofan.mk q.1 fun (j : J) ↦ q.ι.app j) : c₁.pt ⟶ q.1)
have refine_2 : ∀ (j : Discrete ((p : J × J) × (p.1 ⟶ p.2))),
  Eq (α :=
    Quiver.Hom.{v, u} (V := C)
      (Functor.obj.{w, v, w, u}
        (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) j)
      q.1)
    (c₁.ι.app j ≫ s ≫ t₂.desc (Cofan.mk q.1 fun (j : J) ↦ q.ι.app j) :
      Quiver.Hom.{v, u} (V := C)
        (Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) j)
        q.1)
    (c₁.ι.app j ≫ t ≫ t₂.desc (Cofan.mk q.1 fun (j : J) ↦ q.ι.app j) :
      Quiver.Hom.{v, u} (V := C)
        (Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1) j)
        q.1)
Tactic: apply t₁.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{w, v, w, u} J C
c₁ : Cofan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
c₂ : Cofan.{w, v, u} F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    c₁.ι.app { as := f } ≫ s =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 : Discrete J }
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
        c₂.pt)
      (c₁.ι.app { as := f } ≫ t) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 })
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
j f : (p : J × J) × (p.1 ⟶ p.2)
W : C
h : c₂.pt ⟶ W
⊢ c₁.ι.app { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ s ≫ h =
    F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫ c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 } ≫ h
have simp : (c₁.ι.app { as := f } ≫ s) ≫ h =
  (F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
      c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 : Discrete J }) ≫
    h
Tactic: simp only [← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{w, v, w, u} J C
c₁ : Cofan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
c₂ : Cofan.{w, v, u} F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    c₁.ι.app { as := f } ≫ s =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 : Discrete J }
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
        c₂.pt)
      (c₁.ι.app { as := f } ≫ t) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 })
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
j : (p : J × J) × (p.1 ⟶ p.2)
⊢ Eq (α :=
    Quiver.Hom.{v, u} (V := C)
      (Functor.obj.{w, v, w, u}
        (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
        { as := j : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      q.1)
    (c₁.ι.app { as := j : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ s ≫ t₂.desc (Cofan.mk q.1 fun (j : J) ↦ q.ι.app j) :
      Quiver.Hom.{v, u} (V := C)
        (Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
          { as := j : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
        q.1)
    (c₁.ι.app { as := j : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ t ≫ t₂.desc (Cofan.mk q.1 fun (j : J) ↦ q.ι.app j) :
      Quiver.Hom.{v, u} (V := C)
        (Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
          { as := j : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
        q.1)
have reassoced_s : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)) {W : C} (h : c₂.pt ⟶ W),
  c₁.ι.app { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ s ≫ h =
    F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫ c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 } ≫ h
Tactic: have reassoced_s (f : (p : J × J) × (p.fst ⟶ p.snd)) {W : C} (h : _ ⟶ W) :
        c₁.ι.app ⟨f⟩ ≫ s ≫ h = F.map f.snd ≫ c₂.ι.app ⟨f.fst.snd⟩ ≫ h := by
          simp only [← Category.assoc]
          apply eq_whisker (hs f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{w, v, w, u} J C
c₁ : Cofan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
c₂ : Cofan.{w, v, u} F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    c₁.ι.app { as := f } ≫ s =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 : Discrete J }
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
        c₂.pt)
      (c₁.ι.app { as := f } ≫ t) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 })
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
j : (p : J × J) × (p.1 ⟶ p.2)
reassoced_s :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)) {W : C} (h : c₂.pt ⟶ W),
    c₁.ι.app { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ s ≫ h =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 } ≫ h
f : (p : J × J) × (p.1 ⟶ p.2)
W : C
h : c₂.pt ⟶ W
⊢ c₁.ι.app { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ t ≫ h =
    c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫ h
have simp : Eq (α :=
  Functor.obj.{w, v, w, u}
      (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
      { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
    W)
  ((c₁.ι.app { as := f } ≫ t) ≫ h) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫ h)
Tactic: simp only [← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{w, v, w, u} J C
c₁ : Cofan.{w, v, u} (C := C) fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
c₂ : Cofan.{w, v, u} F.obj
s t : c₁.pt ⟶ c₂.pt
hs :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    c₁.ι.app { as := f } ≫ s =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 : Discrete J }
ht :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)),
    Eq (α :=
      Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
          { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ⟶
        c₂.pt)
      (c₁.ι.app { as := f } ≫ t) (c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 })
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
j : (p : J × J) × (p.1 ⟶ p.2)
reassoced_s :
  ∀ (f : (p : J × J) × (p.1 ⟶ p.2)) {W : C} (h : c₂.pt ⟶ W),
    c₁.ι.app { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ s ≫ h =
      F.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
        c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 } ≫ h
⊢ Eq (α :=
    Quiver.Hom.{v, u} (V := C)
      (Functor.obj.{w, v, w, u}
        (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
        { as := j : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
      q.1)
    (c₁.ι.app { as := j : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ s ≫ t₂.desc (Cofan.mk q.1 fun (j : J) ↦ q.ι.app j) :
      Quiver.Hom.{v, u} (V := C)
        (Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
          { as := j : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
        q.1)
    (c₁.ι.app { as := j : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ t ≫ t₂.desc (Cofan.mk q.1 fun (j : J) ↦ q.ι.app j) :
      Quiver.Hom.{v, u} (V := C)
        (Functor.obj.{w, v, w, u}
          (Discrete.functor fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ F.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1)
          { as := j : Discrete ((p : J × J) × (p.1 ⟶ p.2)) })
        q.1)
have reassoced_t : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)) {W : C} (h : c₂.pt ⟶ W),
  c₁.ι.app { as := f : Discrete ((p : J × J) × (p.1 ⟶ p.2)) } ≫ t ≫ h =
    c₂.ι.app { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 } ≫ h
Tactic: have reassoced_t (f : (p : J × J) × (p.fst ⟶ p.snd)) {W : C} (h : _ ⟶ W) :
        c₁.ι.app ⟨f⟩ ≫ t ≫ h = c₂.ι.app ⟨f.fst.fst⟩ ≫ h := by
          simp only [← Category.assoc]
          apply eq_whisker (ht f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasColimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasColimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasCoequalizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesColimitsOfShape WalkingParallelPair G
inst_7 : PreservesColimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesColimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := sigmaObj.{w, v, u} K.obj
Q : C := sigmaObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
s : Q ⟶ P :=
  Sigma.desc fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
      colimit.ι (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
t : Q ⟶ P :=
  Sigma.desc fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    colimit.ι (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ PreservesColimit K G
have apply : IsColimit (G.mapCocone (buildColimit s t sorry sorry (colimit.cocone (parallelPair s t))))
Tactic: apply preservesColimit_of_preserves_colimit_cocone
        (buildIsColimit s t (by simp [P, s]) (by simp [P, t]) (colimit.isColimit _)
          (colimit.isColimit _) (colimit.isColimit _))