have := smooth_urysohn_support_Ioo (a := 1 / 2) (b := 1) (c := 3/2) (d := 2) (by linarith)
  (by linarith)
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
this :
  ∃ Ψ,
    ContDiff ℝ ⊤ Ψ ∧
      HasCompactSupport Ψ ∧
        (Icc 1 (3 / 2)).indicator 1 ≤ Ψ ∧ Ψ ≤ (Ioo (1 / 2) 2).indicator 1 ∧ Function.support Ψ = Ioo (1 / 2) 2
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x