exact fun h ↦ h.left.left
case h.mp
𝕂 : 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 : ℝ
⊢ ((1 / 2 < x ∧ x < 2) ∧ (x < 0 ∨ 0 < x)) ∧ 0 ≤ x → 1 / 2 < x ∧ x < 2
no goals