rcases h with ⟨Ψ, hΨ, hΨnonneg, hΨsupp, hΨpos⟩
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
h : ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ ∫ (x : ℝ) in Ici 0, Ψ x / x = 1
case intro.intro.intro.intro
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨ : ContDiff ℝ ⊤ Ψ
hΨnonneg : ∀ (x : ℝ), 0 ≤ Ψ x
hΨsupp : Function.support Ψ ⊆ Icc (1 / 2) 2
hΨpos : 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ ∃ Ψ, ContDiff ℝ ⊤ Ψ ∧ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ ∫ (x : ℝ) in Ici 0, Ψ x / x = 1