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

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
α : Type u_2
f : α → 𝕂
⊢ (support fun x => ‖f x‖) = support f
Tactic:
simp only [support, ne_eq, mem_setOf_eq]
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
α : Type u_2
f : α → 𝕂
⊢ {x | ¬‖f x‖ = 0} = {x | ¬f x = 0}

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
α : Type u_2
f : α → 𝕂
⊢ {x | ¬‖f x‖ = 0} = {x | ¬f x = 0}
Tactic:
simp_rw [norm_ne_zero_iff]
State after:
no goals