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
i : J
⊢ ι f i ≫ toSubtype f p ≫ fromSubtype f p = ι f i ≫ map fun j => if p j then 𝟙 (f j) else 0
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
⊢ toSubtype f p ≫ fromSubtype f p = map fun j => if p j then 𝟙 (f j) else 0
ext1 i
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
i : J
h : p i
⊢ ι f i ≫ toSubtype f p ≫ fromSubtype f p = ι f i ≫ map fun j => if p j then 𝟙 (f j) else 0

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
i : J
h : ¬p i
⊢ ι f i ≫ toSubtype f p ≫ fromSubtype f p = ι f i ≫ map fun j => if p j then 𝟙 (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)
inst✝ : DecidablePred p
i : J
⊢ ι f i ≫ toSubtype f p ≫ fromSubtype f p = ι f i ≫ map fun j => if p j then 𝟙 (f j) else 0
by_cases h : p i
no goals
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
i : J
h : p i
⊢ ι f i ≫ toSubtype f p ≫ fromSubtype f p = ι f i ≫ map fun j => if p j then 𝟙 (f j) else 0
simp [h]
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
i : J
h : ¬p i
⊢ ι f i ≫ toSubtype f p ≫ fromSubtype f p = ι f i ≫ map fun j => if p j then 𝟙 (f j) else 0
simp [h]