awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
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 : ℝ)
ε : ℝ
εpos : 0 < ε
⊢ ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
have rcases : ∀ (c : ℕ → ℕ) (cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ))
  (ctop : Tendsto c atTop atTop) (clim : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)),
  ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
Tactic: rcases hlim (1 + ε) ((lt_add_iff_pos_right _).2 εpos) with ⟨c, cgrowth, ctop, clim⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (hypothesis)
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 : ℝ)
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
⊢ ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
have clim₁ : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / (↑(c x) : ℝ) - l‖ ≤ c_1 * norm (E := ℝ) 1
Tactic: rw [← tendsto_sub_nhds_zero_iff, ← Asymptotics.isLittleO_one_iff ℝ,
        Asymptotics.isLittleO_iff] at clim
Cleared hypotheses: clim
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
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 : ℝ)
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / (↑(c x) : ℝ) - l‖ ≤ c_1 * norm (E := ℝ) 1
⊢ ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
have h : ∀ (n : ℕ) (hn : ‖u (c n) / (↑(c n) : ℝ) - l‖ ≤ ε * norm (E := ℝ) 1) (cnpos' : n ∈ c ⁻¹' Set.Ioi 0),
  (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
Tactic: filter_upwards [clim εpos, ctop (Ioi_mem_atTop 0)] with n hn cnpos'
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (hypothesis)
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 : ℝ)
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / (↑(c x) : ℝ) - l‖ ≤ c_1 * norm (E := ℝ) 1
n : ℕ
hn : ‖u (c n) / (↑(c n) : ℝ) - l‖ ≤ ε * norm (E := ℝ) 1
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
⊢ (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
have cnpos : 0 < c n
Tactic: have cnpos : 0 < c n := cnpos'
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
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 : ℝ)
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / (↑(c x) : ℝ) - l‖ ≤ c_1 * norm (E := ℝ) 1
n : ℕ
hn : ‖u (c n) / (↑(c n) : ℝ) - l‖ ≤ ε * norm (E := ℝ) 1
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
cnpos : 0 < c n
⊢ -(u (c n) / (↑(c n) : ℝ) - l) * (↑(c n) : ℝ) ≤ ε * (↑(c n) : ℝ)
have hbc : -(u (c n) / (↑(c n) : ℝ) - l) ≤ ε
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
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 : ℝ)
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / (↑(c x) : ℝ) - l‖ ≤ c_1 * norm (E := ℝ) 1
n : ℕ
hn : ‖u (c n) / (↑(c n) : ℝ) - l‖ ≤ ε * norm (E := ℝ) 1
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
cnpos : 0 < c n
⊢ -(u (c n) / (↑(c n) : ℝ) - l) ≤ ε
have hbc : |u (c n) / (↑(c n) : ℝ) - l| ≤ ε
Tactic: refine le_trans (neg_le_abs _) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
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 : ℝ)
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / (↑(c x) : ℝ) - l‖ ≤ c_1 * norm (E := ℝ) 1
n : ℕ
hn : ‖u (c n) / (↑(c n) : ℝ) - l‖ ≤ ε * norm (E := ℝ) 1
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
cnpos : 0 < c n
⊢ (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
have n₁ : (↑(c n) : ℝ) * l - u (c n) = -(u (c n) / (↑(c n) : ℝ) - l) * (↑(c n) : ℝ)
Tactic: 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
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
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 : ℝ)
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : ∀ ⦃c_1 : ℝ⦄, 0 < c_1 → ∀ᶠ (x : ℕ) in atTop, ‖u (c x) / (↑(c x) : ℝ) - l‖ ≤ c_1 * norm (E := ℝ) 1
n : ℕ
hn : ‖u (c n) / (↑(c n) : ℝ) - l‖ ≤ ε * norm (E := ℝ) 1
cnpos' : n ∈ c ⁻¹' Set.Ioi 0
cnpos : 0 < c n
n₁ : (↑(c n) : ℝ) * l - u (c n) = -(u (c n) / (↑(c n) : ℝ) - l) * (↑(c n) : ℝ)
⊢ (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
have n₂ : -(u (c n) / (↑(c n) : ℝ) - l) * (↑(c n) : ℝ) ≤ ε * (↑(c n) : ℝ)
Tactic: 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
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (hypothesis)
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 : ℝ)
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
⊢ ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
have L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
Tactic: 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
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
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 : ℝ)
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
⊢ ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
have obtain : ∀ (a : ℕ)
  (ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(c b) : ℝ)),
  ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
Tactic: 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)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
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 : ℝ)
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
⊢ ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
have h : ∀ (n : ℕ) (hn : n ∈ Set.Ici M), (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
Tactic: filter_upwards [Ici_mem_atTop M] with n hn
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
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 : ℝ)
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
⊢ ∃ (N : ℕ), n < c N
have rcases : ∀ (N : ℕ) (hN : n + 1 ≤ c N), ∃ (N : ℕ), n < c N
Tactic: rcases (tendsto_atTop.1 ctop (n + 1)).exists with ⟨N, hN⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (hypothesis)
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 : ℝ)
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
⊢ (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
have exN : ∃ (N : ℕ), n < c N
Tactic: have exN : ∃ N, n < c N := by
      rcases (tendsto_atTop.1 ctop (n + 1)).exists with ⟨N, hN⟩
      exact ⟨N, by lia⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (hypothesis)
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 : ℝ)
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
⊢ (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
have ncN : n < c N
Tactic: have ncN : n < c N := Nat.find_spec exN
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
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 : ℝ)
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
ncN : n < c N
⊢ a + 1 ≤ N
have by_contra! : ∀ (h : N < a + 1), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
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 : ℝ)
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
ncN : n < c N
h : N < a + 1
⊢ c N ≤ M
have H2 : Membership.mem (γ := Finset ℕ) (image (fun (i : ℕ) ↦ c i) (range (a + 1))) (c N)
Tactic: apply le_max'
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
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 : ℝ)
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
ncN : n < c N
h : N < a + 1
⊢ Membership.mem (γ := Finset ℕ) (image (fun (i : ℕ) ↦ c i) (range (a + 1))) (c N)
have H2 : N ∈ range (a + 1)
Tactic: apply mem_image_of_mem
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (hypothesis)
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 : ℝ)
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
ncN : n < c N
h : N < a + 1
⊢ False
have cNM : c N ≤ M
Tactic: have cNM : c N ≤ M := by
        apply le_max'
        apply mem_image_of_mem
        exact mem_range.2 h
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (hypothesis)
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 : ℝ)
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
ncN : n < c N
⊢ (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
have aN : a + 1 ≤ N
Tactic: 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)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (hypothesis)
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 : ℝ)
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
ncN : n < c N
aN : a + 1 ≤ N
⊢ (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
have Npos : 0 < N
Tactic: have Npos : 0 < N := lt_of_lt_of_le Nat.succ_pos' aN
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (hypothesis)
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 : ℝ)
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
⊢ (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
have aN' : a ≤ N - 1
Tactic: have aN' : a ≤ N - 1 := (Nat.le_sub_one_iff_lt Npos).mpr aN
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (hypothesis)
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 : ℝ)
ε : ℝ
εpos : 0 < ε
c : ℕ → ℕ
cgrowth : ∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ (1 + ε) * (↑(c n) : ℝ)
ctop : Tendsto c atTop atTop
clim : Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)
L : ∀ᶠ (n : ℕ) in atTop, (↑(c n) : ℝ) * l - u (c n) ≤ ε * (↑(c n) : ℝ)
a : ℕ
ha : ∀ (b : ℕ), a ≤ b → (↑(c (b + 1)) : ℝ) ≤ (1 + ε) * (↑(c b) : ℝ) ∧ (↑(c b) : ℝ) * l - u (c b) ≤ ε * (↑(c b) : ℝ)
M : ℕ := max' (image (fun (i : ℕ) ↦ c i) (range (a + 1))) ⋯
n : ℕ
hn : n ∈ Set.Ici M
exN : ∃ (N : ℕ), n < c N
N : ℕ := Nat.find (p := fun (n_1 : ℕ) ↦ n < c n_1) exN
ncN : n < c N
aN : a + 1 ≤ N
Npos : 0 < N
aN' : a ≤ N - 1
⊢ c (N - 1) ≤ n
have this : N - 1 < N
Tactic: have : N - 1 < N := Nat.pred_lt Npos.ne'