case h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → AddZeroClass (β i)
p : ι → Prop
inst✝ : DecidablePred p
f g : Π₀ (i : ι), β i
i✝ : ι
⊢ ↑(filter p (f + g)) i✝ = ↑(filter p f + filter p g) i✝
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → AddZeroClass (β i)
p : ι → Prop
inst✝ : DecidablePred p
f g : Π₀ (i : ι), β i
⊢ filter p (f + g) = filter p f + filter p g
ext
no goals
case h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → AddZeroClass (β i)
p : ι → Prop
inst✝ : DecidablePred p
f g : Π₀ (i : ι), β i
i✝ : ι
⊢ ↑(filter p (f + g)) i✝ = ↑(filter p f + filter p g) i✝
simp [ite_add_zero]