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)
inst_4 : DecidablePred p
j : J
w :
  ∀ (i : Subtype p),
    Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (toSubtype f p))
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
⊢ Eq.{v + 1} (α := f j ⟶ biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (toSubtype f p))
    (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
have w₁ : ∀ (i : Subtype p),
  Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (if h : j = (↑i : J) then eqToHom sorry else 0)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
Tactic: classical
  ext i
  rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π]
  by_cases h : p j
  · rw [dif_pos h, biproduct.ι_π]
    split_ifs with h₁ h₂ h₂
    exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]
  · rw [dif_neg h, dif_neg (show j ≠ i from fun h₂ => h (h₂.symm ▸ i.2)), zero_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
j : J
w :
  ∀ (i : Subtype p),
    Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (toSubtype f p))
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
w₁ :
  ∀ (i : Subtype p),
    Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (if h : j = (↑i : J) then eqToHom ⋯ else 0)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
⊢ Eq.{v + 1} (α := f j ⟶ biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (toSubtype f p))
    (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
have pos : ∀ (i : Subtype p) (h : p j),
  Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (if h : j = (↑i : J) then eqToHom sorry else 0)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
Tactic: classical
  ext i
  rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π]
  by_cases h : p j
  · rw [dif_pos h, biproduct.ι_π]
    split_ifs with h₁ h₂ h₂
    exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]
  · rw [dif_neg h, dif_neg (show j ≠ i from fun h₂ => h (h₂.symm ▸ i.2)), zero_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
j : J
w :
  ∀ (i : Subtype p),
    Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (toSubtype f p))
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
w₁ :
  ∀ (i : Subtype p),
    Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (if h : j = (↑i : J) then eqToHom ⋯ else 0)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
pos :
  ∀ (i : Subtype p) (h : p j),
    Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (if h : j = (↑i : J) then eqToHom ⋯ else 0)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
⊢ Eq.{v + 1} (α := f j ⟶ biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (toSubtype f p))
    (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
have neg : ∀ (i : Subtype p) (h : ¬p j),
  Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (if h : j = (↑i : J) then eqToHom sorry else 0)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (if h : p j then ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) (Subtype.mk (p := p) j h) else 0)
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
Tactic: classical
  ext i
  rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π]
  by_cases h : p j
  · rw [dif_pos h, biproduct.ι_π]
    split_ifs with h₁ h₂ h₂
    exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]
  · rw [dif_neg h, dif_neg (show j ≠ i from fun h₂ => h (h₂.symm ▸ i.2)), zero_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
⊢ Eq.{v + 1} (α := f (↑j : J) ⟶ biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f (↑j : J)) (toSubtype f p))
    (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) j)
have w : ∀ (j_1 : Subtype p),
  Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f (↑j : J)) (toSubtype f p))
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j_1))
    (CategoryStruct.comp (Y := 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_1))
Tactic: ext
-- 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 j_1 : Subtype p
⊢ Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f (↑j : J)) (toSubtype f p))
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j_1))
    (CategoryStruct.comp (Y := 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_1))
have w : Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1)
  (if h : (↑j : J) = (↑j_1 : J) then eqToHom sorry else 0) (if h : j = j_1 then eqToHom sorry else 0)
Tactic: rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π, biproduct.ι_π]
-- 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 j_1 : Subtype p
⊢ Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1)
    (if h : (↑j : J) = (↑j_1 : J) then eqToHom ⋯ else 0) (if h : j = j_1 then eqToHom ⋯ else 0)
have pos : ∀ (h₁ : (↑j : J) = (↑j_1 : J)) (h₂ : j = j_1),
  Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) (eqToHom sorry) (eqToHom sorry)
Tactic: split_ifs with h₁ h₂ h₂
-- 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 j_1 : Subtype p
pos :
  ∀ (h₁ : (↑j : J) = (↑j_1 : J)) (h₂ : j = j_1),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) (eqToHom ⋯) (eqToHom ⋯)
⊢ Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1)
    (if h : (↑j : J) = (↑j_1 : J) then eqToHom ⋯ else 0) (if h : j = j_1 then eqToHom ⋯ else 0)
have neg : ∀ (h₁ : (↑j : J) = (↑j_1 : J)) (h₂ : ¬j = j_1),
  Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) (eqToHom sorry) 0
Tactic: split_ifs with h₁ h₂ h₂
-- 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 j_1 : Subtype p
pos :
  ∀ (h₁ : (↑j : J) = (↑j_1 : J)) (h₂ : j = j_1),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) (eqToHom ⋯) (eqToHom ⋯)
neg :
  ∀ (h₁ : (↑j : J) = (↑j_1 : J)) (h₂ : ¬j = j_1),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) (eqToHom ⋯) 0
⊢ Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1)
    (if h : (↑j : J) = (↑j_1 : J) then eqToHom ⋯ else 0) (if h : j = j_1 then eqToHom ⋯ else 0)
have pos₁ : ∀ (h₁ : ¬(↑j : J) = (↑j_1 : J)) (h₂ : j = j_1),
  Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) 0 (eqToHom sorry)
Tactic: split_ifs with h₁ h₂ h₂
-- 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 j_1 : Subtype p
pos :
  ∀ (h₁ : (↑j : J) = (↑j_1 : J)) (h₂ : j = j_1),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) (eqToHom ⋯) (eqToHom ⋯)
neg :
  ∀ (h₁ : (↑j : J) = (↑j_1 : J)) (h₂ : ¬j = j_1),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) (eqToHom ⋯) 0
pos₁ :
  ∀ (h₁ : ¬(↑j : J) = (↑j_1 : J)) (h₂ : j = j_1),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) 0 (eqToHom ⋯)
⊢ Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1)
    (if h : (↑j : J) = (↑j_1 : J) then eqToHom ⋯ else 0) (if h : j = j_1 then eqToHom ⋯ else 0)
have neg₁ : ∀ (h₁ : ¬(↑j : J) = (↑j_1 : J)) (h₂ : ¬j = j_1),
  Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) 0 0
Tactic: split_ifs with h₁ h₂ h₂
-- 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
⊢ Eq.{v + 1} (α := f (↑j : J) ⟶ biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f (↑j : J)) (toSubtype f p))
    (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) j)
have w : ∀ (j_1 : Subtype p),
  Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f (↑j : J)) (toSubtype f p))
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j_1))
    (CategoryStruct.comp (Y := 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_1))
Tactic: classical
  ext
  rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π, biproduct.ι_π]
  split_ifs with h₁ h₂ h₂
  exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]
-- 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
w :
  ∀ (j_1 : Subtype p),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f (↑j : J)) (toSubtype f p))
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j_1))
      (CategoryStruct.comp (Y := 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_1))
⊢ Eq.{v + 1} (α := f (↑j : J) ⟶ biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f (↑j : J)) (toSubtype f p))
    (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) j)
have w₁ : ∀ (j_1 : Subtype p),
  Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1)
    (if h : (↑j : J) = (↑j_1 : J) then eqToHom sorry else 0) (if h : j = j_1 then eqToHom sorry else 0)
Tactic: classical
  ext
  rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π, biproduct.ι_π]
  split_ifs with h₁ h₂ h₂
  exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]
-- 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
w :
  ∀ (j_1 : Subtype p),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f (↑j : J)) (toSubtype f p))
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j_1))
      (CategoryStruct.comp (Y := 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_1))
w₁ :
  ∀ (j_1 : Subtype p),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1)
      (if h : (↑j : J) = (↑j_1 : J) then eqToHom ⋯ else 0) (if h : j = j_1 then eqToHom ⋯ else 0)
⊢ Eq.{v + 1} (α := f (↑j : J) ⟶ biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f (↑j : J)) (toSubtype f p))
    (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) j)
have pos : ∀ (j_1 : Subtype p) (h₁ : (↑j : J) = (↑j_1 : J)) (h₂ : j = j_1),
  Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) (eqToHom sorry) (eqToHom sorry)
Tactic: classical
  ext
  rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π, biproduct.ι_π]
  split_ifs with h₁ h₂ h₂
  exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]
-- 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
w :
  ∀ (j_1 : Subtype p),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f (↑j : J)) (toSubtype f p))
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j_1))
      (CategoryStruct.comp (Y := 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_1))
w₁ :
  ∀ (j_1 : Subtype p),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1)
      (if h : (↑j : J) = (↑j_1 : J) then eqToHom ⋯ else 0) (if h : j = j_1 then eqToHom ⋯ else 0)
pos :
  ∀ (j_1 : Subtype p) (h₁ : (↑j : J) = (↑j_1 : J)) (h₂ : j = j_1),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) (eqToHom ⋯) (eqToHom ⋯)
⊢ Eq.{v + 1} (α := f (↑j : J) ⟶ biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f (↑j : J)) (toSubtype f p))
    (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) j)
have neg : ∀ (j_1 : Subtype p) (h₁ : (↑j : J) = (↑j_1 : J)) (h₂ : ¬j = j_1),
  Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) (eqToHom sorry) 0
Tactic: classical
  ext
  rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π, biproduct.ι_π]
  split_ifs with h₁ h₂ h₂
  exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]
-- 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
w :
  ∀ (j_1 : Subtype p),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f (↑j : J)) (toSubtype f p))
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j_1))
      (CategoryStruct.comp (Y := 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_1))
w₁ :
  ∀ (j_1 : Subtype p),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1)
      (if h : (↑j : J) = (↑j_1 : J) then eqToHom ⋯ else 0) (if h : j = j_1 then eqToHom ⋯ else 0)
pos :
  ∀ (j_1 : Subtype p) (h₁ : (↑j : J) = (↑j_1 : J)) (h₂ : j = j_1),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) (eqToHom ⋯) (eqToHom ⋯)
neg :
  ∀ (j_1 : Subtype p) (h₁ : (↑j : J) = (↑j_1 : J)) (h₂ : ¬j = j_1),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) (eqToHom ⋯) 0
⊢ Eq.{v + 1} (α := f (↑j : J) ⟶ biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f (↑j : J)) (toSubtype f p))
    (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) j)
have pos₁ : ∀ (j_1 : Subtype p) (h₁ : ¬(↑j : J) = (↑j_1 : J)) (h₂ : j = j_1),
  Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) 0 (eqToHom sorry)
Tactic: classical
  ext
  rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π, biproduct.ι_π]
  split_ifs with h₁ h₂ h₂
  exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]
-- 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
w :
  ∀ (j_1 : Subtype p),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f (↑j : J)) (toSubtype f p))
        (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j_1))
      (CategoryStruct.comp (Y := 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_1))
w₁ :
  ∀ (j_1 : Subtype p),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1)
      (if h : (↑j : J) = (↑j_1 : J) then eqToHom ⋯ else 0) (if h : j = j_1 then eqToHom ⋯ else 0)
pos :
  ∀ (j_1 : Subtype p) (h₁ : (↑j : J) = (↑j_1 : J)) (h₂ : j = j_1),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) (eqToHom ⋯) (eqToHom ⋯)
neg :
  ∀ (j_1 : Subtype p) (h₁ : (↑j : J) = (↑j_1 : J)) (h₂ : ¬j = j_1),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) (eqToHom ⋯) 0
pos₁ :
  ∀ (j_1 : Subtype p) (h₁ : ¬(↑j : J) = (↑j_1 : J)) (h₂ : j = j_1),
    Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) 0 (eqToHom ⋯)
⊢ Eq.{v + 1} (α := f (↑j : J) ⟶ biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f (↑j : J)) (toSubtype f p))
    (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) j)
have neg₁ : ∀ (j_1 : Subtype p) (h₁ : ¬(↑j : J) = (↑j_1 : J)) (h₂ : ¬j = j_1),
  Eq.{v + 1} (α := f (↑j : J) ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f j_1) 0 0
Tactic: classical
  ext
  rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π, biproduct.ι_π]
  split_ifs with h₁ h₂ h₂
  exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]