have hx2 := Smooth1Properties_above_aux hx hε
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
⊢ Smooth1 Ψ ε x = 0
case h.right
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
ε : ℝ
hε : ε ∈ Ioo 0 1
c : ℝ := 2 * Real.log 2
x : ℝ
hx : 1 + c * ε ≤ x
hx2 : 2 ^ ε < x
⊢ Smooth1 Ψ ε x = 0