awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (toSubtype f p) =
    𝟙 (biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
have refine : ∀ (j : Subtype p),
  CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (toSubtype f p))
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j) =
    𝟙 (biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) ≫
      π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j
Tactic: refine biproduct.hom_ext _ _ fun j => ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
j : Subtype p
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (toSubtype f p))
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j) =
    𝟙 (biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) ≫
      π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j
have rw : CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) (toSubtype f p)
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j)) =
  𝟙 (biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) ≫
    π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j
Tactic: rw [Category.assoc, biproduct.toSubtype_π, biproduct.fromSubtype_π_subtype, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
j : Subtype p
rw :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) (toSubtype f p)
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j)) =
    𝟙 (biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) ≫
      π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (toSubtype f p))
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j) =
    𝟙 (biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) ≫
      π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j
have rw₁ : CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (π f (↑j : J)) =
  𝟙 (biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) ≫
    π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j
Tactic: rw [Category.assoc, biproduct.toSubtype_π, biproduct.fromSubtype_π_subtype, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
j : Subtype p
rw :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) (toSubtype f p)
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j)) =
    𝟙 (biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) ≫
      π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j
rw₁ :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (π f (↑j : J)) =
    𝟙 (biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) ≫
      π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (toSubtype f p))
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j) =
    𝟙 (biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) ≫
      π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j
have rw₂ : π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j =
  𝟙 (biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) ≫
    π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j
Tactic: rw [Category.assoc, biproduct.toSubtype_π, biproduct.fromSubtype_π_subtype, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
j : Subtype p
rw :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) (toSubtype f p)
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j)) =
    𝟙 (biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) ≫
      π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j
rw₁ :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (π f (↑j : J)) =
    𝟙 (biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) ≫
      π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j
rw₂ :
  π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j =
    𝟙 (biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) ≫
      π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (toSubtype f p))
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j) =
    𝟙 (biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) ≫
      π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j
have rw₃ : Eq.{v + 1} (α :=
  biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j)
  (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j) (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j)
Tactic: rw [Category.assoc, biproduct.toSubtype_π, biproduct.fromSubtype_π_subtype, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
inst_4 : DecidablePred p
⊢ Eq.{v + 1} (α := biproduct.{w, v, u} f ⟶ biproduct.{w, v, u} f)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) (toSubtype f p)
      (fromSubtype f p))
    (map fun (j : J) ↦ if p j then 𝟙 (f j) else 0)
have w : ∀ (i : J),
  Eq.{v + 1} (α := biproduct.{w, v, u} f ⟶ f i)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) (toSubtype f p)
        (fromSubtype f p))
      (π f i))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (map fun (j : J) ↦ if p j then 𝟙 (f j) else 0) (π f i))
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
inst_4 : DecidablePred p
i : J
⊢ Eq.{v + 1} (α := biproduct.{w, v, u} f ⟶ f i)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) (toSubtype f p)
        (fromSubtype f p))
      (π f i))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (map fun (j : J) ↦ if p j then 𝟙 (f j) else 0) (π f i))
have pos : ∀ (h : p i),
  Eq.{v + 1} (α := biproduct.{w, v, u} f ⟶ f i)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) (toSubtype f p)
        (fromSubtype f p))
      (π f i))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (map fun (j : J) ↦ if p j then 𝟙 (f j) else 0) (π f i))
Tactic: by_cases h : p i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
inst_2 : HasBiproduct.{w, v, u} f
p : J → Prop
inst_3 : HasBiproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)
inst_4 : DecidablePred p
i : J
pos :
  ∀ (h : p i),
    Eq.{v + 1} (α := biproduct.{w, v, u} f ⟶ f i)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
        (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) (toSubtype f p)
          (fromSubtype f p))
        (π f i))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (map fun (j : J) ↦ if p j then 𝟙 (f j) else 0) (π f i))
⊢ Eq.{v + 1} (α := biproduct.{w, v, u} f ⟶ f i)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) (toSubtype f p)
        (fromSubtype f p))
      (π f i))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (map fun (j : J) ↦ if p j then 𝟙 (f j) else 0) (π f i))
have neg : ∀ (h : ¬p i),
  Eq.{v + 1} (α := biproduct.{w, v, u} f ⟶ f i)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) (toSubtype f p)
        (fromSubtype f p))
      (π f i))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (map fun (j : J) ↦ if p j then 𝟙 (f j) else 0) (π f i))
Tactic: by_cases h : p i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Fork.{v, u} (X := biproduct.{w, v, u} f) (π f i) 0
⊢ CategoryStruct.comp (Y :=
      Cone.pt.{0, v, 0, u} (F := parallelPair (X := biproduct.{w, v, u} f) (π f i) 0)
        (KernelFork.ofι (Z :=
          biproduct.{w, v, u} (J := { j : J // j ≠ i })
            (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
          (fromSubtype f fun (j : J) ↦ j ≠ i) ⋯))
      (s.ι ≫ toSubtype f fun (j : J) ↦ j ≠ i)
      (Fork.ι
        (KernelFork.ofι (Z :=
          biproduct.{w, v, u} (J := { j : J // j ≠ i })
            (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
          (fromSubtype f fun (j : J) ↦ j ≠ i) ⋯)) =
    s.ι
have w : ∀ (j : J),
  CategoryStruct.comp (Y := biproduct.{w, v, u} f)
      (CategoryStruct.comp (Y :=
        Cone.pt.{0, v, 0, u} (F := parallelPair (X := biproduct.{w, v, u} f) (π f i) 0)
          (KernelFork.ofι (Z :=
            biproduct.{w, v, u} (J := { j : J // j ≠ i })
              (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
            (fromSubtype f fun (j : J) ↦ j ≠ i) sorry))
        (s.ι ≫ toSubtype f fun (j : J) ↦ j ≠ i)
        (Fork.ι
          (KernelFork.ofι (Z :=
            biproduct.{w, v, u} (J := { j : J // j ≠ i })
              (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
            (fromSubtype f fun (j : J) ↦ j ≠ i) sorry)))
      (π f j) =
    s.ι ≫ π f j
Tactic: apply biproduct.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Fork.{v, u} (X := biproduct.{w, v, u} f) (π f i) 0
j : J
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f)
      (CategoryStruct.comp (Y :=
        Cone.pt.{0, v, 0, u} (F := parallelPair (X := biproduct.{w, v, u} f) (π f i) 0)
          (KernelFork.ofι (Z :=
            biproduct.{w, v, u} (J := { j : J // j ≠ i })
              (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
            (fromSubtype f fun (j : J) ↦ j ≠ i) ⋯))
        (s.ι ≫ toSubtype f fun (j : J) ↦ j ≠ i)
        (Fork.ι
          (KernelFork.ofι (Z :=
            biproduct.{w, v, u} (J := { j : J // j ≠ i })
              (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
            (fromSubtype f fun (j : J) ↦ j ≠ i) ⋯)))
      (π f j) =
    s.ι ≫ π f j
have w : (s.ι ≫ π f j ≫ if j ≠ i then 𝟙 (f j) else 0) = s.ι ≫ π f j
Tactic: rw [KernelFork.ι_ofι, Category.assoc, Category.assoc,
        biproduct.toSubtype_fromSubtype_assoc, biproduct.map_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Fork.{v, u} (X := biproduct.{w, v, u} f) (π f i) 0
⊢ (s.ι ≫ π f i ≫ if i ≠ i then 𝟙 (f i) else 0) = s.ι ≫ π f i
have w : s.ι ≫ π f i ≫ 0 = s.ι ≫ π f i
Tactic: rw [if_neg (Classical.not_not.2 rfl), comp_zero, comp_zero, KernelFork.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Fork.{v, u} (X := biproduct.{w, v, u} f) (π f i) 0
w : s.ι ≫ π f i ≫ 0 = s.ι ≫ π f i
⊢ (s.ι ≫ π f i ≫ if i ≠ i then 𝟙 (f i) else 0) = s.ι ≫ π f i
have w₁ : s.ι ≫ 0 = s.ι ≫ π f i
Tactic: rw [if_neg (Classical.not_not.2 rfl), comp_zero, comp_zero, KernelFork.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Fork.{v, u} (X := biproduct.{w, v, u} f) (π f i) 0
w : s.ι ≫ π f i ≫ 0 = s.ι ≫ π f i
w₁ : s.ι ≫ 0 = s.ι ≫ π f i
⊢ (s.ι ≫ π f i ≫ if i ≠ i then 𝟙 (f i) else 0) = s.ι ≫ π f i
have w₂ : 0 = s.ι ≫ π f i
Tactic: rw [if_neg (Classical.not_not.2 rfl), comp_zero, comp_zero, KernelFork.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Fork.{v, u} (X := biproduct.{w, v, u} f) (π f i) 0
w : s.ι ≫ π f i ≫ 0 = s.ι ≫ π f i
w₁ : s.ι ≫ 0 = s.ι ≫ π f i
w₂ : 0 = s.ι ≫ π f i
⊢ (s.ι ≫ π f i ≫ if i ≠ i then 𝟙 (f i) else 0) = s.ι ≫ π f i
have w₃ : Eq.{v + 1} (α := s.pt ⟶ f i) 0 0
Tactic: rw [if_neg (Classical.not_not.2 rfl), comp_zero, comp_zero, KernelFork.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Fork.{v, u} (X := biproduct.{w, v, u} f) (π f i) 0
j : J
h : ¬i = j
⊢ (s.ι ≫ π f j ≫ if j ≠ i then 𝟙 (f j) else 0) = s.ι ≫ π f j
have w : s.ι ≫ π f j ≫ 𝟙 (f j) = s.ι ≫ π f j
Tactic: rw [if_pos (Ne.symm h), Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Fork.{v, u} (X := biproduct.{w, v, u} f) (π f i) 0
j : J
h : ¬i = j
w : s.ι ≫ π f j ≫ 𝟙 (f j) = s.ι ≫ π f j
⊢ (s.ι ≫ π f j ≫ if j ≠ i then 𝟙 (f j) else 0) = s.ι ≫ π f j
have w₁ : s.ι ≫ π f j = s.ι ≫ π f j
Tactic: rw [if_pos (Ne.symm h), Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Fork.{v, u} (X := biproduct.{w, v, u} f) (π f i) 0
m :
  s.pt ⟶
    Cone.pt.{0, v, 0, u} (F := parallelPair (X := biproduct.{w, v, u} f) (π f i) 0)
      (KernelFork.ofι (Z :=
        biproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
        (fromSubtype f fun (j : J) ↦ j ≠ i) ⋯)
hm :
  m ≫
      Fork.ι
        (KernelFork.ofι (Z :=
          biproduct.{w, v, u} (J := { j : J // j ≠ i })
            (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
          (fromSubtype f fun (j : J) ↦ j ≠ i) ⋯) =
    s.ι
⊢ m = s.ι ≫ toSubtype f fun (j : J) ↦ j ≠ i
have rw : m =
  m ≫
    𝟙 (biproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
Tactic: rw [← hm, KernelFork.ι_ofι, Category.assoc, biproduct.fromSubtype_toSubtype]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Cofork.{v, u} (Y := biproduct.{w, v, u} f) (ι f i) 0
⊢ CategoryStruct.comp (Y :=
      Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := biproduct.{w, v, u} f) (ι f i) 0)
        (CokernelCofork.ofπ (Z :=
          biproduct.{w, v, u} (J := { j : J // j ≠ i })
            (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
          (toSubtype f fun (j : J) ↦ j ≠ i) ⋯))
      (Cofork.π
        (CokernelCofork.ofπ (Z :=
          biproduct.{w, v, u} (J := { j : J // j ≠ i })
            (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
          (toSubtype f fun (j : J) ↦ j ≠ i) ⋯))
      ((fromSubtype f fun (j : J) ↦ j ≠ i) ≫ s.π) =
    s.π
have w : ∀ (j : J),
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (CategoryStruct.comp (Y :=
        Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := biproduct.{w, v, u} f) (ι f i) 0)
          (CokernelCofork.ofπ (Z :=
            biproduct.{w, v, u} (J := { j : J // j ≠ i })
              (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
            (toSubtype f fun (j : J) ↦ j ≠ i) sorry))
        (Cofork.π
          (CokernelCofork.ofπ (Z :=
            biproduct.{w, v, u} (J := { j : J // j ≠ i })
              (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
            (toSubtype f fun (j : J) ↦ j ≠ i) sorry))
        ((fromSubtype f fun (j : J) ↦ j ≠ i) ≫ s.π)) =
    ι f j ≫ s.π
Tactic: apply biproduct.hom_ext'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f : J → C
i : J
inst_6 : HasBiproduct.{w, v, u} f
inst_7 :
  HasBiproduct.{w, v, u} (J := { j : J // j ≠ i }) (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f)
s : Cofork.{v, u} (Y := biproduct.{w, v, u} f) (ι f i) 0
j : J
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (CategoryStruct.comp (Y :=
        Cocone.pt.{0, v, 0, u} (F := parallelPair (Y := biproduct.{w, v, u} f) (ι f i) 0)
          (CokernelCofork.ofπ (Z :=
            biproduct.{w, v, u} (J := { j : J // j ≠ i })
              (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
            (toSubtype f fun (j : J) ↦ j ≠ i) ⋯))
        (Cofork.π
          (CokernelCofork.ofπ (Z :=
            biproduct.{w, v, u} (J := { j : J // j ≠ i })
              (Subtype.restrict (β := fun (x : J) ↦ C) (fun (j : J) ↦ j ≠ i) f))
            (toSubtype f fun (j : J) ↦ j ≠ i) ⋯))
        ((fromSubtype f fun (j : J) ↦ j ≠ i) ≫ s.π)) =
    ι f j ≫ s.π
have w : (if j ≠ i then 𝟙 (f j) else 0) ≫ ι f j ≫ s.π = ι f j ≫ s.π
Tactic: rw [CokernelCofork.π_ofπ, biproduct.toSubtype_fromSubtype_assoc, biproduct.ι_map_assoc]