rcases this with ⟨Ψ, hΨContDiff, _, hΨ0, hΨ1, hΨSupport⟩
𝕂 : 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
case intro.intro.intro.intro.intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨ0 : (Icc 1 (3 / 2)).indicator 1 ≤ Ψ
hΨ1 : Ψ ≤ (Ioo (1 / 2) 2).indicator 1
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x