awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
⊢ ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)

Tactic:
have B : ∀ ε : ℝ, 0 < ε → ∀ᶠ n : ℕ in atTop, (n : ℝ) * l - u n ≤ ε * (1 + l) * n := by
    intro ε εpos
    rcases hlim (1 + ε) ((lt_add_iff_pos_right _).2 εpos) with ⟨c, cgrowth, ctop, clim⟩
    have L : ∀ᶠ n : ℕ in atTop, (c n : ℝ) * l - u (c n) ≤ ε * c n := by
      rw [← tendsto_sub_nhds_zero_iff, ← Asymptotics.isLittleO_one_iff ℝ,
        Asymptotics.isLittleO_iff] at clim
      filter_upwards [clim εpos, ctop (Ioi_mem_atTop 0)] with n hn cnpos'
      have cnpos : 0 < c n := cnpos'
      calc
        (c n : ℝ) * l - u (c n) = -(u (c n) / c n - l) * c n := by field
        _ ≤ ε * c n := by
          gcongr
          refine le_trans (neg_le_abs _) ?_
          simpa using hn
    obtain ⟨a, ha⟩ :
      ∃ a : ℕ,
        ∀ b : ℕ, a ≤ b → (c (b + 1) : ℝ) ≤ (1 + ε) * c b ∧ (c b : ℝ) * l - u (c b) ≤ ε * c b :=
      eventually_atTop.1 (cgrowth.and L)
    let M := ((Finset.range (a + 1)).image fun i => c i).max' (by simp)
    filter_upwards [Ici_mem_atTop M] with n hn
    have exN : ∃ N, n < c N := by
      rcases (tendsto_atTop.1 ctop (n + 1)).exists with ⟨N, hN⟩
      exact ⟨N, by lia⟩
    let N := Nat.find exN
    have ncN : n < c N := Nat.find_spec exN
    have aN : a + 1 ≤ N := by
      by_contra! h
      have cNM : c N ≤ M := by
        apply le_max'
        apply mem_image_of_mem
        exact mem_range.2 h
      exact lt_irrefl _ ((cNM.trans hn).trans_lt ncN)
    have Npos : 0 < N := lt_of_lt_of_le Nat.succ_pos' aN
    have aN' : a ≤ N - 1 := (Nat.le_sub_one_iff_lt Npos).mpr aN
    have cNn : c (N - 1) ≤ n := by
      have : N - 1 < N := Nat.pred_lt Npos.ne'
      simpa only [not_lt] using Nat.find_min exN this
    calc
      (n : ℝ) * l - u n ≤ c N * l - u (c (N - 1)) := by
        gcongr
        exact hmono cNn
      _ ≤ (1 + ε) * c (N - 1) * l - u (c (N - 1)) := by
        gcongr
        have B : N - 1 + 1 = N := Nat.succ_pred_eq_of_pos Npos
        simpa [B] using (ha _ aN').1
      _ = c (N - 1) * l - u (c (N - 1)) + ε * c (N - 1) * l := by ring
      _ ≤ ε * c (N - 1) + ε * c (N - 1) * l := add_le_add (ha _ aN').2 le_rfl
      _ = ε * (1 + l) * c (N - 1) := by ring
      _ ≤ ε * (1 + l) * n := by gcongr
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
⊢ Tendsto (fun (n : ℕ) ↦ u n / (↑n : ℝ)) atTop (𝓝 l)

Tactic:
tendsto_order.2 ⟨fun d hd => ?_, fun d hd => ?_⟩

Premises used: Iff.mpr, tendsto_order, And.intro
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
refine_1 : ∀ (d : ℝ) (hd : d < l), ∀ᶠ (b : ℕ) in atTop, d < u b / (↑b : ℝ)
refine_2 : ∀ (d : ℝ) (hd : d > l), ∀ᶠ (b : ℕ) in atTop, u b / (↑b : ℝ) < d
⊢ Tendsto (fun (n : ℕ) ↦ u n / (↑n : ℝ)) atTop (𝓝 l)

Tactic:
refine tendsto_order.2 ⟨fun d hd => ?_, fun d hd => ?_⟩

Premises used: Iff.mpr, tendsto_order, And.intro
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d < l
apply : Tendsto (fun (ε : ℝ) ↦ d + ε * (1 + l)) (𝓝 0) (𝓝 (d + 0 * (1 + l)))
⊢ Tendsto (fun (ε : ℝ) ↦ d + ε * (1 + l)) (𝓝[>] 0) (𝓝 (d + 0 * (1 + l)))

Tactic:
apply Tendsto.mono_left _ nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds, Filter.Tendsto.mono_left
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d < l
⊢ Tendsto (fun (ε : ℝ) ↦ d + ε * (1 + l)) (𝓝 0) (𝓝 (d + 0 * (1 + l)))

Tactic:
tendsto_const_nhds.add (tendsto_id.mul tendsto_const_nhds)

Premises used: Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.mul, Filter.Tendsto.add
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d < l
⊢ Tendsto (fun (ε : ℝ) ↦ d + ε * (1 + l)) (𝓝 0) (𝓝 (d + 0 * (1 + l)))

Tactic:
exact tendsto_const_nhds.add (tendsto_id.mul tendsto_const_nhds)

Premises used: Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.mul, Filter.Tendsto.add
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d < l
⊢ Tendsto (fun (ε : ℝ) ↦ d + ε * (1 + l)) (𝓝[>] 0) (𝓝 (d + 0 * (1 + l)))

Tactic:
have L : Tendsto (fun ε => d + ε * (1 + l)) (𝓝[>] 0) (𝓝 (d + 0 * (1 + l))) := by
        apply Tendsto.mono_left _ nhdsWithin_le_nhds
        exact tendsto_const_nhds.add (tendsto_id.mul tendsto_const_nhds)
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d < l
L : Tendsto (fun (ε : ℝ) ↦ d + ε * (1 + l)) (𝓝[>] 0) (𝓝 (d + 0 * (1 + l)))
⊢ Tendsto (fun (ε : ℝ) ↦ d + ε * (1 + l)) (𝓝[>] 0) (𝓝 d)

Tactic:
simp only [zero_mul, add_zero] at L

Premises used: MulZeroClass.zero_mul, add_zero
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d < l
L : Tendsto (fun (ε : ℝ) ↦ d + ε * (1 + l)) (𝓝[>] 0) (𝓝 d)
⊢ ∃ (ε : ℝ), d + ε * (1 + l) < l ∧ 0 < ε

Tactic:
(((tendsto_order.1 L).2 l hd).and self_mem_nhdsWithin).exists

Premises used: tendsto_order, Filter.Eventually.and, Filter.Eventually.exists, And.right, self_mem_nhdsWithin, Iff.mp
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d < l
L : Tendsto (fun (ε : ℝ) ↦ d + ε * (1 + l)) (𝓝[>] 0) (𝓝 d)
⊢ ∃ (ε : ℝ), d + ε * (1 + l) < l ∧ 0 < ε

Tactic:
exact (((tendsto_order.1 L).2 l hd).and self_mem_nhdsWithin).exists

Premises used: tendsto_order, Filter.Eventually.and, Filter.Eventually.exists, And.right, self_mem_nhdsWithin, Iff.mp
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d < l
refine_1 : ∀ (ε : ℝ) (hε : d + ε * (1 + l) < l) (εpos : 0 < ε), ∀ᶠ (b : ℕ) in atTop, d < u b / (↑b : ℝ)
⊢ ∀ᶠ (b : ℕ) in atTop, d < u b / (↑b : ℝ)

Tactic:
obtain ⟨ε, hε, εpos⟩ : ∃ ε : ℝ, d + ε * (1 + l) < l ∧ 0 < ε := by
      have L : Tendsto (fun ε => d + ε * (1 + l)) (𝓝[>] 0) (𝓝 (d + 0 * (1 + l))) := by
        apply Tendsto.mono_left _ nhdsWithin_le_nhds
        exact tendsto_const_nhds.add (tendsto_id.mul tendsto_const_nhds)
      simp only [zero_mul, add_zero] at L
      exact (((tendsto_order.1 L).2 l hd).and self_mem_nhdsWithin).exists

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d < l
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
h :
  ∀ (n : ℕ) (hn : (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)) (npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n),
    d < u n / (↑n : ℝ)
⊢ ∀ᶠ (b : ℕ) in atTop, d < u b / (↑b : ℝ)

Tactic:
filter_upwards [B ε εpos, Ioi_mem_atTop 0] with n hn npos

Premises used: Filter.Ioi_mem_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d < l
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
h : d < (↑n : ℝ)⁻¹ * u n
⊢ d < u n / (↑n : ℝ)

Tactic:
simp_rw [div_eq_inv_mul]

Premises used: div_eq_inv_mul
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d < l
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
rw : d < l - ε * (1 + l)
rw₁ : Ne (α := ℝ) (↑n : ℝ) 0
⊢ d < HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) * (l - ε * (1 + l))

Tactic:
rw [inv_mul_cancel₀, one_mul]

Premises used: inv_mul_cancel₀, one_mul
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d < l
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
linarith : l - ε * (1 + l) ≤ d → l - ε * (1 + l) - d + (d + ε * (1 + l) - l) = 0
⊢ d < l - ε * (1 + l)

Tactic:
linarith only [hε]
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d < l
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
Nat.cast_ne_zero.2 (ne_of_gt npos)

Premises used: Iff.mpr, ne_of_gt, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d < l
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
exact Nat.cast_ne_zero.2 (ne_of_gt npos)

Premises used: Iff.mpr, ne_of_gt, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d < l
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
⊢ HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) * (l - ε * (1 + l)) = (↑n : ℝ)⁻¹ * ((↑n : ℝ) * l - ε * (1 + l) * (↑n : ℝ))

Tactic:
ring
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d < l
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
hbc : (↑n : ℝ) * l - ε * (1 + l) * (↑n : ℝ) ≤ u n
⊢ (↑n : ℝ)⁻¹ * ((↑n : ℝ) * l - ε * (1 + l) * (↑n : ℝ)) ≤ (↑n : ℝ)⁻¹ * u n

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d < l
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
linarith :
  u n < (↑n : ℝ) * l - ε * (1 + l) * (↑n : ℝ) →
    u n - ((↑n : ℝ) * l - ε * (1 + l) * (↑n : ℝ)) + ((↑n : ℝ) * l - u n - ε * (1 + l) * (↑n : ℝ)) = 0
⊢ (↑n : ℝ) * l - ε * (1 + l) * (↑n : ℝ) ≤ u n

Tactic:
linarith only [hn]
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d < l
ε : ℝ
hε : d + ε * (1 + l) < l
εpos : 0 < ε
n : ℕ
hn : (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
npos : Membership.mem (γ := Set ℕ) (Set.Ioi 0) n
d₁ : d < HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) * (l - ε * (1 + l))
d₂ : HMul.hMul (α := ℝ) (↑n : ℝ)⁻¹ (↑n : ℝ) * (l - ε * (1 + l)) = (↑n : ℝ)⁻¹ * ((↑n : ℝ) * l - ε * (1 + l) * (↑n : ℝ))
d₃ : (↑n : ℝ)⁻¹ * ((↑n : ℝ) * l - ε * (1 + l) * (↑n : ℝ)) ≤ (↑n : ℝ)⁻¹ * u n
⊢ d < (↑n : ℝ)⁻¹ * u n

Tactic:
calc
      d < (n : ℝ)⁻¹ * n * (l - ε * (1 + l)) := by
        rw [inv_mul_cancel₀, one_mul]
        · linarith only [hε]
        · exact Nat.cast_ne_zero.2 (ne_of_gt npos)
      _ = (n : ℝ)⁻¹ * (n * l - ε * (1 + l) * n) := by ring
      _ ≤ (n : ℝ)⁻¹ * u n := by gcongr; linarith only [hn]

Premises used: HMul.hMul, HSub.hSub, Nat.cast, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d > l
apply : Tendsto (fun (ε : ℝ) ↦ l + ε * (1 + ε + l)) (𝓝 0) (𝓝 (l + 0 * (HAdd.hAdd (α := ℝ) 1 0 + l)))
⊢ Tendsto (fun (ε : ℝ) ↦ l + ε * (1 + ε + l)) (𝓝[>] 0) (𝓝 (l + 0 * (HAdd.hAdd (α := ℝ) 1 0 + l)))

Tactic:
apply Tendsto.mono_left _ nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds, Filter.Tendsto.mono_left
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d > l
⊢ Tendsto (fun (ε : ℝ) ↦ l + ε * (1 + ε + l)) (𝓝 0) (𝓝 (l + 0 * (HAdd.hAdd (α := ℝ) 1 0 + l)))

Tactic:
tendsto_const_nhds.add
            (tendsto_id.mul ((tendsto_const_nhds.add tendsto_id).add tendsto_const_nhds))

Premises used: Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.mul, Filter.Tendsto.add
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d > l
⊢ Tendsto (fun (ε : ℝ) ↦ l + ε * (1 + ε + l)) (𝓝 0) (𝓝 (l + 0 * (HAdd.hAdd (α := ℝ) 1 0 + l)))

Tactic:
exact
          tendsto_const_nhds.add
            (tendsto_id.mul ((tendsto_const_nhds.add tendsto_id).add tendsto_const_nhds))

Premises used: Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.mul, Filter.Tendsto.add
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d > l
⊢ Tendsto (fun (ε : ℝ) ↦ l + ε * (1 + ε + l)) (𝓝[>] 0) (𝓝 (l + 0 * (HAdd.hAdd (α := ℝ) 1 0 + l)))

Tactic:
have L : Tendsto (fun ε => l + ε * (1 + ε + l)) (𝓝[>] 0) (𝓝 (l + 0 * (1 + 0 + l))) := by
        apply Tendsto.mono_left _ nhdsWithin_le_nhds
        exact
          tendsto_const_nhds.add
            (tendsto_id.mul ((tendsto_const_nhds.add tendsto_id).add tendsto_const_nhds))
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
hlim :
  ∀ (a : ℝ),
    1 < a →
      ∃ (c : ℕ → ℕ),
        (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
          Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
lnonneg : 0 ≤ l
A : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d > l
L : Tendsto (fun (ε : ℝ) ↦ l + ε * (1 + ε + l)) (𝓝[>] 0) (𝓝 (l + 0 * (HAdd.hAdd (α := ℝ) 1 0 + l)))
⊢ Tendsto (fun (ε : ℝ) ↦ l + ε * (1 + ε + l)) (𝓝[>] 0) (𝓝 l)

Tactic:
simp only [zero_mul, add_zero] at L

Premises used: MulZeroClass.zero_mul, add_zero