exact ⟨Nat.ceil (M * x), fun i hi => by simpa using Nat.ceil_mono ((div_le_iff hx).mp (hM hi))⟩
case intro.h.hs
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
g : ℝ → ℝ
hg : HasCompactSupport g
hx : 0 < x
M : ℝ
hM : M ∈ upperBounds (Function.support g)
⊢ BddAbove (Function.support fun x_1 => g (↑x_1 / x))
no goals