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)
j : Subtype p
w :
  ∀ (j_1 : Subtype p),
    Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f j_1 ⟶ f (↑j : J))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) j_1)
        (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (π f (↑j : J))))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) j_1) (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j))
w₁ :
  ∀ (j_1 : Subtype p),
    Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f j_1 ⟶ f (↑j : J))
      (if h : (↑j_1 : J) = (↑j : J) then eqToHom ⋯ else 0) (if h : j_1 = j then eqToHom ⋯ else 0)
⊢ Eq.{v + 1} (α := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f) ⟶ f (↑j : J))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (π f (↑j : J)))
    (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j)
have pos : ∀ (j_1 : Subtype p) (h₁ : (↑j_1 : J) = (↑j : J)) (h₂ : j_1 = j),
  Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f j_1 ⟶ f (↑j : J)) (eqToHom sorry) (eqToHom sorry)
Tactic: classical
  ext
  rw [biproduct.fromSubtype, biproduct.ι_desc_assoc, 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} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f j_1 ⟶ f (↑j : J))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) j_1)
        (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (π f (↑j : J))))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) j_1) (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j))
w₁ :
  ∀ (j_1 : Subtype p),
    Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f j_1 ⟶ f (↑j : J))
      (if h : (↑j_1 : J) = (↑j : J) then eqToHom ⋯ else 0) (if h : j_1 = j then eqToHom ⋯ else 0)
pos :
  ∀ (j_1 : Subtype p) (h₁ : (↑j_1 : J) = (↑j : J)) (h₂ : j_1 = j),
    Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f j_1 ⟶ f (↑j : J)) (eqToHom ⋯) (eqToHom ⋯)
⊢ Eq.{v + 1} (α := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f) ⟶ f (↑j : J))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (π f (↑j : J)))
    (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j)
have neg : ∀ (j_1 : Subtype p) (h₁ : (↑j_1 : J) = (↑j : J)) (h₂ : ¬j_1 = j),
  Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f j_1 ⟶ f (↑j : J)) (eqToHom sorry) 0
Tactic: classical
  ext
  rw [biproduct.fromSubtype, biproduct.ι_desc_assoc, 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} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f j_1 ⟶ f (↑j : J))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) j_1)
        (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (π f (↑j : J))))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) j_1) (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j))
w₁ :
  ∀ (j_1 : Subtype p),
    Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f j_1 ⟶ f (↑j : J))
      (if h : (↑j_1 : J) = (↑j : J) then eqToHom ⋯ else 0) (if h : j_1 = j then eqToHom ⋯ else 0)
pos :
  ∀ (j_1 : Subtype p) (h₁ : (↑j_1 : J) = (↑j : J)) (h₂ : j_1 = j),
    Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f j_1 ⟶ f (↑j : J)) (eqToHom ⋯) (eqToHom ⋯)
neg :
  ∀ (j_1 : Subtype p) (h₁ : (↑j_1 : J) = (↑j : J)) (h₂ : ¬j_1 = j),
    Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f j_1 ⟶ f (↑j : J)) (eqToHom ⋯) 0
⊢ Eq.{v + 1} (α := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f) ⟶ f (↑j : J))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (π f (↑j : J)))
    (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j)
have pos₁ : ∀ (j_1 : Subtype p) (h₁ : ¬(↑j_1 : J) = (↑j : J)) (h₂ : j_1 = j),
  Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f j_1 ⟶ f (↑j : J)) 0 (eqToHom sorry)
Tactic: classical
  ext
  rw [biproduct.fromSubtype, biproduct.ι_desc_assoc, 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} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f j_1 ⟶ f (↑j : J))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) j_1)
        (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (π f (↑j : J))))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f))
        (ι (Subtype.restrict (β := fun (x : J) ↦ C) p f) j_1) (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j))
w₁ :
  ∀ (j_1 : Subtype p),
    Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f j_1 ⟶ f (↑j : J))
      (if h : (↑j_1 : J) = (↑j : J) then eqToHom ⋯ else 0) (if h : j_1 = j then eqToHom ⋯ else 0)
pos :
  ∀ (j_1 : Subtype p) (h₁ : (↑j_1 : J) = (↑j : J)) (h₂ : j_1 = j),
    Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f j_1 ⟶ f (↑j : J)) (eqToHom ⋯) (eqToHom ⋯)
neg :
  ∀ (j_1 : Subtype p) (h₁ : (↑j_1 : J) = (↑j : J)) (h₂ : ¬j_1 = j),
    Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f j_1 ⟶ f (↑j : J)) (eqToHom ⋯) 0
pos₁ :
  ∀ (j_1 : Subtype p) (h₁ : ¬(↑j_1 : J) = (↑j : J)) (h₂ : j_1 = j),
    Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f j_1 ⟶ f (↑j : J)) 0 (eqToHom ⋯)
⊢ Eq.{v + 1} (α := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f) ⟶ f (↑j : J))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (fromSubtype f p) (π f (↑j : J)))
    (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) j)
have neg₁ : ∀ (j_1 : Subtype p) (h₁ : ¬(↑j_1 : J) = (↑j : J)) (h₂ : ¬j_1 = j),
  Eq.{v + 1} (α := Subtype.restrict (β := fun (x : J) ↦ C) p f j_1 ⟶ f (↑j : J)) 0 0
Tactic: classical
  ext
  rw [biproduct.fromSubtype, biproduct.ι_desc_assoc, 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)
inst_4 : DecidablePred p
j : J
⊢ 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)
    (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))
Tactic: ext 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
j : J
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))
have w : 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: rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, 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)
inst_4 : DecidablePred p
j : J
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))
have pos : ∀ (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: by_cases h : p 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)
inst_4 : DecidablePred p
j : J
i : Subtype p
pos :
  ∀ (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 ⟶ 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))
have neg : ∀ (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: by_cases h : p 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)
inst_4 : DecidablePred p
j : J
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))
have pos : Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (if h : j = (↑i : J) then eqToHom sorry else 0)
  (if h_1 : Subtype.mk (p := p) j h = i then eqToHom sorry else 0)
Tactic: rw [dif_pos h, 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)
inst_4 : DecidablePred p
j : J
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)
    (if h_1 : Subtype.mk (p := p) j h = i then eqToHom ⋯ else 0)
have pos : ∀ (h₁ : j = (↑i : J)) (h₂ : Subtype.mk (p := p) j h = i),
  Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (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)
inst_4 : DecidablePred p
j : J
i : Subtype p
h : p j
pos :
  ∀ (h₁ : j = (↑i : J)) (h₂ : Subtype.mk (p := p) j h = i),
    Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (eqToHom ⋯) (eqToHom ⋯)
⊢ Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (if h : j = (↑i : J) then eqToHom ⋯ else 0)
    (if h_1 : Subtype.mk (p := p) j h = i then eqToHom ⋯ else 0)
have neg : ∀ (h₁ : j = (↑i : J)) (h₂ : ¬Subtype.mk (p := p) j h = i),
  Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (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)
inst_4 : DecidablePred p
j : J
i : Subtype p
h : p j
pos :
  ∀ (h₁ : j = (↑i : J)) (h₂ : Subtype.mk (p := p) j h = i),
    Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (eqToHom ⋯) (eqToHom ⋯)
neg :
  ∀ (h₁ : j = (↑i : J)) (h₂ : ¬Subtype.mk (p := p) j h = i),
    Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (eqToHom ⋯) 0
⊢ Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (if h : j = (↑i : J) then eqToHom ⋯ else 0)
    (if h_1 : Subtype.mk (p := p) j h = i then eqToHom ⋯ else 0)
have pos₁ : ∀ (h₁ : ¬j = (↑i : J)) (h₂ : Subtype.mk (p := p) j h = i),
  Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) 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)
inst_4 : DecidablePred p
j : J
i : Subtype p
h : p j
pos :
  ∀ (h₁ : j = (↑i : J)) (h₂ : Subtype.mk (p := p) j h = i),
    Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (eqToHom ⋯) (eqToHom ⋯)
neg :
  ∀ (h₁ : j = (↑i : J)) (h₂ : ¬Subtype.mk (p := p) j h = i),
    Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (eqToHom ⋯) 0
pos₁ :
  ∀ (h₁ : ¬j = (↑i : J)) (h₂ : Subtype.mk (p := p) j h = i),
    Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) 0 (eqToHom ⋯)
⊢ Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) (if h : j = (↑i : J) then eqToHom ⋯ else 0)
    (if h_1 : Subtype.mk (p := p) j h = i then eqToHom ⋯ else 0)
have neg₁ : ∀ (h₁ : ¬j = (↑i : J)) (h₂ : ¬Subtype.mk (p := p) j h = i),
  Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) 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)
inst_4 : DecidablePred p
j : J
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))
have neg : 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)) 0
    (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
Tactic: 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
i : Subtype p
h : ¬p j
neg :
  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)) 0
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
⊢ 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))
have neg₁ : Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) 0
  (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) 0
    (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
Tactic: 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
i : Subtype p
h : ¬p j
neg :
  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)) 0
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
neg₁ :
  Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) 0
    (CategoryStruct.comp (Y := biproduct.{w, v, u} (Subtype.restrict (β := fun (x : J) ↦ C) p f)) 0
      (π (Subtype.restrict (β := fun (x : J) ↦ C) p f) i))
⊢ 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))
have neg₂ : Eq.{v + 1} (α := f j ⟶ Subtype.restrict (β := fun (x : J) ↦ C) p f i) 0 0
Tactic: 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
⊢ 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)
    (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))
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]