-- Mathlib/Topology/Algebra/Order/Floor.lean
theorem tendsto_mul_pow_div_factorial_sub_atTop (a c : K) (d : ℕ) :
    Tendsto (fun n ↦ a * c ^ n / (n - d)!) atTop (𝓝 0)

Proof state:
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
⊢ Tendsto (fun n => a * c ^ n / ↑(n - d)!) atTop (𝓝 0)

Tactic:
rw [tendsto_order]

Result:
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
⊢ (∀ a' < 0, ∀ᶠ (b : ℕ) in atTop, a' < a * c ^ b / ↑(b - d)!) ∧
    ∀ a' > 0, ∀ᶠ (b : ℕ) in atTop, a * c ^ b / ↑(b - d)! < a'

Proof state:
case right
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
⊢ ∀ a' > 0, ∀ᶠ (b : ℕ) in atTop, a * c ^ b / ↑(b - d)! < a'

Tactic:
intro ε hε

Result:
case right
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε > 0
⊢ ∀ᶠ (b : ℕ) in atTop, a * c ^ b / ↑(b - d)! < ε

Proof state:
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
⊢ (∀ a' < 0, ∀ᶠ (b : ℕ) in atTop, a' < a * c ^ b / ↑(b - d)!) ∧
    ∀ a' > 0, ∀ᶠ (b : ℕ) in atTop, a * c ^ b / ↑(b - d)! < a'

Tactic:
constructor

Result:
case left
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
⊢ ∀ a' < 0, ∀ᶠ (b : ℕ) in atTop, a' < a * c ^ b / ↑(b - d)!

case right
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
⊢ ∀ a' > 0, ∀ᶠ (b : ℕ) in atTop, a * c ^ b / ↑(b - d)! < a'

Proof state:
case h
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε > 0
n : ℕ
h : a * ε⁻¹ * c ^ n < ↑(n - d)!
⊢ a * c ^ n / ↑(n - d)! < ε

Tactic:
rw [mul_right_comm, ← div_eq_mul_inv] at h

Result:
case h
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε > 0
n : ℕ
h : a * c ^ n / ε < ↑(n - d)!
⊢ a * c ^ n / ↑(n - d)! < ε

Proof state:
case h
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε < 0
n : ℕ
h : ↑(n - d)! * ε < a * c ^ n
⊢ ε < a * c ^ n / ↑(n - d)!

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

Result:
no goals

Proof state:
case left
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
⊢ ∀ a' < 0, ∀ᶠ (b : ℕ) in atTop, a' < a * c ^ b / ↑(b - d)!

case right
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
⊢ ∀ a' > 0, ∀ᶠ (b : ℕ) in atTop, a * c ^ b / ↑(b - d)! < a'

Tactic:
all_goals
  intro ε hε
  filter_upwards [eventually_mul_pow_lt_factorial_sub (a * ε⁻¹) c d] with n h
  rw [mul_right_comm, ← div_eq_mul_inv] at h

Result:
case h
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε < 0
n : ℕ
h : a * c ^ n / ε < ↑(n - d)!
⊢ ε < a * c ^ n / ↑(n - d)!

case h
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε > 0
n : ℕ
h : a * c ^ n / ε < ↑(n - d)!
⊢ a * c ^ n / ↑(n - d)! < ε

Proof state:
case right
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε > 0
⊢ ∀ᶠ (b : ℕ) in atTop, a * c ^ b / ↑(b - d)! < ε

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

Result:
case h
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε > 0
n : ℕ
h : a * ε⁻¹ * c ^ n < ↑(n - d)!
⊢ a * c ^ n / ↑(n - d)! < ε

Proof state:
case h
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε > 0
n : ℕ
h : a * c ^ n / ε < ↑(n - d)!
⊢ a * c ^ n / ↑(n - d)! < ε

Tactic:
rw [div_lt_iff₀ hε] at h

Result:
case h
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε > 0
n : ℕ
h : a * c ^ n < ↑(n - d)! * ε
⊢ a * c ^ n / ↑(n - d)! < ε

Proof state:
case h
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε < 0
n : ℕ
h : a * c ^ n / ε < ↑(n - d)!
⊢ ε < a * c ^ n / ↑(n - d)!

Tactic:
rw [div_lt_iff_of_neg hε] at h

Result:
case h
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε < 0
n : ℕ
h : ↑(n - d)! * ε < a * c ^ n
⊢ ε < a * c ^ n / ↑(n - d)!

Proof state:
case h
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
a c : K
d : ℕ
ε : K
hε : ε > 0
n : ℕ
h : a * c ^ n < ↑(n - d)! * ε
⊢ a * c ^ n / ↑(n - d)! < ε

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

Result:
no goals