apply div_nonneg <| le_trans (by simp [apply_ite]) (hΨ0 y)
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∈ Function.support Ψ
⊢ 0 ≤ Ψ y / y
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
hΨ0 : ∀ (i : ℝ), (if 1 ≤ i ∧ i ≤ 3 / 2 then 1 else 0) ≤ Ψ i
hΨ1 : ∀ (i : ℝ), Ψ i ≤ if 1 / 2 < i ∧ i < 2 then 1 else 0
y : ℝ
h : y ∈ Function.support Ψ
⊢ 0 ≤ y