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

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

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

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

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