case w
J : Type w
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
⊢ ∀ (j_1 : Subtype p),
    (ι f j ≫ toSubtype f p) ≫ π (Subtype.restrict p f) j_1 =
      (if h : p j then ι (Subtype.restrict p f) { val := j, property := h } else 0) ≫ π (Subtype.restrict p f) j_1
J : Type w
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
⊢ ι f j ≫ toSubtype f p = if h : p j then ι (Subtype.restrict p f) { val := j, property := h } else 0
apply biproduct.hom_ext
case w
J : Type w
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
⊢ (ι f j ≫ toSubtype f p) ≫ π (Subtype.restrict p f) i =
    (if h : p j then ι (Subtype.restrict p f) { val := j, property := h } else 0) ≫ π (Subtype.restrict p f) i
case w
J : Type w
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
⊢ ∀ (j_1 : Subtype p),
    (ι f j ≫ toSubtype f p) ≫ π (Subtype.restrict p f) j_1 =
      (if h : p j then ι (Subtype.restrict p f) { val := j, property := h } else 0) ≫ π (Subtype.restrict p f) j_1
intro i
case w
J : Type w
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
⊢ (if h : j = ↑i then eqToHom (_ : f j = f ↑i) else 0) =
    (if h : p j then ι (Subtype.restrict p f) { val := j, property := h } else 0) ≫ π (Subtype.restrict p f) i
case w
J : Type w
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
⊢ (ι f j ≫ toSubtype f p) ≫ π (Subtype.restrict p f) i =
    (if h : p j then ι (Subtype.restrict p f) { val := j, property := h } else 0) ≫ π (Subtype.restrict p f) i
rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π]
case pos
J : Type w
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
⊢ (if h : j = ↑i then eqToHom (_ : f j = f ↑i) else 0) =
    (if h : p j then ι (Subtype.restrict p f) { val := j, property := h } else 0) ≫ π (Subtype.restrict p f) i

case neg
J : Type w
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : ¬p j
⊢ (if h : j = ↑i then eqToHom (_ : f j = f ↑i) else 0) =
    (if h : p j then ι (Subtype.restrict p f) { val := j, property := h } else 0) ≫ π (Subtype.restrict p f) i
case w
J : Type w
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
⊢ (if h : j = ↑i then eqToHom (_ : f j = f ↑i) else 0) =
    (if h : p j then ι (Subtype.restrict p f) { val := j, property := h } else 0) ≫ π (Subtype.restrict p f) i
by_cases h : p j
case pos
J : Type w
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
⊢ (if h : j = ↑i then eqToHom (_ : f j = f ↑i) else 0) =
    if h_1 : { val := j, property := h } = i then
      eqToHom (_ : Subtype.restrict p f { val := j, property := h } = Subtype.restrict p f i)
    else 0
case pos
J : Type w
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
⊢ (if h : j = ↑i then eqToHom (_ : f j = f ↑i) else 0) =
    (if h : p j then ι (Subtype.restrict p f) { val := j, property := h } else 0) ≫ π (Subtype.restrict p f) i
rw [dif_pos h, biproduct.ι_π]
case pos.inl.inl
J : Type w
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
h₁ : j = ↑i
h₂ : { val := j, property := h } = i
⊢ eqToHom (_ : f j = f ↑i) = eqToHom (_ : Subtype.restrict p f { val := j, property := h } = Subtype.restrict p f i)

case pos.inl.inr
J : Type w
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
h₁ : j = ↑i
h₂ : ¬{ val := j, property := h } = i
⊢ eqToHom (_ : f j = f ↑i) = 0

case pos.inr.inl
J : Type w
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
h₁ : ¬j = ↑i
h₂ : { val := j, property := h } = i
⊢ 0 = eqToHom (_ : Subtype.restrict p f { val := j, property := h } = Subtype.restrict p f i)

case pos.inr.inr
J : Type w
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
h₁ : ¬j = ↑i
h₂ : ¬{ val := j, property := h } = i
⊢ 0 = 0
case pos
J : Type w
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
⊢ (if h : j = ↑i then eqToHom (_ : f j = f ↑i) else 0) =
    if h_1 : { val := j, property := h } = i then
      eqToHom (_ : Subtype.restrict p f { val := j, property := h } = Subtype.restrict p f i)
    else 0
split_ifs with h₁ h₂ h₂
no goals
case pos.inl.inl
J : Type w
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
h₁ : j = ↑i
h₂ : { val := j, property := h } = i
⊢ eqToHom (_ : f j = f ↑i) = eqToHom (_ : Subtype.restrict p f { val := j, property := h } = Subtype.restrict p f i)

case pos.inl.inr
J : Type w
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
h₁ : j = ↑i
h₂ : ¬{ val := j, property := h } = i
⊢ eqToHom (_ : f j = f ↑i) = 0

case pos.inr.inl
J : Type w
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
h₁ : ¬j = ↑i
h₂ : { val := j, property := h } = i
⊢ 0 = eqToHom (_ : Subtype.restrict p f { val := j, property := h } = Subtype.restrict p f i)

case pos.inr.inr
J : Type w
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : p j
h₁ : ¬j = ↑i
h₂ : ¬{ val := j, property := h } = i
⊢ 0 = 0
exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]
no goals
case neg
J : Type w
C : Type u
inst✝⁴ : Category C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : ¬p j
⊢ (if h : j = ↑i then eqToHom (_ : f j = f ↑i) else 0) =
    (if h : p j then ι (Subtype.restrict p f) { val := j, property := h } else 0) ≫ π (Subtype.restrict p f) i
rw [dif_neg h, dif_neg (show j ≠ i from fun h₂ => h (h₂.symm ▸ i.2)), zero_comp]