ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
i : ι
⊢ ((if p i then ↑f i else 0) + if ¬p i then ↑f i else 0) = ↑f i
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
i : ι
⊢ ↑(filter p f + filter (fun i => ¬p i) f) i = ↑f i
simp only [add_apply, filter_apply]
no goals
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
i : ι
⊢ ((if p i then ↑f i else 0) + if ¬p i then ↑f i else 0) = ↑f i
split_ifs <;> simp only [add_zero, zero_add]