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

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℝ
⊢ (support fun x => ↑(f x)) = support f
Tactic:
apply Function.support_comp_eq (g := ofReal')
State after:
case hg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℝ
⊢ ∀ {x : ℝ}, ↑x = 0 ↔ x = 0

State before:
case hg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
f : ℝ → ℝ
⊢ ∀ {x : ℝ}, ↑x = 0 ↔ x = 0
Tactic:
simp [ofReal_zero]
State after:
no goals