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 : ℝ)
B : ∀ (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in atTop, (↑n : ℝ) * l - u n ≤ ε * (1 + l) * (↑n : ℝ)
d : ℝ
hd : d > l
L : Tendsto (fun (ε : ℝ) ↦ l + ε * (1 + ε + l)) (𝓝[>] 0) (𝓝 l)
⊢ ∃ (ε : ℝ), l + ε * (1 + ε + l) < d ∧ 0 < ε

Tactic:
(((tendsto_order.1 L).2 d 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 (ε : ℝ) ↦ l + ε * (1 + ε + l)) (𝓝[>] 0) (𝓝 l)
⊢ ∃ (ε : ℝ), l + ε * (1 + ε + l) < d ∧ 0 < ε

Tactic:
exact (((tendsto_order.1 L).2 d 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_2 : ∀ (ε : ℝ) (hε : l + ε * (1 + ε + l) < d) (εpos : 0 < ε), ∀ᶠ (b : ℕ) in atTop, u b / (↑b : ℝ) < d
⊢ ∀ᶠ (b : ℕ) in atTop, u b / (↑b : ℝ) < d

Tactic:
obtain ⟨ε, hε, εpos⟩ : ∃ ε : ℝ, l + ε * (1 + ε + l) < d ∧ 0 < ε := by
      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))
      simp only [zero_mul, add_zero] at L
      exact (((tendsto_order.1 L).2 d hd).and self_mem_nhdsWithin).exists
-- 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ε : l + ε * (1 + ε + l) < d
εpos : 0 < ε
n : ℕ
hn : u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
h : ∀ (npos : 0 < n), u n / (↑n : ℝ) < d
⊢ Membership.mem (γ := Set ℕ) (Set.Ioi 0) n → u n / (↑n : ℝ) < d

Tactic:
(npos : 0 < n)
-- 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ε : l + ε * (1 + ε + l) < d
εpos : 0 < ε
h : ∀ (n : ℕ) (hn : u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)) (npos : 0 < n), u n / (↑n : ℝ) < d
⊢ ∀ᶠ (b : ℕ) in atTop, u b / (↑b : ℝ) < d

Tactic:
filter_upwards [A ε εpos, Ioi_mem_atTop 0] with n hn (npos : 0 < n)

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ε : l + ε * (1 + ε + l) < d
εpos : 0 < ε
n : ℕ
hn : u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
npos : 0 < n
hab : u n ≤ (↑n : ℝ) * l + ε * (1 + ε + l) * (↑n : ℝ)
⊢ u n / (↑n : ℝ) ≤ ((↑n : ℝ) * l + ε * (1 + ε + l) * (↑n : ℝ)) / (↑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ε : l + ε * (1 + ε + l) < d
εpos : 0 < ε
n : ℕ
hn : u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
npos : 0 < n
linarith :
  (↑n : ℝ) * l + ε * (1 + ε + l) * (↑n : ℝ) < u n →
    (↑n : ℝ) * l + ε * (1 + ε + l) * (↑n : ℝ) - u n + (u n - (↑n : ℝ) * l - ε * (1 + ε + l) * (↑n : ℝ)) = 0
⊢ u n ≤ (↑n : ℝ) * l + ε * (1 + ε + l) * (↑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ε : l + ε * (1 + ε + l) < d
εpos : 0 < ε
n : ℕ
hn : u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
npos : 0 < n
⊢ ((↑n : ℝ) * l + ε * (1 + ε + l) * (↑n : ℝ)) / (↑n : ℝ) = l + ε * (1 + ε + l)

Tactic:
field
-- 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ε : l + ε * (1 + ε + l) < d
εpos : 0 < ε
n : ℕ
hn : u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
npos : 0 < n
⊢ l + ε * (1 + ε + l) < d

Tactic:
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ε : l + ε * (1 + ε + l) < d
εpos : 0 < ε
n : ℕ
hn : u n - (↑n : ℝ) * l ≤ ε * (1 + ε + l) * (↑n : ℝ)
npos : 0 < n
u₁ : u n / (↑n : ℝ) ≤ ((↑n : ℝ) * l + ε * (1 + ε + l) * (↑n : ℝ)) / (↑n : ℝ)
u₂ : ((↑n : ℝ) * l + ε * (1 + ε + l) * (↑n : ℝ)) / (↑n : ℝ) = l + ε * (1 + ε + l)
⊢ u n / (↑n : ℝ) < d

Tactic:
calc
      u n / n ≤ (n * l + ε * (1 + ε + l) * n) / n := by gcongr; linarith only [hn]
      _ = (l + ε * (1 + ε + l)) := by field
      _ < d := hε

Premises used: HMul.hMul, Nat.cast, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
apply :
  ∀ (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)
⊢ Tendsto (fun (n : ℕ) ↦ u n / (↑n : ℝ)) atTop (𝓝 l)

Tactic:
apply tendsto_div_of_monotone_of_exists_subseq_tendsto_div u l hmono

Premises used: tendsto_div_of_monotone_of_exists_subseq_tendsto_div
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
⊢ ∃ (k : ℕ), c k < a

Tactic:
((tendsto_order.1 clim).2 a ha).exists

Premises used: tendsto_order, Filter.Eventually.exists, And.right, Iff.mp
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
obtain :
  ∀ (k : ℕ) (hk : c k < 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)
⊢ ∃ (c : ℕ → ℕ),
    (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
      Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)

Tactic:
obtain ⟨k, hk⟩ : ∃ k, c k < a := ((tendsto_order.1 clim).2 a ha).exists

Premises used: tendsto_order, Filter.Eventually.exists, And.right, Iff.mp
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < 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)

Tactic:
⟨fun n => ⌊c k ^ n⌋₊, ?_,
      (tendsto_nat_floor_atTop (α := ℝ)).comp (tendsto_pow_atTop_atTop_of_one_lt (cone k)), hc k⟩

Premises used: tendsto_nat_floor_atTop, tendsto_pow_atTop_atTop_of_one_lt, HPow.hPow, And.intro, Exists.intro, Nat.floor, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
n : ∀ᶠ (n : ℕ) in atTop, (↑((fun (n : ℕ) ↦ ⌊c k ^ n⌋₊) (n + 1)) : ℝ) ≤ a * (↑((fun (n : ℕ) ↦ ⌊c k ^ n⌋₊) n) : ℝ)
⊢ ∃ (c : ℕ → ℕ),
    (∀ᶠ (n : ℕ) in atTop, (↑(c (n + 1)) : ℝ) ≤ a * (↑(c n) : ℝ)) ∧
      Tendsto c atTop atTop ∧ Tendsto (fun (n : ℕ) ↦ u (c n) / (↑(c n) : ℝ)) atTop (𝓝 l)

Tactic:
refine
    ⟨fun n => ⌊c k ^ n⌋₊, ?_,
      (tendsto_nat_floor_atTop (α := ℝ)).comp (tendsto_pow_atTop_atTop_of_one_lt (cone k)), hc k⟩
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
n : ℕ
⊢ LT.lt (α := ℝ) 0 (↑⌊c k ^ n⌋₊ : ℝ)

Tactic:
zero_lt_one.trans_le ?_

Premises used: zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
n : ℕ
refine : LE.le (α := ℝ) 1 (↑⌊c k ^ n⌋₊ : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑⌊c k ^ n⌋₊ : ℝ)

Tactic:
refine zero_lt_one.trans_le ?_

Premises used: zero_lt_one, LT.lt.trans_le
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
n : ℕ
⊢ LE.le (α := ℝ) 1 (↑⌊c k ^ n⌋₊ : ℝ)

Tactic:
simp only [Nat.one_le_cast, Nat.one_le_floor_iff, one_le_pow₀ (cone k).le]

Premises used: Nat.one_le_cast, Nat.one_le_floor_iff, one_le_pow₀, LT.lt.le
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
⊢ ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c k ^ n⌋₊ : ℝ)

Tactic:
have H : ∀ n : ℕ, (0 : ℝ) < ⌊c k ^ n⌋₊ := by
    intro n
    refine zero_lt_one.trans_le ?_
    simp only [Nat.one_le_cast, Nat.one_le_floor_iff, one_le_pow₀ (cone k).le]
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c k ^ n⌋₊ : ℝ)
⊢ Tendsto (fun (n : ℕ) ↦ (↑⌊c k ^ (n + 1)⌋₊ : ℝ) / c k ^ (n + 1) * c k / ((↑⌊c k ^ n⌋₊ : ℝ) / c k ^ n)) atTop
    (𝓝 (1 * c k / 1))

Tactic:
Tendsto.div (Tendsto.mul ?_ tendsto_const_nhds) ?_ one_ne_zero

Premises used: tendsto_const_nhds, Filter.Tendsto.div, Filter.Tendsto.mul, one_ne_zero
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c k ^ n⌋₊ : ℝ)
refine_1 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑⌊c k ^ (n + 1)⌋₊ : ℝ) / c k ^ (n + 1)) atTop (𝓝 1)
refine_2 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑⌊c k ^ n⌋₊ : ℝ) / c k ^ n) atTop (𝓝 1)
⊢ Tendsto (fun (n : ℕ) ↦ (↑⌊c k ^ (n + 1)⌋₊ : ℝ) / c k ^ (n + 1) * c k / ((↑⌊c k ^ n⌋₊ : ℝ) / c k ^ n)) atTop
    (𝓝 (1 * c k / 1))

Tactic:
refine Tendsto.div (Tendsto.mul ?_ tendsto_const_nhds) ?_ one_ne_zero

Premises used: tendsto_const_nhds, Filter.Tendsto.div, Filter.Tendsto.mul, one_ne_zero
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c k ^ n⌋₊ : ℝ)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑⌊c k ^ (n + 1)⌋₊ : ℝ) / c k ^ (n + 1)) atTop (𝓝 1)

Tactic:
tendsto_nat_floor_div_atTop.comp ?_

Premises used: tendsto_nat_floor_div_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c k ^ n⌋₊ : ℝ)
refine_1 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ c k ^ (n + 1)) atTop atTop
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑⌊c k ^ (n + 1)⌋₊ : ℝ) / c k ^ (n + 1)) atTop (𝓝 1)

Tactic:
refine tendsto_nat_floor_div_atTop.comp ?_

Premises used: tendsto_nat_floor_div_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c k ^ n⌋₊ : ℝ)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ c k ^ (n + 1)) atTop atTop

Tactic:
(tendsto_pow_atTop_atTop_of_one_lt (cone k)).comp (tendsto_add_atTop_nat 1)

Premises used: tendsto_pow_atTop_atTop_of_one_lt, Filter.tendsto_add_atTop_nat, Filter.Tendsto.comp, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c k ^ n⌋₊ : ℝ)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ c k ^ (n + 1)) atTop atTop

Tactic:
exact (tendsto_pow_atTop_atTop_of_one_lt (cone k)).comp (tendsto_add_atTop_nat 1)

Premises used: tendsto_pow_atTop_atTop_of_one_lt, Filter.tendsto_add_atTop_nat, Filter.Tendsto.comp, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c k ^ n⌋₊ : ℝ)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑⌊c k ^ n⌋₊ : ℝ) / c k ^ n) atTop (𝓝 1)

Tactic:
tendsto_nat_floor_div_atTop.comp ?_

Premises used: tendsto_nat_floor_div_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c k ^ n⌋₊ : ℝ)
refine_2 : Tendsto (α := ℕ) (HPow.hPow (c k)) atTop atTop
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑⌊c k ^ n⌋₊ : ℝ) / c k ^ n) atTop (𝓝 1)

Tactic:
refine tendsto_nat_floor_div_atTop.comp ?_

Premises used: tendsto_nat_floor_div_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c k ^ n⌋₊ : ℝ)
⊢ Tendsto (α := ℕ) (HPow.hPow (c k)) atTop atTop

Tactic:
tendsto_pow_atTop_atTop_of_one_lt (cone k)

Premises used: tendsto_pow_atTop_atTop_of_one_lt
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c k ^ n⌋₊ : ℝ)
⊢ Tendsto (α := ℕ) (HPow.hPow (c k)) atTop atTop

Tactic:
exact tendsto_pow_atTop_atTop_of_one_lt (cone k)

Premises used: tendsto_pow_atTop_atTop_of_one_lt
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c k ^ n⌋₊ : ℝ)
A :
  Tendsto (fun (n : ℕ) ↦ (↑⌊c k ^ (n + 1)⌋₊ : ℝ) / c k ^ (n + 1) * c k / ((↑⌊c k ^ n⌋₊ : ℝ) / c k ^ n)) atTop
    (𝓝 (1 * c k / 1))
⊢ Tendsto (fun (n : ℕ) ↦ (↑⌊c k ^ (n + 1)⌋₊ : ℝ) / c k ^ (n + 1) * c k / ((↑⌊c k ^ n⌋₊ : ℝ) / c k ^ n)) atTop (𝓝 (c k))

Tactic:
simp only [one_mul, div_one] at A

Premises used: div_one, one_mul
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c k ^ n⌋₊ : ℝ)
A :
  Tendsto (fun (n : ℕ) ↦ (↑⌊c k ^ (n + 1)⌋₊ : ℝ) / c k ^ (n + 1) * c k / ((↑⌊c k ^ n⌋₊ : ℝ) / c k ^ n)) atTop (𝓝 (c k))
⊢ Tendsto (fun (n : ℕ) ↦ (↑⌊c k ^ (n + 1)⌋₊ : ℝ) / c k ^ (n + 1) * c k / ((↑⌊c k ^ n⌋₊ : ℝ) / c k ^ n)) atTop (𝓝 (c k))

Tactic:
A
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c k ^ n⌋₊ : ℝ)
A :
  Tendsto (fun (n : ℕ) ↦ (↑⌊c k ^ (n + 1)⌋₊ : ℝ) / c k ^ (n + 1) * c k / ((↑⌊c k ^ n⌋₊ : ℝ) / c k ^ n)) atTop (𝓝 (c k))
h :
  Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑⌊c k ^ (n + 1)⌋₊ : ℝ) (↑⌊c k ^ n⌋₊ : ℝ)) fun (n : ℕ) ↦
    (↑⌊c k ^ (n + 1)⌋₊ : ℝ) / c k ^ (n + 1) * c k / ((↑⌊c k ^ n⌋₊ : ℝ) / c k ^ n)
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑⌊c k ^ (n + 1)⌋₊ : ℝ) (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 (c k))

Tactic:
convert! A using 1
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c k ^ n⌋₊ : ℝ)
A :
  Tendsto (fun (n : ℕ) ↦ (↑⌊c k ^ (n + 1)⌋₊ : ℝ) / c k ^ (n + 1) * c k / ((↑⌊c k ^ n⌋₊ : ℝ) / c k ^ n)) atTop (𝓝 (c k))
h :
  ∀ (n : ℕ),
    HDiv.hDiv (α := ℝ) (↑⌊c k ^ (n + 1)⌋₊ : ℝ) (↑⌊c k ^ n⌋₊ : ℝ) =
      (↑⌊c k ^ (n + 1)⌋₊ : ℝ) / c k ^ (n + 1) * c k / ((↑⌊c k ^ n⌋₊ : ℝ) / c k ^ n)
⊢ Eq (α := ℕ → ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑⌊c k ^ (n + 1)⌋₊ : ℝ) (↑⌊c k ^ n⌋₊ : ℝ)) fun (n : ℕ) ↦
    (↑⌊c k ^ (n + 1)⌋₊ : ℝ) / c k ^ (n + 1) * c k / ((↑⌊c k ^ n⌋₊ : ℝ) / c k ^ n)

Tactic:
ext1 n
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c k ^ n⌋₊ : ℝ)
A :
  Tendsto (fun (n : ℕ) ↦ (↑⌊c k ^ (n + 1)⌋₊ : ℝ) / c k ^ (n + 1) * c k / ((↑⌊c k ^ n⌋₊ : ℝ) / c k ^ n)) atTop (𝓝 (c k))
n : ℕ
⊢ HDiv.hDiv (α := ℝ) (↑⌊c k ^ (n + 1)⌋₊ : ℝ) (↑⌊c k ^ n⌋₊ : ℝ) =
    (↑⌊c k ^ (n + 1)⌋₊ : ℝ) / c k ^ (n + 1) * c k / ((↑⌊c k ^ n⌋₊ : ℝ) / c k ^ n)

Tactic:
field [(zero_lt_one.trans (cone k)).ne']

Premises used: LT.lt.ne', zero_lt_one, LT.lt.trans
-- Module: Mathlib.Analysis.SpecificLimits.FloorPow
Goal:
u : ℕ → ℝ
l : ℝ
hmono : Monotone u
c : ℕ → ℝ
cone : ∀ (k : ℕ), 1 < c k
clim : Tendsto c atTop (𝓝 1)
hc : ∀ (k : ℕ), Tendsto (fun (n : ℕ) ↦ u ⌊c k ^ n⌋₊ / (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 l)
a : ℝ
ha : 1 < a
k : ℕ
hk : c k < a
H : ∀ (n : ℕ), LT.lt (α := ℝ) 0 (↑⌊c k ^ n⌋₊ : ℝ)
A :
  Tendsto (fun (n : ℕ) ↦ (↑⌊c k ^ (n + 1)⌋₊ : ℝ) / c k ^ (n + 1) * c k / ((↑⌊c k ^ n⌋₊ : ℝ) / c k ^ n)) atTop
    (𝓝 (1 * c k / 1))
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑⌊c k ^ (n + 1)⌋₊ : ℝ) (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 (c k))

Tactic:
have B : Tendsto (fun n : ℕ => (⌊c k ^ (n + 1)⌋₊ : ℝ) / ⌊c k ^ n⌋₊) atTop (𝓝 (c k)) := by
    simp only [one_mul, div_one] at A
    convert! A using 1
    ext1 n
    field [(zero_lt_one.trans (cone k)).ne']