simp only [one_div, mem_Icc] at this
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : x ^ ε⁻¹ ∈ Icc (1 / 2) 2
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
x : ℝ
hx : 0 ≤ x
h : Ψ (x ^ ε⁻¹) ≠ 0 ∧ ε ≠ 0
this : 2⁻¹ ≤ x ^ ε⁻¹ ∧ x ^ ε⁻¹ ≤ 2
⊢ 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε