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)
j : Subtype p
⊢ ∀ (j_1 : Subtype p),
    ι (Subtype.restrict p f) j_1 ≫ fromSubtype f p ≫ π f ↑j = ι (Subtype.restrict p f) j_1 ≫ π (Subtype.restrict p f) j
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)
j : Subtype p
⊢ fromSubtype f p ≫ π f ↑j = π (Subtype.restrict p f) j
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)
j i : Subtype p
⊢ ι (Subtype.restrict p f) i ≫ fromSubtype f p ≫ π f ↑j = ι (Subtype.restrict p f) i ≫ π (Subtype.restrict p f) j
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)
j : Subtype p
⊢ ∀ (j_1 : Subtype p),
    ι (Subtype.restrict p f) j_1 ≫ fromSubtype f p ≫ π f ↑j = ι (Subtype.restrict p f) j_1 ≫ π (Subtype.restrict p f) j
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)
j i : Subtype p
⊢ (if h : ↑i = ↑j then eqToHom (_ : f ↑i = f ↑j) else 0) =
    if h : i = j then eqToHom (_ : Subtype.restrict p f i = Subtype.restrict p f j) else 0
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)
j i : Subtype p
⊢ ι (Subtype.restrict p f) i ≫ fromSubtype f p ≫ π f ↑j = ι (Subtype.restrict p f) i ≫ π (Subtype.restrict p f) j
rw [biproduct.fromSubtype, biproduct.ι_desc_assoc, biproduct.ι_π, biproduct.ι_π]
case w.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)
j i : Subtype p
h₁ : ↑i = ↑j
h₂ : i = j
⊢ eqToHom (_ : f ↑i = f ↑j) = eqToHom (_ : Subtype.restrict p f i = Subtype.restrict p f j)

case w.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)
j i : Subtype p
h₁ : ↑i = ↑j
h₂ : ¬i = j
⊢ eqToHom (_ : f ↑i = f ↑j) = 0

case w.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)
j i : Subtype p
h₁ : ¬↑i = ↑j
h₂ : i = j
⊢ 0 = eqToHom (_ : Subtype.restrict p f i = Subtype.restrict p f j)

case w.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)
j i : Subtype p
h₁ : ¬↑i = ↑j
h₂ : ¬i = j
⊢ 0 = 0
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)
j i : Subtype p
⊢ (if h : ↑i = ↑j then eqToHom (_ : f ↑i = f ↑j) else 0) =
    if h : i = j then eqToHom (_ : Subtype.restrict p f i = Subtype.restrict p f j) else 0
split_ifs with h₁ h₂ h₂
no goals
case w.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)
j i : Subtype p
h₁ : ↑i = ↑j
h₂ : i = j
⊢ eqToHom (_ : f ↑i = f ↑j) = eqToHom (_ : Subtype.restrict p f i = Subtype.restrict p f j)

case w.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)
j i : Subtype p
h₁ : ↑i = ↑j
h₂ : ¬i = j
⊢ eqToHom (_ : f ↑i = f ↑j) = 0

case w.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)
j i : Subtype p
h₁ : ¬↑i = ↑j
h₂ : i = j
⊢ 0 = eqToHom (_ : Subtype.restrict p f i = Subtype.restrict p f j)

case w.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)
j i : Subtype p
h₁ : ¬↑i = ↑j
h₂ : ¬i = j
⊢ 0 = 0
exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]