α : Type ?u.113642
β : Type ?u.113645
γ : Type ?u.113648
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y✝ z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
x y : ℝ≥0∞
h : ∀ (a : ℝ≥0∞), a < 1 → a * x ≤ y
this : Tendsto (fun x_1 => x_1 * x) (𝓝[Iio 1] 1) (𝓝 x)
⊢ x ≤ y
α : Type ?u.113642
β : Type ?u.113645
γ : Type ?u.113648
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y✝ z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
x y : ℝ≥0∞
h : ∀ (a : ℝ≥0∞), a < 1 → a * x ≤ y
this : Tendsto (fun x_1 => x_1 * x) (𝓝[Iio 1] 1) (𝓝 (1 * x))
⊢ x ≤ y
rw [one_mul] at this
no goals
α : Type ?u.113642
β : Type ?u.113645
γ : Type ?u.113648
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y✝ z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
x y : ℝ≥0∞
h : ∀ (a : ℝ≥0∞), a < 1 → a * x ≤ y
this : Tendsto (fun x_1 => x_1 * x) (𝓝[Iio 1] 1) (𝓝 x)
⊢ x ≤ y
exact le_of_tendsto this (eventually_nhdsWithin_iff.2 <| eventually_of_forall h)