simp only [one_div, Function.support_subset_iff, ne_eq, ite_eq_left_iff, not_lt, div_eq_zero_iff,
  not_forall, exists_prop, mem_Icc, and_imp]
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
⊢ (Function.support fun x => if x < 0 then 0 else Ψ (x ^ (1 / ε)) / ε) ⊆ Icc (2 ^ (-ε)) (2 ^ ε)
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
⊢ ∀ (x : ℝ), 0 ≤ x → ¬(Ψ (x ^ ε⁻¹) = 0 ∨ ε = 0) → 2 ^ (-ε) ≤ x ∧ x ≤ 2 ^ ε