refine ⟨hΨ.div_const c, fun y ↦ div_nonneg (hΨnonneg y) (le_of_lt hΨpos), ?_, ?_⟩
case h
𝕂 : 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
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ (ContDiff ℝ ⊤ fun y => Ψ y / c) ∧
    (∀ (x : ℝ), 0 ≤ Ψ x / c) ∧ (Function.support fun y => Ψ y / c) ⊆ Icc (1 / 2) 2 ∧ ∫ (x : ℝ) in Ici 0, Ψ x / c / x = 1
case h.refine_1
𝕂 : 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
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ (Function.support fun y => Ψ y / c) ⊆ Icc (1 / 2) 2

case h.refine_2
𝕂 : 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
c : ℝ := ∫ (x : ℝ) in Ici 0, Ψ x / x
⊢ ∫ (x : ℝ) in Ici 0, Ψ x / c / x = 1