Theorem: Function.support_mul_subset_of_subset (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
s : Set ℝ
f g : ℝ → 𝕂
fSupp : support f ⊆ s
⊢ support (f * g) ⊆ s
Tactic:
simp_rw [support_mul', inter_subset, subset_union_of_subset_right fSupp]
State after:
no goals