simp [hb, sqrt_pi_pos.ne']
case h
b : ℝ
hb : b ≠ 0
x : ℝ
⊢ (x ∈
      ((Function.support fun a => b) ∩ Function.support fun a => sqrt π) ∩
        Function.support fun x => rexp (-(b * x) ^ 2)) ↔
    x ∈ Set.univ
case h
b : ℝ
hb : b ≠ 0
x : ℝ
⊢ ¬rexp (-(b * x) ^ 2) = 0