awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
a c : K
d : ℕ
left : ∀ a' < 0, ∀ᶠ (b : ℕ) in atTop, a' < a * c ^ b / (↑(b - d)! : K)
right : ∀ a' > 0, ∀ᶠ (b : ℕ) in atTop, a * c ^ b / (↑(b - d)! : K) < a'
⊢ (∀ a' < 0, ∀ᶠ (b : ℕ) in atTop, a' < a * c ^ b / (↑(b - d)! : K)) ∧
    ∀ a' > 0, ∀ᶠ (b : ℕ) in atTop, a * c ^ b / (↑(b - d)! : K) < a'

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε < 0
h : ∀ (n : ℕ) (h : a * ε⁻¹ * c ^ n < (↑(n - d)! : K)), ε < a * c ^ n / (↑(n - d)! : K)
⊢ ∀ᶠ (b : ℕ) in atTop, ε < a * c ^ b / (↑(b - d)! : K)

Tactic:
filter_upwards [eventually_mul_pow_lt_factorial_sub (a * ε⁻¹) c d] with n h

Premises used: HMul.hMul, Inv.inv, FloorSemiring.eventually_mul_pow_lt_factorial_sub
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε < 0
n : ℕ
h : a * ε⁻¹ * c ^ n < (↑(n - d)! : K)
⊢ a * c ^ n / ε < (↑(n - d)! : K)

Tactic:
rw [mul_right_comm, ← div_eq_mul_inv] at h

Premises used: div_eq_mul_inv, mul_right_comm
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε > 0
h : ∀ (n : ℕ) (h : a * ε⁻¹ * c ^ n < (↑(n - d)! : K)), a * c ^ n / (↑(n - d)! : K) < ε
⊢ ∀ᶠ (b : ℕ) in atTop, a * c ^ b / (↑(b - d)! : K) < ε

Tactic:
filter_upwards [eventually_mul_pow_lt_factorial_sub (a * ε⁻¹) c d] with n h

Premises used: HMul.hMul, Inv.inv, FloorSemiring.eventually_mul_pow_lt_factorial_sub
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε > 0
n : ℕ
h : a * ε⁻¹ * c ^ n < (↑(n - d)! : K)
⊢ a * c ^ n / ε < (↑(n - d)! : K)

Tactic:
rw [mul_right_comm, ← div_eq_mul_inv] at h

Premises used: div_eq_mul_inv, mul_right_comm
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε < 0
n : ℕ
h : a * c ^ n / ε < (↑(n - d)! : K)
⊢ (↑(n - d)! : K) * ε < a * c ^ n

Tactic:
rw [div_lt_iff_of_neg hε] at h

Premises used: div_lt_iff_of_neg
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε < 0
n : ℕ
h : (↑(n - d)! : K) * ε < a * c ^ n
h₁ h₂ h₃ h₄ : (↑(n - d)! : K) * ε < a * c ^ n
⊢ ε < a * c ^ n / (↑(n - d)! : K)

Tactic:
rwa [lt_div_iff₀' (Nat.cast_pos.mpr (Nat.factorial_pos _))]

Premises used: lt_div_iff₀'
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε > 0
n : ℕ
h : a * c ^ n / ε < (↑(n - d)! : K)
⊢ a * c ^ n < (↑(n - d)! : K) * ε

Tactic:
rw [div_lt_iff₀ hε] at h

Premises used: div_lt_iff₀
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε > 0
n : ℕ
h : a * c ^ n < (↑(n - d)! : K) * ε
h₁ h₂ h₃ h₄ : a * c ^ n < (↑(n - d)! : K) * ε
⊢ a * c ^ n / (↑(n - d)! : K) < ε

Tactic:
rwa [div_lt_iff₀' (Nat.cast_pos.mpr (Nat.factorial_pos _))]

Premises used: div_lt_iff₀'
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
c : K
⊢ Tendsto.{0, u_1} (β := K) (fun (n : ℕ) ↦ 1 * c ^ n / (↑(n - 0)! : K)) atTop (𝓝 0)

Tactic:
tendsto_mul_pow_div_factorial_sub_atTop 1 c 0

Premises used: FloorSemiring.tendsto_mul_pow_div_factorial_sub_atTop, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
c : K
h : ∀ (x : ℕ), c ^ x = 1 * c ^ x
⊢ Tendsto.{0, u_1} (β := K) (fun (n : ℕ) ↦ c ^ n / (↑n ! : K)) atTop (𝓝 0)

Tactic:
convert! tendsto_mul_pow_div_factorial_sub_atTop 1 c 0

Premises used: FloorSemiring.tendsto_mul_pow_div_factorial_sub_atTop, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
inst_3 : FloorSemiring K
inst_4 : TopologicalSpace K
inst_5 : OrderTopology K
c : K
x : ℕ
h h₁ : c ^ x = c ^ x
⊢ c ^ x = 1 * c ^ x

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : IsStrictOrderedRing α
b : ℤ
rw : b ≤ b + 1
⊢ b ≤ floor.{u_1} (α := α) (↑(b + 1) : α)

Tactic:
rw [floor_intCast]

Premises used: Int.floor_intCast
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : IsStrictOrderedRing α
b : ℤ
⊢ b ≤ b + 1

Tactic:
(lt_add_one _).le

Premises used: lt_add_one, LT.lt.le
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : IsStrictOrderedRing α
b : ℤ
⊢ b ≤ b + 1

Tactic:
exact (lt_add_one _).le

Premises used: lt_add_one, LT.lt.le
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : IsStrictOrderedRing α
⊢ Tendsto.{u_1, 0} (α := α) floor atBot atBot

Tactic:
floor_mono.tendsto_atBot_atBot fun b => ⟨b, (floor_intCast _).le⟩

Premises used: Int.cast, Monotone.tendsto_atBot_atBot, Int.floor_intCast, Int.floor_mono, Eq.le, Exists.intro
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : IsStrictOrderedRing α
⊢ Tendsto.{u_1, 0} (α := α) ceil atTop atTop

Tactic:
ceil_mono.tendsto_atTop_atTop fun b => ⟨b, (ceil_intCast _).ge⟩

Premises used: Int.cast, Eq.ge, Int.ceil_intCast, Exists.intro, Int.ceil_mono, Monotone.tendsto_atTop_atTop
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : IsStrictOrderedRing α
b : ℤ
rw : b - 1 ≤ b
⊢ ceil.{u_1} (α := α) (↑(b - 1) : α) ≤ b

Tactic:
rw [ceil_intCast]

Premises used: Int.ceil_intCast
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : IsStrictOrderedRing α
b : ℤ
⊢ b - 1 ≤ b

Tactic:
(sub_one_lt _).le

Premises used: LT.lt.le, sub_one_lt
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : IsStrictOrderedRing α
b : ℤ
⊢ b - 1 ≤ b

Tactic:
exact (sub_one_lt _).le

Premises used: LT.lt.le, sub_one_lt
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
n : ℤ
⊢ ContinuousOn (Y := α) (fun (x : α) ↦ (↑⌊x⌋ : α)) (Ico (↑n : α) (HAdd.hAdd (α := α) (↑n : α) 1))

Tactic:
(continuousOn_congr <| floor_eq_on_Ico' n).mpr continuousOn_const

Premises used: Iff.mpr, continuousOn_congr, Int.floor_eq_on_Ico', continuousOn_const
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
n : ℤ
⊢ ContinuousOn (Y := α) (fun (x : α) ↦ (↑⌈x⌉ : α)) (Ioc (HSub.hSub (α := α) (↑n : α) 1) (↑n : α))

Tactic:
(continuousOn_congr <| ceil_eq_on_Ioc' n).mpr continuousOn_const

Premises used: Iff.mpr, continuousOn_congr, continuousOn_const, Int.ceil_eq_on_Ioc'
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
x : α
⊢ Tendsto floor (𝓝[≥] x) (pure ⌊x⌋)

Tactic:
tendsto_pure.2 <| mem_of_superset (Ico_mem_nhdsGE <| lt_floor_add_one x) fun _y hy =>
    floor_eq_on_Ico _ _ ⟨(floor_le x).trans hy.1, hy.2⟩

Premises used: Iff.mpr, Int.floor, Int.lt_floor_add_one, Filter.tendsto_pure, And.right, And.left, And.intro, Int.floor_le, LE.le.trans, Ico_mem_nhdsGE, Int.floor_eq_on_Ico, Filter.mem_of_superset
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
n : ℤ
⊢ Tendsto.{u_1, 0} (α := α) floor (𝓝[≥] (↑n : α)) (pure n)

Tactic:
simpa only [floor_intCast] using tendsto_floor_right_pure_floor (n : α)

Premises used: Int.cast, Int.floor_intCast, tendsto_floor_right_pure_floor
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
x : α
⊢ Tendsto ceil (𝓝[≤] x) (pure ⌈x⌉)

Tactic:
tendsto_pure.2 <| mem_of_superset
    (Ioc_mem_nhdsLE <| sub_lt_iff_lt_add.2 <| ceil_lt_add_one _) fun _y hy =>
      ceil_eq_on_Ioc _ _ ⟨hy.1, hy.2.trans (le_ceil _)⟩

Premises used: Ioc_mem_nhdsLE, Iff.mpr, Int.le_ceil, Filter.tendsto_pure, And.right, Int.ceil_lt_add_one, And.left, And.intro, sub_lt_iff_lt_add, Int.ceil_eq_on_Ioc, LE.le.trans, Int.ceil, Filter.mem_of_superset
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
n : ℤ
⊢ Tendsto.{u_1, 0} (α := α) ceil (𝓝[≤] (↑n : α)) (pure n)

Tactic:
simpa only [ceil_intCast] using tendsto_ceil_left_pure_ceil (n : α)

Premises used: Int.cast, tendsto_ceil_left_pure_ceil, Int.ceil_intCast
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
x : α
rw : (↑⌈x⌉ : α) < x + 1
⊢ (↑(⌈x⌉ - 1) : α) < x

Tactic:
rw [cast_sub, cast_one, sub_lt_iff_lt_add]

Premises used: Int.cast_sub, sub_lt_iff_lt_add, Int.cast_one
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
x : α
⊢ (↑⌈x⌉ : α) < x + 1

Tactic:
ceil_lt_add_one _

Premises used: Int.ceil_lt_add_one
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
x : α
⊢ (↑⌈x⌉ : α) < x + 1

Tactic:
exact ceil_lt_add_one _

Premises used: Int.ceil_lt_add_one
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
x : α
h₁ : (↑(⌈x⌉ - 1) : α) < x
rw : x ≤ (↑⌈x⌉ : α)
⊢ x ≤ HAdd.hAdd (α := α) (↑(⌈x⌉ - 1) : α) 1

Tactic:
rw [cast_sub, cast_one, sub_add_cancel]

Premises used: Int.cast_sub, sub_add_cancel, Int.cast_one
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
x : α
h₁ : (↑(⌈x⌉ - 1) : α) < x
⊢ x ≤ (↑⌈x⌉ : α)

Tactic:
le_ceil _

Premises used: Int.le_ceil
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
x : α
h₁ : (↑(⌈x⌉ - 1) : α) < x
⊢ x ≤ (↑⌈x⌉ : α)

Tactic:
exact le_ceil _

Premises used: Int.le_ceil
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
n : ℤ
⊢ Tendsto.{u_1, 0} (α := α) floor (𝓝[<] (↑n : α)) (pure (n - 1))

Tactic:
simpa only [ceil_intCast] using tendsto_floor_left_pure_ceil_sub_one (n : α)

Premises used: Int.cast, Int.ceil_intCast, tendsto_floor_left_pure_ceil_sub_one
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
x : α
rw : (↑⌊x⌋ : α) ≤ x
⊢ HSub.hSub (α := α) (↑(⌊x⌋ + 1) : α) 1 ≤ x

Tactic:
rw [cast_add, cast_one, add_sub_cancel_right]

Premises used: Int.cast_add, add_sub_cancel_right, Int.cast_one
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
x : α
⊢ (↑⌊x⌋ : α) ≤ x

Tactic:
floor_le _

Premises used: Int.floor_le
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
x : α
⊢ (↑⌊x⌋ : α) ≤ x

Tactic:
exact floor_le _

Premises used: Int.floor_le
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
n : ℤ
⊢ Tendsto.{u_1, 0} (α := α) ceil (𝓝[>] (↑n : α)) (pure (n + 1))

Tactic:
simpa only [floor_intCast] using tendsto_ceil_right_pure_floor_add_one (n : α)

Premises used: Int.cast, Int.floor_intCast, tendsto_ceil_right_pure_floor_add_one
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
n : ℤ
⊢ Tendsto (β := α) (fun (x : α) ↦ (↑⌊x⌋ : α)) (𝓝[≥] (↑n : α)) (𝓝[≥] (↑n : α))

Tactic:
((tendsto_pure_pure _ _).comp (tendsto_floor_right_pure n)).mono_right <|
    pure_le_nhdsWithin le_rfl

Premises used: le_rfl, tendsto_floor_right_pure, Filter.tendsto_pure_pure, pure_le_nhdsWithin, Filter.Tendsto.mono_right, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
n : ℤ
⊢ Tendsto (β := α) (fun (x : α) ↦ (↑⌊x⌋ : α)) (𝓝[≥] (↑n : α)) (𝓝 (↑n : α))

Tactic:
(tendsto_floor_right n).mono_right inf_le_left

Premises used: tendsto_floor_right, inf_le_left, Filter.Tendsto.mono_right
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
n : ℤ
⊢ Tendsto (β := α) (fun (x : α) ↦ (↑⌈x⌉ : α)) (𝓝[≤] (↑n : α)) (𝓝[≤] (↑n : α))

Tactic:
((tendsto_pure_pure _ _).comp (tendsto_ceil_left_pure n)).mono_right <|
    pure_le_nhdsWithin le_rfl

Premises used: le_rfl, Filter.tendsto_pure_pure, tendsto_ceil_left_pure, pure_le_nhdsWithin, Filter.Tendsto.mono_right, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
n : ℤ
⊢ Tendsto (β := α) (fun (x : α) ↦ (↑⌈x⌉ : α)) (𝓝[≤] (↑n : α)) (𝓝 (↑n : α))

Tactic:
(tendsto_ceil_left n).mono_right inf_le_left

Premises used: tendsto_ceil_left, inf_le_left, Filter.Tendsto.mono_right
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
n : ℤ
rw : LE.le.{u_1} (α := Filter α) (pure (IntCast.intCast (n - 1))) (𝓝[≤] (↑(n - 1) : α))
⊢ pure (IntCast.intCast (n - 1)) ≤ 𝓝[≤] HSub.hSub (α := α) (↑n : α) 1

Tactic:
rw [← @cast_one α, ← cast_sub]

Premises used: Int.cast_sub, Int.cast_one
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
n : ℤ
⊢ LE.le.{u_1} (α := Filter α) (pure (IntCast.intCast (n - 1))) (𝓝[≤] (↑(n - 1) : α))

Tactic:
pure_le_nhdsWithin le_rfl

Premises used: le_rfl, Set.Mem, setOf, pure_le_nhdsWithin
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
n : ℤ
⊢ LE.le.{u_1} (α := Filter α) (pure (IntCast.intCast (n - 1))) (𝓝[≤] (↑(n - 1) : α))

Tactic:
exact pure_le_nhdsWithin le_rfl

Premises used: le_rfl, pure_le_nhdsWithin
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
n : ℤ
rw : LE.le.{u_1} (α := Filter α) (pure (IntCast.intCast (n + 1))) (𝓝[≥] (↑(n + 1) : α))
⊢ pure (IntCast.intCast (n + 1)) ≤ 𝓝[≥] HAdd.hAdd (α := α) (↑n : α) 1

Tactic:
rw [← @cast_one α, ← cast_add]

Premises used: Int.cast_add, Int.cast_one
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
n : ℤ
⊢ LE.le.{u_1} (α := Filter α) (pure (IntCast.intCast (n + 1))) (𝓝[≥] (↑(n + 1) : α))

Tactic:
pure_le_nhdsWithin le_rfl

Premises used: le_rfl, Set.Mem, setOf, pure_le_nhdsWithin
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
n : ℤ
⊢ LE.le.{u_1} (α := Filter α) (pure (IntCast.intCast (n + 1))) (𝓝[≥] (↑(n + 1) : α))

Tactic:
exact pure_le_nhdsWithin le_rfl

Premises used: le_rfl, pure_le_nhdsWithin
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
n : ℤ
⊢ Tendsto (fun (x : α) ↦ (↑⌊x⌋ : α)) (𝓝[<] (↑n : α)) (𝓝 (HSub.hSub (α := α) (↑n : α) 1))

Tactic:
(tendsto_floor_left n).mono_right inf_le_left

Premises used: inf_le_left, Filter.Tendsto.mono_right, tendsto_floor_left
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
n : ℤ
⊢ Tendsto (fun (x : α) ↦ (↑⌈x⌉ : α)) (𝓝[>] (↑n : α)) (𝓝 (HAdd.hAdd (α := α) (↑n : α) 1))

Tactic:
(tendsto_ceil_right n).mono_right inf_le_left

Premises used: inf_le_left, Filter.Tendsto.mono_right, tendsto_ceil_right
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsTopologicalAddGroup α
n : ℤ
⊢ ContinuousOn fract (Ico (↑n : α) (HAdd.hAdd (α := α) (↑n : α) 1))

Tactic:
continuousOn_id.sub (continuousOn_floor n)

Premises used: continuousOn_floor, Int.fract, ContinuousOn.sub, continuousOn_id
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
inst_5 : IsTopologicalAddGroup α
x : α
h : x ≠ (↑⌊x⌋ : α)
⊢ ContinuousAt fract x

Tactic:
(continuousOn_fract ⌊x⌋).continuousAt <|
    Ico_mem_nhds ((floor_le _).lt_of_ne h.symm) (lt_floor_add_one _)

Premises used: Int.floor, continuousOn_fract, Int.lt_floor_add_one, Ne.symm, LE.le.lt_of_ne, Int.floor_le, Ico_mem_nhds, ContinuousOn.continuousAt
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
inst_6 : IsTopologicalAddGroup α
n : ℤ
rw : Tendsto fract (𝓝[<] (↑n : α)) (𝓝 ((↑n : α) - HSub.hSub (α := α) (↑n : α) 1))
⊢ Tendsto.{u_1, u_1} (α := α) fract (𝓝[<] (↑n : α)) (𝓝 1)

Tactic:
rw [← sub_sub_cancel (n : α) 1]

Premises used: Int.cast, sub_sub_cancel, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
inst_6 : IsTopologicalAddGroup α
n : ℤ
⊢ Tendsto fract (𝓝[<] (↑n : α)) (𝓝 ((↑n : α) - HSub.hSub (α := α) (↑n : α) 1))

Tactic:
(tendsto_id.mono_left nhdsWithin_le_nhds).sub ?_

Premises used: Filter.tendsto_id, Int.fract, nhdsWithin_le_nhds, Filter.Tendsto.mono_left, Filter.Tendsto.sub
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
inst_6 : IsTopologicalAddGroup α
n : ℤ
refine : Tendsto (fun (x : α) ↦ (↑⌊x⌋ : α)) (𝓝[<] (↑n : α)) (𝓝 (HSub.hSub (α := α) (↑n : α) 1))
⊢ Tendsto fract (𝓝[<] (↑n : α)) (𝓝 ((↑n : α) - HSub.hSub (α := α) (↑n : α) 1))

Tactic:
refine (tendsto_id.mono_left nhdsWithin_le_nhds).sub ?_

Premises used: Filter.tendsto_id, nhdsWithin_le_nhds, Filter.Tendsto.mono_left, Filter.Tendsto.sub
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
inst_6 : IsTopologicalAddGroup α
n : ℤ
⊢ Tendsto (fun (x : α) ↦ (↑⌊x⌋ : α)) (𝓝[<] (↑n : α)) (𝓝 (HSub.hSub (α := α) (↑n : α) 1))

Tactic:
tendsto_floor_left' n

Premises used: tendsto_floor_left'
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
inst_6 : IsTopologicalAddGroup α
n : ℤ
⊢ Tendsto (fun (x : α) ↦ (↑⌊x⌋ : α)) (𝓝[<] (↑n : α)) (𝓝 (HSub.hSub (α := α) (↑n : α) 1))

Tactic:
exact tendsto_floor_left' n

Premises used: tendsto_floor_left'
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
inst_6 : IsTopologicalAddGroup α
n : ℤ
⊢ Tendsto.{u_1, u_1} (α := α) fract (𝓝[<] (↑n : α)) (𝓝[<] 1)

Tactic:
tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ (tendsto_fract_left' _)
    (Eventually.of_forall fract_lt_one)

Premises used: tendsto_fract_left', Filter.Eventually.of_forall, tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within, Int.fract_lt_one
-- Module: Mathlib.Topology.Algebra.Order.Floor
Goal:
α : Type u_1
inst : Ring α
inst_1 : LinearOrder α
inst_2 : FloorRing α
inst_3 : TopologicalSpace α
inst_4 : IsStrictOrderedRing α
inst_5 : OrderClosedTopology α
inst_6 : IsTopologicalAddGroup α
n : ℤ
⊢ Tendsto.{u_1, u_1} (α := α) fract (𝓝[≥] (↑n : α)) (𝓝 0)

Tactic:
sub_self (n : α) ▸ (tendsto_nhdsWithin_of_tendsto_nhds tendsto_id).sub (tendsto_floor_right' n)

Premises used: Int.cast, sub_self, Filter.tendsto_id, Eq.rec, tendsto_nhdsWithin_of_tendsto_nhds, Filter.Tendsto.sub, tendsto_floor_right'