awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
val : Encodable ι
a : ℝ≥0
a0 : 0 < a
aε : a < ε
ε' : ι → ℝ
hε' : ∀ (i : ι), 0 < ε' i
c : ℝ
hc : HasSum ε' c
hcε : c ≤ (↑a : ℝ)
⊢ ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ≥0), HasSum ε' c ∧ c < ε

Tactic:
⟨fun i ↦ ⟨ε' i, (hε' i).le⟩, fun i ↦ NNReal.coe_lt_coe.1 <| hε' i,
      ⟨c, hasSum_le (fun i ↦ (hε' i).le) hasSum_zero hc⟩, NNReal.hasSum_coe.1 hc,
      aε.trans_le' <| NNReal.coe_le_coe.1 hcε⟩

Premises used: hasSum_le, LT.lt.le, LT.lt.trans_le', Subtype.mk, hasSum_zero, And.intro, Exists.intro, Iff.mp, NNReal.coe_lt_coe, NNReal.hasSum_coe, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ε : ℝ≥0
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
val : Encodable ι
a : ℝ≥0
a0 : 0 < a
aε : a < ε
ε' : ι → ℝ
hε' : ∀ (i : ι), 0 < ε' i
c : ℝ
hc : HasSum ε' c
hcε : c ≤ (↑a : ℝ)
⊢ ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∃ (c : ℝ≥0), HasSum ε' c ∧ c < ε

Tactic:
exact
    ⟨fun i ↦ ⟨ε' i, (hε' i).le⟩, fun i ↦ NNReal.coe_lt_coe.1 <| hε' i,
      ⟨c, hasSum_le (fun i ↦ (hε' i).le) hasSum_zero hc⟩, NNReal.hasSum_coe.1 hc,
      aε.trans_le' <| NNReal.coe_le_coe.1 hcε⟩
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
rcases :
  ∀ (r : ℝ≥0∞) (h0r : 0 < r) (hrε : r < ε), ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), (↑(ε' i) : ℝ≥0∞) < ε
⊢ ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), (↑(ε' i) : ℝ≥0∞) < ε

Tactic:
rcases exists_between (pos_iff_ne_zero.2 hε) with ⟨r, h0r, hrε⟩

Premises used: Iff.mpr, exists_between, pos_iff_ne_zero
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
r : ℝ≥0∞
h0r : 0 < r
hrε : r < ε
rcases :
  ∀ (x : ℝ≥0),
    (↑x : ℝ≥0∞) < ε →
      ∀ (h0r : 0 < (↑x : ℝ≥0∞)) (hrε : (↑x : ℝ≥0∞) < ε),
        ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), (↑(ε' i) : ℝ≥0∞) < ε
⊢ ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), (↑(ε' i) : ℝ≥0∞) < ε

Tactic:
rcases lt_iff_exists_coe.1 hrε with ⟨x, rfl, _⟩

Premises used: ENNReal.lt_iff_exists_coe, Iff.mp, rfl
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
x : ℝ≥0
right : (↑x : ℝ≥0∞) < ε
h0r : 0 < (↑x : ℝ≥0∞)
hrε : (↑x : ℝ≥0∞) < ε
rcases :
  ∀ (ε' : ι → ℝ≥0) (hp : ∀ (i : ι), 0 < ε' i) (c : ℝ≥0) (hc : HasSum ε' c) (hcr : c < x),
    ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), (↑(ε' i) : ℝ≥0∞) < ε
⊢ ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), (↑(ε' i) : ℝ≥0∞) < ε

Tactic:
rcases NNReal.exists_pos_sum_of_countable (coe_pos.1 h0r).ne' ι with ⟨ε', hp, c, hc, hcr⟩

Premises used: NNReal.exists_pos_sum_of_countable, LT.lt.ne', ENNReal.coe_pos, Iff.mp
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
x : ℝ≥0
right : (↑x : ℝ≥0∞) < ε
h0r : 0 < (↑x : ℝ≥0∞)
hrε : (↑x : ℝ≥0∞) < ε
ε' : ι → ℝ≥0
hp : ∀ (i : ι), 0 < ε' i
c : ℝ≥0
hc : HasSum ε' c
hcr : c < x
⊢ ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), (↑(ε' i) : ℝ≥0∞) < ε

Tactic:
⟨ε', hp, (ENNReal.tsum_coe_eq hc).symm ▸ lt_trans (coe_lt_coe.2 hcr) hrε⟩

Premises used: Iff.mpr, lt_trans, ENNReal.coe_lt_coe, Eq.rec, ENNReal.tsum_coe_eq, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
x : ℝ≥0
right : (↑x : ℝ≥0∞) < ε
h0r : 0 < (↑x : ℝ≥0∞)
hrε : (↑x : ℝ≥0∞) < ε
ε' : ι → ℝ≥0
hp : ∀ (i : ι), 0 < ε' i
c : ℝ≥0
hc : HasSum ε' c
hcr : c < x
⊢ ∃ (ε' : ι → ℝ≥0), (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), (↑(ε' i) : ℝ≥0∞) < ε

Tactic:
exact ⟨ε', hp, (ENNReal.tsum_coe_eq hc).symm ▸ lt_trans (coe_lt_coe.2 hcr) hrε⟩
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
⊢ ∃ (ε' : ι → ℝ≥0∞), (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ε' i < ε

Tactic:
let ⟨δ, δpos, hδ⟩ := exists_pos_sum_of_countable hε ι
  ⟨fun i ↦ δ i, fun i ↦ ENNReal.coe_pos.2 (δpos i), hδ⟩

Premises used: Iff.mpr, ENNReal.ofNNReal, Exists, ENNReal.coe_pos, ENNReal.exists_pos_sum_of_countable, And, _private.0.ENNReal.exists_pos_sum_of_countable'.match_1, tsum, And.intro, LT.lt, Exists.intro, SummationFilter.unconditional
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
w : ι → ℝ≥0∞
hw : ∀ (i : ι), w i ≠ ∞
⊢ ∀ (i : ι), w i ≠ ∞

Tactic:
hw
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
w : ι → ℝ≥0∞
hw : ∀ (i : ι), w i ≠ ∞
lift :
  ∀ (w : (i : ι) → ℝ≥0),
    ∃ (δ : ι → ℝ≥0), (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * (↑(δ i) : ℝ≥0∞) < ε
⊢ ∃ (δ : ι → ℝ≥0), (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), w i * (↑(δ i) : ℝ≥0∞) < ε

Tactic:
lift w to ι → ℝ≥0 using hw
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
w : (i : ι) → ℝ≥0
rcases :
  ∀ (δ' : ι → ℝ≥0) (Hpos : ∀ (i : ι), 0 < δ' i) (Hsum : ∑' (i : ι), (↑(δ' i) : ℝ≥0∞) < ε),
    ∃ (δ : ι → ℝ≥0), (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * (↑(δ i) : ℝ≥0∞) < ε
⊢ ∃ (δ : ι → ℝ≥0), (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * (↑(δ i) : ℝ≥0∞) < ε

Tactic:
rcases exists_pos_sum_of_countable hε ι with ⟨δ', Hpos, Hsum⟩

Premises used: ENNReal.exists_pos_sum_of_countable
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), (↑(δ' i) : ℝ≥0∞) < ε
⊢ ∀ (i : ι), 0 < max 1 (w i)

Tactic:
have : ∀ i, 0 < max 1 (w i) := fun i ↦ zero_lt_one.trans_le (le_max_left _ _)
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), (↑(δ' i) : ℝ≥0∞) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
⊢ ∃ (δ : ι → ℝ≥0), (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * (↑(δ i) : ℝ≥0∞) < ε

Tactic:
⟨fun i ↦ δ' i / max 1 (w i), fun i ↦ div_pos (Hpos _) (this i), ?_⟩

Premises used: HDiv.hDiv, Max.max, And.intro, Exists.intro, div_pos, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), (↑(δ' i) : ℝ≥0∞) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
refine : ∑' (i : ι), (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * (↑((fun (i : ι) ↦ δ' i / max 1 (w i)) i) : ℝ≥0∞) < ε
⊢ ∃ (δ : ι → ℝ≥0), (∀ (i : ι), 0 < δ i) ∧ ∑' (i : ι), (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * (↑(δ i) : ℝ≥0∞) < ε

Tactic:
refine ⟨fun i ↦ δ' i / max 1 (w i), fun i ↦ div_pos (Hpos _) (this i), ?_⟩
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), (↑(δ' i) : ℝ≥0∞) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
⊢ ∑' (i : ι), (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * (↑((fun (i : ι) ↦ δ' i / max 1 (w i)) i) : ℝ≥0∞) < ε

Tactic:
lt_of_le_of_lt (ENNReal.tsum_le_tsum fun i ↦ ?_) Hsum

Premises used: lt_of_le_of_lt, ENNReal.tsum_le_tsum
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), (↑(δ' i) : ℝ≥0∞) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
refine :
  ∀ (i : ι), (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * (↑((fun (i : ι) ↦ δ' i / max 1 (w i)) i) : ℝ≥0∞) ≤ (↑(δ' i) : ℝ≥0∞)
⊢ ∑' (i : ι), (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * (↑((fun (i : ι) ↦ δ' i / max 1 (w i)) i) : ℝ≥0∞) < ε

Tactic:
refine lt_of_le_of_lt (ENNReal.tsum_le_tsum fun i ↦ ?_) Hsum

Premises used: lt_of_le_of_lt, ENNReal.tsum_le_tsum
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), (↑(δ' i) : ℝ≥0∞) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
i : ι
rw : (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * ((↑(δ' i) : ℝ≥0∞) / (↑(max 1 (w i)) : ℝ≥0∞)) ≤ (↑(δ' i) : ℝ≥0∞)
⊢ (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * (↑((fun (i : ι) ↦ δ' i / max 1 (w i)) i) : ℝ≥0∞) ≤ (↑(δ' i) : ℝ≥0∞)

Tactic:
rw [coe_div (this i).ne']

Premises used: LT.lt.ne', ENNReal.coe_div
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), (↑(δ' i) : ℝ≥0∞) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
i : ι
⊢ (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * ((↑(δ' i) : ℝ≥0∞) / (↑(max 1 (w i)) : ℝ≥0∞)) ≤ (↑(δ' i) : ℝ≥0∞)

Tactic:
mul_le_of_le_div' ?_

Premises used: ENNReal.mul_le_of_le_div'
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), (↑(δ' i) : ℝ≥0∞) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
i : ι
refine : (↑(δ' i) : ℝ≥0∞) / (↑(max 1 (w i)) : ℝ≥0∞) ≤ (↑(δ' i) : ℝ≥0∞) / (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i
⊢ (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i * ((↑(δ' i) : ℝ≥0∞) / (↑(max 1 (w i)) : ℝ≥0∞)) ≤ (↑(δ' i) : ℝ≥0∞)

Tactic:
refine mul_le_of_le_div' ?_

Premises used: ENNReal.mul_le_of_le_div'
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
ε : ℝ≥0∞
hε : ε ≠ 0
ι : Type u_4
inst : Countable ι
w δ' : ι → ℝ≥0
Hpos : ∀ (i : ι), 0 < δ' i
Hsum : ∑' (i : ι), (↑(δ' i) : ℝ≥0∞) < ε
this : ∀ (i : ι), 0 < max 1 (w i)
i : ι
grw grw₁ : (↑(δ' i) : ℝ≥0∞) / (↑(w i) : ℝ≥0∞) ≤ (↑(δ' i) : ℝ≥0∞) / (↑(w i) : ℝ≥0∞)
⊢ (↑(δ' i) : ℝ≥0∞) / (↑(max 1 (w i)) : ℝ≥0∞) ≤ (↑(δ' i) : ℝ≥0∞) / (fun (i : ι) ↦ (↑(w i) : ℝ≥0∞)) i

Tactic:
grw [← le_max_right]

Premises used: le_max_right
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
⊢ Tendsto factorial atTop atTop

Tactic:
tendsto_atTop_atTop_of_monotone (fun _ _ ↦ Nat.factorial_le) fun n ↦ ⟨n, n.self_le_factorial⟩

Premises used: Filter.tendsto_atTop_atTop_of_monotone, Exists.intro, Nat.factorial_le, Nat.self_le_factorial
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
⊢ ∀ᶠ (b : ℕ) in atTop, (↑b ! : ℝ) / HPow.hPow (α := ℝ) (↑b : ℝ) b ≤ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ)

Tactic:
(eventually_gt_atTop 0).mono fun n hn ↦ ?_

Premises used: Filter.Eventually.mono, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
refine : ∀ (n : ℕ) (hn : 0 < n), (↑n ! : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) n ≤ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)
⊢ ∀ᶠ (b : ℕ) in atTop, (↑b ! : ℝ) / HPow.hPow (α := ℝ) (↑b : ℝ) b ≤ HDiv.hDiv (α := ℝ) 1 (↑b : ℝ)

Tactic:
refine (eventually_gt_atTop 0).mono fun n hn ↦ ?_

Premises used: Filter.Eventually.mono, OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
n : ℕ
hn : 0 < n
rcases :
  ∀ (k : ℕ) (hn : 0 < k.succ),
    (↑k.succ ! : ℝ) / HPow.hPow (α := ℝ) (↑k.succ : ℝ) k.succ ≤ HDiv.hDiv (α := ℝ) 1 (↑k.succ : ℝ)
⊢ (↑n ! : ℝ) / HPow.hPow (α := ℝ) (↑n : ℝ) n ≤ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)

Tactic:
rcases Nat.exists_eq_succ_of_ne_zero hn.ne.symm with ⟨k, rfl⟩

Premises used: Ne.symm, Nat.exists_eq_succ_of_ne_zero, rfl, LT.lt.ne
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
k : ℕ
hn : 0 < k.succ
rw :
  (∏ k_1 ∈ Finset.range k, (↑(k_1 + 1 + 1) : ℝ) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹) *
      ((↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹) ≤
    (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹
⊢ (↑k.succ ! : ℝ) / HPow.hPow (α := ℝ) (↑k.succ : ℝ) k.succ ≤ HDiv.hDiv (α := ℝ) 1 (↑k.succ : ℝ)

Tactic:
rw [factorial_eq_prod_range_add_one, pow_eq_prod_const, div_eq_mul_inv, ← inv_eq_one_div,
        prod_natCast, Nat.cast_succ, ← Finset.prod_inv_distrib, ← prod_mul_distrib,
        Finset.prod_range_succ']

Premises used: Nat.cast_succ, Finset.prod_range_succ', Finset.prod_mul_distrib, Finset.prod_inv_distrib, inv_eq_one_div, div_eq_mul_inv, Finset.prod_natCast, Nat.factorial_eq_prod_range_add_one, Finset.pow_eq_prod_const
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
k : ℕ
hn : 0 < k.succ
simp :
  (∏ x ∈ Finset.range k, (HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹) *
      (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹ ≤
    (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹
⊢ (∏ k_1 ∈ Finset.range k, (↑(k_1 + 1 + 1) : ℝ) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹) *
      ((↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹) ≤
    (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹

Tactic:
simp only [one_mul, Nat.cast_add, zero_add, Nat.cast_one]

Premises used: zero_add, Nat.cast_add, Nat.cast_one, one_mul
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
k : ℕ
hn : 0 < k.succ
⊢ (∏ x ∈ Finset.range k, (HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹) *
      (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹ ≤
    (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹

Tactic:
mul_le_of_le_one_left (inv_nonneg.mpr <| mod_cast hn.le) (prod_le_one ?_ ?_)

Premises used: Iff.mpr, congrArg, Nat.cast_add._simp_1, cast, Finset.prod_le_one, LT.lt.le, Nat.cast_le._simp_1, LE.le, Nat.cast, mul_le_of_le_one_left, inv_nonneg, HAdd.hAdd, congr, Nat.cast_zero, OfNat.ofNat, Eq.symm, Nat.cast_one, Eq.trans
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
k : ℕ
hn : 0 < k.succ
refine_1 : ∀ i ∈ Finset.range k, 0 ≤ (HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹
refine_2 : ∀ i ∈ Finset.range k, (HAdd.hAdd (α := ℝ) (↑i : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹ ≤ 1
⊢ (∏ x ∈ Finset.range k, (HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹) *
      (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹ ≤
    (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹

Tactic:
refine
            mul_le_of_le_one_left (inv_nonneg.mpr <| mod_cast hn.le) (prod_le_one ?_ ?_)

Premises used: Iff.mpr, Finset.prod_le_one, mul_le_of_le_one_left, inv_nonneg
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x ∈ Finset.range k
⊢ x < k

Tactic:
rw [Finset.mem_range] at hx

Premises used: Finset.mem_range
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ 0 ≤ (HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ (HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹ ≤ 1

Tactic:
(div_le_one <| mod_cast hn).mpr ?_

Premises used: Iff.mpr, DivInvMonoid.div', div_le_one
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
refine_2 : HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 + 1 ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1
⊢ (HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 + 1) * (HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)⁻¹ ≤ 1

Tactic:
refine (div_le_one <| mod_cast hn).mpr ?_

Premises used: Iff.mpr, div_le_one
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
refine_2 : x + 1 + 1 ≤ k + 1
⊢ HAdd.hAdd (α := ℝ) (↑x : ℝ) 1 + 1 ≤ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1

Tactic:
norm_cast
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
k : ℕ
hn : 0 < k.succ
x : ℕ
hx : x < k
⊢ x + 1 + 1 ≤ k + 1

Tactic:
lia
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_4
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorSemiring α
x : ℕ
⊢ x ≤ ⌊max 0 (HAdd.hAdd (α := α) (↑x : α) 1)⌋₊

Tactic:
simp [Nat.le_floor_iff]

Premises used: Nat.le_floor_iff
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_4
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorSemiring α
⊢ Tendsto (β := ℕ) (fun (x : α) ↦ ⌈x⌉₊) atTop atTop

Tactic:
Nat.ceil_mono.tendsto_atTop_atTop (fun x ↦ ⟨x, ?_⟩)

Premises used: Nat.ceil_mono, Nat.cast, Exists.intro, Monotone.tendsto_atTop_atTop
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_4
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorSemiring α
refine : ∀ (x : ℕ), x ≤ ceil.{u_4} (α := α) (↑x : α)
⊢ Tendsto (β := ℕ) (fun (x : α) ↦ ⌈x⌉₊) atTop atTop

Tactic:
refine Nat.ceil_mono.tendsto_atTop_atTop (fun x ↦ ⟨x, ?_⟩)

Premises used: Nat.ceil_mono, Exists.intro, Monotone.tendsto_atTop_atTop
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_4
inst : Semiring α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorSemiring α
x : ℕ
⊢ x ≤ ceil.{u_4} (α := α) (↑x : α)

Tactic:
simp only [Nat.ceil_natCast, le_refl]

Premises used: le_refl, Nat.ceil_natCast
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
α : Type u_4
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : FloorSemiring α
inst_4 : Archimedean α
a : α
ha : 0 < a
⊢ Tendsto (β := ℕ) (fun (x : ℕ) ↦ ⌊a * (↑x : α)⌋₊) atTop atTop

Tactic:
Tendsto.comp tendsto_nat_floor_atTop
    <| Tendsto.const_mul_atTop ha tendsto_natCast_atTop_atTop

Premises used: Filter.Tendsto.const_mul_atTop, tendsto_nat_floor_atTop, tendsto_natCast_atTop_atTop, Nat.floor, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
⊢ Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 (a - 0))

Tactic:
have A : Tendsto (fun x : R ↦ a - x⁻¹) atTop (𝓝 (a - 0)) :=
    tendsto_const_nhds.sub tendsto_inv_atTop_zero
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 (a - 0))
⊢ Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 a)

Tactic:
rw [sub_zero] at A

Premises used: sub_zero
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 a)
hgf : ∀ᶠ (b : R) in atTop, a - b⁻¹ ≤ (↑⌊a * b⌋₊ : R) / b
hfh : ∀ᶠ (b : R) in atTop, (↑⌊a * b⌋₊ : R) / b ≤ a
⊢ Tendsto (fun (x : R) ↦ (↑⌊a * x⌋₊ : R) / x) atTop (𝓝 a)

Tactic:
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' A tendsto_const_nhds

Premises used: tendsto_const_nhds, tendsto_of_tendsto_of_tendsto_of_le_of_le'
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, a - b⁻¹ ≤ (↑⌊a * b⌋₊ : R) / b

Tactic:
eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩

Premises used: Iff.mpr, Exists.intro, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 a)
hgf : ∀ (x : R) (hx : x ≥ 1), a - x⁻¹ ≤ (↑⌊a * x⌋₊ : R) / x
⊢ ∀ᶠ (b : R) in atTop, a - b⁻¹ ≤ (↑⌊a * b⌋₊ : R) / b

Tactic:
refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩

Premises used: Iff.mpr, Exists.intro, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
hgf : a * x - 1 ≤ (↑⌊a * x⌋₊ : R)
⊢ a - x⁻¹ ≤ (↑⌊a * x⌋₊ : R) / x

Tactic:
simp only [le_div_iff₀ (zero_lt_one.trans_le hx), _root_.sub_mul,
      inv_mul_cancel₀ (zero_lt_one.trans_le hx).ne']

Premises used: LT.lt.ne', sub_mul, zero_lt_one, LT.lt.trans_le, le_div_iff₀, inv_mul_cancel₀
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
⊢ a * x < HAdd.hAdd (α := R) (↑⌊a * x⌋₊ : R) 1

Tactic:
have := Nat.lt_floor_add_one (a * x)
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
this : a * x < HAdd.hAdd (α := R) (↑⌊a * x⌋₊ : R) 1
linarith :
  (↑⌊a * x⌋₊ : R) < a * x - 1 → a * x - HAdd.hAdd (α := R) (↑⌊a * x⌋₊ : R) 1 + ((↑⌊a * x⌋₊ : R) - (a * x - 1)) = 0
⊢ a * x - 1 ≤ (↑⌊a * x⌋₊ : R)

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 a)
⊢ ∀ᶠ (b : R) in atTop, (↑⌊a * b⌋₊ : R) / b ≤ a

Tactic:
eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩

Premises used: Iff.mpr, Exists.intro, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 a)
hfh : ∀ (x : R) (hx : x ≥ 1), (↑⌊a * x⌋₊ : R) / x ≤ a
⊢ ∀ᶠ (b : R) in atTop, (↑⌊a * b⌋₊ : R) / b ≤ a

Tactic:
refine eventually_atTop.2 ⟨1, fun x hx ↦ ?_⟩

Premises used: Iff.mpr, Exists.intro, Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
hfh : (↑⌊a * x⌋₊ : R) ≤ a * x
⊢ (↑⌊a * x⌋₊ : R) / x ≤ a

Tactic:
rw [div_le_iff₀ (zero_lt_one.trans_le hx)]

Premises used: div_le_iff₀, zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a - x⁻¹) atTop (𝓝 a)
x : R
hx : x ≥ 1
⊢ (↑⌊a * x⌋₊ : R) ≤ a * x

Tactic:
simp [Nat.floor_le (mul_nonneg ha (zero_le_one.trans hx))]

Premises used: mul_nonneg, zero_le_one, Nat.floor_le, LE.le.trans
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
⊢ Tendsto (β := R) (fun (x : R) ↦ (↑⌊x⌋₊ : R) / x) atTop (𝓝 1)

Tactic:
simpa using tendsto_nat_floor_mul_div_atTop (zero_le_one' R)

Premises used: zero_le_one', tendsto_nat_floor_mul_div_atTop
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
⊢ Tendsto (fun (x : R) ↦ a + x⁻¹) atTop (𝓝 (a + 0))

Tactic:
have A : Tendsto (fun x : R ↦ a + x⁻¹) atTop (𝓝 (a + 0)) :=
    tendsto_const_nhds.add tendsto_inv_atTop_zero
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a + x⁻¹) atTop (𝓝 (a + 0))
⊢ Tendsto (fun (x : R) ↦ a + x⁻¹) atTop (𝓝 a)

Tactic:
rw [add_zero] at A

Premises used: add_zero
-- Module: Mathlib.Analysis.SpecificLimits.Basic
Goal:
R : Type u_4
inst : TopologicalSpace R
inst_1 : Field R
inst_2 : LinearOrder R
inst_3 : IsStrictOrderedRing R
inst_4 : OrderTopology R
inst_5 : FloorRing R
a : R
ha : 0 ≤ a
A : Tendsto (fun (x : R) ↦ a + x⁻¹) atTop (𝓝 a)
hgf : ∀ᶠ (b : R) in atTop, a ≤ (↑⌈a * b⌉₊ : R) / b
hfh : ∀ᶠ (b : R) in atTop, (↑⌈a * b⌉₊ : R) / b ≤ a + b⁻¹
⊢ Tendsto (fun (x : R) ↦ (↑⌈a * x⌉₊ : R) / x) atTop (𝓝 a)

Tactic:
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds A

Premises used: tendsto_const_nhds, tendsto_of_tendsto_of_tendsto_of_le_of_le'