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

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
⊢ (support fun x => x) = Iio 0 ∪ Ioi 0
Tactic:
ext x
State after:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x : ℝ
⊢ (x ∈ support fun x => x) ↔ x ∈ Iio 0 ∪ Ioi 0

State before:
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
x : ℝ
⊢ (x ∈ support fun x => x) ↔ x ∈ Iio 0 ∪ Ioi 0
Tactic:
simp only [mem_support, ne_eq, Iio_union_Ioi, mem_compl_iff, mem_singleton_iff]
State after:
no goals