simp only [mem_Icc, Pi.one_apply, Pi.le_def, mem_Ioo] at hΨ0 hΨ1
case right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
hΨContDiff : ContDiff ℝ ⊤ Ψ
left✝ : HasCompactSupport Ψ
hΨ0 : (fun x => if x ∈ Icc 1 (3 / 2) then 1 x else 0) ≤ Ψ
hΨ1 : Ψ ≤ fun x => if x ∈ Ioo (1 / 2) 2 then 1 x else 0
hΨSupport : Function.support Ψ = Ioo (1 / 2) 2
⊢ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x
case right
𝕂 : 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
⊢ (∀ (x : ℝ), 0 ≤ Ψ x) ∧ Function.support Ψ ⊆ Icc (1 / 2) 2 ∧ 0 < ∫ (x : ℝ) in Ici 0, Ψ x / x