rw [Function.support_div, Function.support_const (ne_of_lt hΨpos).symm, inter_univ]
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_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) ⊆ Icc (1 / 2) 2