Theorem: Finsupp.mul_filter (Etch/Verification/Misc.lean)

State before:
m : Type u → Type v
inst✝³ : Monad m
ι : Type u_2
P Q : ι → Prop
inst✝² : DecidablePred P
inst✝¹ : DecidablePred Q
β : Type u_1
inst✝ : MulZeroClass β
f g : ι →₀ β
⊢ filter P f * filter Q g = filter (fun i => P i ∧ Q i) (f * g)
Tactic:
ext i
State after:
case h
m : Type u → Type v
inst✝³ : Monad m
ι : Type u_2
P Q : ι → Prop
inst✝² : DecidablePred P
inst✝¹ : DecidablePred Q
β : Type u_1
inst✝ : MulZeroClass β
f g : ι →₀ β
i : ι
⊢ (filter P f * filter Q g) i = (filter (fun i => P i ∧ Q i) (f * g)) i

State before:
case h
m : Type u → Type v
inst✝³ : Monad m
ι : Type u_2
P Q : ι → Prop
inst✝² : DecidablePred P
inst✝¹ : DecidablePred Q
β : Type u_1
inst✝ : MulZeroClass β
f g : ι →₀ β
i : ι
⊢ (filter P f * filter Q g) i = (filter (fun i => P i ∧ Q i) (f * g)) i
Tactic:
by_cases h₁ : P i <;> by_cases h₂ : Q i <;> simp [h₁, h₂]
State after:
no goals