α : Type ?u.500878
β : Type ?u.500881
ι : Type ?u.500884
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 (a - 0))
⊢ Tendsto (fun x => ↑⌊a * x⌋₊ / x) atTop (𝓝 a)
α : Type ?u.500878
β : Type ?u.500881
ι : Type ?u.500884
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
⊢ Tendsto (fun x => ↑⌊a * x⌋₊ / x) atTop (𝓝 a)
have A : Tendsto (fun x : R => a - x⁻¹) atTop (𝓝 (a - 0)) :=
  tendsto_const_nhds.sub tendsto_inv_atTop_zero
α : Type ?u.500878
β : Type ?u.500881
ι : Type ?u.500884
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
⊢ Tendsto (fun x => ↑⌊a * x⌋₊ / x) atTop (𝓝 a)
α : Type ?u.500878
β : Type ?u.500881
ι : Type ?u.500884
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 (a - 0))
⊢ Tendsto (fun x => ↑⌊a * x⌋₊ / x) atTop (𝓝 a)
rw [sub_zero] at A
case hgf
α : Type ?u.500878
β : Type ?u.500881
ι : Type ?u.500884
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, a - b⁻¹ ≤ ↑⌊a * b⌋₊ / b

case hfh
α : Type ?u.500878
β : Type ?u.500881
ι : Type ?u.500884
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, ↑⌊a * b⌋₊ / b ≤ a
α : Type ?u.500878
β : Type ?u.500881
ι : Type ?u.500884
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
⊢ Tendsto (fun x => ↑⌊a * x⌋₊ / x) atTop (𝓝 a)
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' A tendsto_const_nhds
case hgf
α : Type ?u.500878
β : Type ?u.500881
ι : Type ?u.500884
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
⊢ a - x⁻¹ ≤ ↑⌊a * x⌋₊ / x
case hgf
α : Type ?u.500878
β : Type ?u.500881
ι : Type ?u.500884
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, a - b⁻¹ ≤ ↑⌊a * b⌋₊ / b
refine' eventually_atTop.2 ⟨1, fun x hx => _⟩
case hgf
α : Type ?u.500878
β : Type ?u.500881
ι : Type ?u.500884
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
⊢ a * x - 1 ≤ ↑⌊a * x⌋₊
case hgf
α : Type ?u.500878
β : Type ?u.500881
ι : Type ?u.500884
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
⊢ a - x⁻¹ ≤ ↑⌊a * x⌋₊ / x
simp only [le_div_iff (zero_lt_one.trans_le hx), _root_.sub_mul,
  inv_mul_cancel (zero_lt_one.trans_le hx).ne']
case hgf
α : Type ?u.500878
β : Type ?u.500881
ι : Type ?u.500884
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
this : a * x < ↑⌊a * x⌋₊ + 1
⊢ a * x - 1 ≤ ↑⌊a * x⌋₊
case hgf
α : Type ?u.500878
β : Type ?u.500881
ι : Type ?u.500884
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
⊢ a * x - 1 ≤ ↑⌊a * x⌋₊
have := Nat.lt_floor_add_one (a * x)
no goals
case hgf
α : Type ?u.500878
β : Type ?u.500881
ι : Type ?u.500884
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
this : a * x < ↑⌊a * x⌋₊ + 1
⊢ a * x - 1 ≤ ↑⌊a * x⌋₊
linarith
case hfh
α : Type ?u.500878
β : Type ?u.500881
ι : Type ?u.500884
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
⊢ ↑⌊a * x⌋₊ / x ≤ a
case hfh
α : Type ?u.500878
β : Type ?u.500881
ι : Type ?u.500884
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, ↑⌊a * b⌋₊ / b ≤ a
refine' eventually_atTop.2 ⟨1, fun x hx => _⟩
case hfh
α : Type ?u.500878
β : Type ?u.500881
ι : Type ?u.500884
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
⊢ ↑⌊a * x⌋₊ ≤ a * x
case hfh
α : Type ?u.500878
β : Type ?u.500881
ι : Type ?u.500884
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
⊢ ↑⌊a * x⌋₊ / x ≤ a
rw [div_le_iff (zero_lt_one.trans_le hx)]
no goals
case hfh
α : Type ?u.500878
β : Type ?u.500881
ι : Type ?u.500884
R : Type u_1
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun x => a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
⊢ ↑⌊a * x⌋₊ ≤ a * x
simp [Nat.floor_le (mul_nonneg ha (zero_le_one.trans hx))]