filter_upwards with x hx
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
⊢ ∀ᵐ (x : ℝ),
    x ∈ Ioi 0 →
      (fun x => ↑(Ψ (x ^ (1 / ε)) / ε)) x * ↑x ^ (s - 1) =
        (|1 / ε| * x ^ (1 / ε - 1)) • (↑(Ψ (x ^ (1 / ε))) * ↑(x ^ (1 / ε)) ^ (↑ε * s - 1))
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : ε > 0
s : ℂ
x : ℝ
hx : x ∈ Ioi 0
⊢ ↑(Ψ (x ^ (1 / ε)) / ε) * ↑x ^ (s - 1) =
    (|1 / ε| * x ^ (1 / ε - 1)) • (↑(Ψ (x ^ (1 / ε))) * ↑(x ^ (1 / ε)) ^ (↑ε * s - 1))