awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
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 : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑⌊c k ^ (n + 1)⌋₊ : ℝ) (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 (c k))
have 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)
Tactic: convert! A using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
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))
⊢ 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)
have 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)
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (hypothesis)
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))
⊢ ∀ᶠ (n : ℕ) in atTop, (↑((fun (n : ℕ) ↦ ⌊c k ^ n⌋₊) (n + 1)) : ℝ) ≤ a * (↑((fun (n : ℕ) ↦ ⌊c k ^ n⌋₊) n) : ℝ)
have B : 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']
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
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))
B : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (↑⌊c k ^ (n + 1)⌋₊ : ℝ) (↑⌊c k ^ n⌋₊ : ℝ)) atTop (𝓝 (c k))
⊢ ∀ᶠ (n : ℕ) in atTop, (↑((fun (n : ℕ) ↦ ⌊c k ^ n⌋₊) (n + 1)) : ℝ) ≤ a * (↑((fun (n : ℕ) ↦ ⌊c k ^ n⌋₊) n) : ℝ)
have h : ∀ (n : ℕ) (hn : HDiv.hDiv (α := ℝ) (↑⌊c k ^ (n + 1)⌋₊ : ℝ) (↑⌊c k ^ n⌋₊ : ℝ) < a),
  (↑⌊c k ^ (n + 1)⌋₊ : ℝ) ≤ a * (↑⌊c k ^ n⌋₊ : ℝ)
Tactic: filter_upwards [(tendsto_order.1 B).2 a hk] with n hn
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (hypothesis)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
⊢ ∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (β := ℕ) (c ^ i) 2 ≤
    HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹ / HPow.hPow (β := ℕ) j 2
have cpos : 0 < c
Tactic: have cpos : 0 < c := zero_lt_one.trans hc
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (hypothesis)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
⊢ ∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (β := ℕ) (c ^ i) 2 ≤
    HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹ / HPow.hPow (β := ℕ) j 2
have A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
Tactic: have A : (0 : ℝ) < c⁻¹ ^ 2 := sq_pos_of_pos (inv_pos.2 cpos)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
⊢ HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
have rw : HPow.hPow (β := ℕ) c 2 * (c - 1) ≤ HPow.hPow (β := ℕ) c 3 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)
Tactic: rw [← div_eq_mul_inv, ← div_eq_mul_inv, div_le_div_iff₀ _ (sub_pos.2 hc)]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
rw : HPow.hPow (β := ℕ) c 2 * (c - 1) ≤ HPow.hPow (β := ℕ) c 3 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)
⊢ HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
have rw₁ : 0 < 1 - HPow.hPow (β := ℕ) c⁻¹ 2
Tactic: rw [← div_eq_mul_inv, ← div_eq_mul_inv, div_le_div_iff₀ _ (sub_pos.2 hc)]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (hypothesis)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
⊢ HPow.hPow (β := ℕ) c 2 * (c - 1) ≤ HPow.hPow (β := ℕ) c 3 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)
have this : HPow.hPow (β := ℕ) c 3 = HPow.hPow (β := ℕ) c 2 * c
Tactic: have : c ^ 3 = c ^ 2 * c := by ring
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
this : HPow.hPow (β := ℕ) c 3 = HPow.hPow (β := ℕ) c 2 * c
⊢ HPow.hPow (β := ℕ) c 2 * (c - 1) ≤ HPow.hPow (β := ℕ) c 3 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)
have simp : HPow.hPow (β := ℕ) c 2 * c * (HPow.hPow (β := ℕ) c 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 2
Tactic: simp only [mul_sub, this, mul_one, inv_pow, sub_le_sub_iff_left]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
this : HPow.hPow (β := ℕ) c 3 = HPow.hPow (β := ℕ) c 2 * c
⊢ HPow.hPow (β := ℕ) c 2 * c * (HPow.hPow (β := ℕ) c 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 2
have rw : c ≤ HPow.hPow (β := ℕ) c 2
Tactic: rw [mul_assoc, mul_comm c, ← mul_assoc, mul_inv_cancel₀ (sq_pos_of_pos cpos).ne', one_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (hypothesis)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
⊢ ∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (β := ℕ) (c ^ i) 2 ≤
    HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹ / HPow.hPow (β := ℕ) j 2
have B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
Tactic: have B : c ^ 2 * ((1 : ℝ) - c⁻¹ ^ 2)⁻¹ ≤ c ^ 3 * (c - 1)⁻¹ := by
    rw [← div_eq_mul_inv, ← div_eq_mul_inv, div_le_div_iff₀ _ (sub_pos.2 hc)]
    swap
    · exact sub_pos.2 (pow_lt_one₀ (inv_nonneg.2 cpos.le) (inv_lt_one_of_one_lt₀ hc) two_ne_zero)
    have : c ^ 3 = c ^ 2 * c := by ring
    simp only [mul_sub, this, mul_one, inv_pow, sub_le_sub_iff_left]
    rw [mul_assoc, mul_comm c, ← mul_assoc, mul_inv_cancel₀ (sq_pos_of_pos cpos).ne', one_mul]
    simpa using pow_right_mono₀ hc.le one_le_two
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (hypothesis)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
⊢ ∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (β := ℕ) (c ^ i) 2 ≤
    HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹ / HPow.hPow (β := ℕ) j 2
have C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
Tactic: have C : c⁻¹ ^ 2 < 1 := pow_lt_one₀ (inv_nonneg.2 cpos.le) (inv_lt_one_of_one_lt₀ hc) two_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
⊢ LE.le (α := ℝ) (∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (β := ℕ) (c ^ i) 2)
    (∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, 1 / HPow.hPow (β := ℕ) (c ^ i) 2)
have h : {i ∈ range N | j < c ^ i} ⊆ Ico ⌊Real.log j / Real.log c⌋₊ N
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (hypothesis)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
i : ℕ
hi : i ∈ {i ∈ range N | j < c ^ i}
⊢ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N
have hi₁ : i < N ∧ j < c ^ i
Tactic: simp only [mem_filter, mem_range] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N
have h : ⌊Real.log j / Real.log c⌋₊ ≤ i
Tactic: simp only [hi.1, mem_Ico, and_true]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ ⌊Real.log j / Real.log c⌋₊ ≤ i
have h : Real.log j / Real.log c ≤ (↑i : ℝ)
Tactic: apply Nat.floor_le_of_le
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ Real.log j / Real.log c ≤ (↑i : ℝ)
have h : Real.log j / Real.log c < (↑i : ℝ)
Tactic: apply le_of_lt
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
i : ℕ
hi : i < N ∧ j < c ^ i
⊢ Real.log j / Real.log c < (↑i : ℝ)
have h : Real.log j < Real.log (c ^ i)
Tactic: rw [div_lt_iff₀ (Real.log_pos hc), ← Real.log_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
⊢ HPow.hPow (β := ℕ) c⁻¹ 2 ^ ⌊Real.log j / Real.log c⌋₊ / (1 - HPow.hPow (β := ℕ) c⁻¹ 2) ≤
    HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c - 1) / (1 - HPow.hPow (β := ℕ) c⁻¹ 2)
have hab : HPow.hPow (β := ℕ) c⁻¹ 2 ^ ⌊Real.log j / Real.log c⌋₊ ≤ HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c - 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
⊢ HPow.hPow (β := ℕ) c⁻¹ 2 ^ ⌊Real.log j / Real.log c⌋₊ ≤ HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c - 1)
have hab : HPow.hPow (β := ℝ) (HPow.hPow (β := ℕ) c⁻¹ 2) (↑⌊Real.log j / Real.log c⌋₊ : ℝ) ≤
  HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c - 1)
Tactic: rw [← Real.rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
⊢ HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c) = 1 / HPow.hPow (β := ℕ) j 2
have a : Membership.mem (γ := Set ℝ) (Set.Ioi 0) (1 / HPow.hPow (β := ℕ) j 2)
Tactic: apply Real.log_injOn_pos (Real.rpow_pos_of_pos A _)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
a : Membership.mem (γ := Set ℝ) (Set.Ioi 0) (1 / HPow.hPow (β := ℕ) j 2)
⊢ HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c) = 1 / HPow.hPow (β := ℕ) j 2
have a₁ : Real.log (HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c)) = Real.log (1 / HPow.hPow (β := ℕ) j 2)
Tactic: apply Real.log_injOn_pos (Real.rpow_pos_of_pos A _)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
⊢ Real.log (HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c)) = Real.log (1 / HPow.hPow (β := ℕ) j 2)
have a : Real.log j / Real.log c * Real.log (HPow.hPow (β := ℕ) c⁻¹ 2) = Real.log (1 / HPow.hPow (β := ℕ) j 2)
Tactic: rw [Real.log_rpow A]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
⊢ Real.log j / Real.log c * Real.log (HPow.hPow (β := ℕ) c⁻¹ 2) = Real.log (1 / HPow.hPow (β := ℕ) j 2)
have a : Real.log j / Real.log c * ((↑2 : ℝ) * Real.log c) = (↑2 : ℝ) * Real.log j
Tactic: simp only [one_div, Real.log_inv, Real.log_pow, mul_neg, neg_inj]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (hypothesis)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
⊢ HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c - 1) / (1 - HPow.hPow (β := ℕ) c⁻¹ 2) =
    HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ / HPow.hPow (β := ℕ) j 2
have I : HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c) = 1 / HPow.hPow (β := ℕ) j 2
Tactic: have I : (c⁻¹ ^ 2) ^ (Real.log j / Real.log c) = (1 : ℝ) / j ^ 2 := by
        apply Real.log_injOn_pos (Real.rpow_pos_of_pos A _)
        · rw [Set.mem_Ioi]; positivity
        rw [Real.log_rpow A]
        simp only [one_div, Real.log_inv, Real.log_pow, mul_neg, neg_inj]
        field [(Real.log_pos hc).ne']
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
I : HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c) = 1 / HPow.hPow (β := ℕ) j 2
⊢ HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c - 1) / (1 - HPow.hPow (β := ℕ) c⁻¹ 2) =
    HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ / HPow.hPow (β := ℕ) j 2
have rw : 1 / HPow.hPow (β := ℕ) j 2 / HPow.hPow (β := ℝ) (HPow.hPow (β := ℕ) c⁻¹ 2) 1 / (1 - HPow.hPow (β := ℕ) c⁻¹ 2) =
  HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ / HPow.hPow (β := ℕ) j 2
Tactic: rw [Real.rpow_sub A, I]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
I : HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c) = 1 / HPow.hPow (β := ℕ) j 2
⊢ 1 / HPow.hPow (β := ℕ) j 2 / HPow.hPow (β := ℝ) (HPow.hPow (β := ℕ) c⁻¹ 2) 1 / (1 - HPow.hPow (β := ℕ) c⁻¹ 2) =
    HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ / HPow.hPow (β := ℕ) j 2
have simp : (HPow.hPow (β := ℕ) j 2)⁻¹ * HPow.hPow (β := ℕ) c 2 / (1 - (HPow.hPow (β := ℕ) c 2)⁻¹) =
  HPow.hPow (β := ℕ) c 2 * (1 - (HPow.hPow (β := ℕ) c 2)⁻¹)⁻¹ / HPow.hPow (β := ℕ) j 2
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
⊢ HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ / HPow.hPow (β := ℕ) j 2 ≤
    HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹ / HPow.hPow (β := ℕ) j 2
have hc₁ : 0 ≤ HPow.hPow (β := ℕ) j 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
⊢ ∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (β := ℕ) (c ^ i) 2 ≤
    HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹ / HPow.hPow (β := ℕ) j 2
have i : LE.le (α := ℝ) (∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (β := ℕ) (c ^ i) 2)
  (∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, 1 / HPow.hPow (β := ℕ) (c ^ i) 2)
Tactic: calc
    (∑ i ∈ range N with j < c ^ i, (1 : ℝ) / (c ^ i) ^ 2) ≤
        ∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, (1 : ℝ) / (c ^ i) ^ 2 := by
      gcongr
      intro i hi
      simp only [mem_filter, mem_range] at hi
      simp only [hi.1, mem_Ico, and_true]
      apply Nat.floor_le_of_le
      apply le_of_lt
      rw [div_lt_iff₀ (Real.log_pos hc), ← Real.log_pow]
      exact Real.log_lt_log hj hi.2
    _ = ∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, (c⁻¹ ^ 2) ^ i := by
      simp [← pow_mul, mul_comm]
    _ ≤ (c⁻¹ ^ 2) ^ ⌊Real.log j / Real.log c⌋₊ / ((1 : ℝ) - c⁻¹ ^ 2) :=
      geom_sum_Ico_le_of_lt_one (sq_nonneg _) C
    _ ≤ (c⁻¹ ^ 2) ^ (Real.log j / Real.log c - 1) / ((1 : ℝ) - c⁻¹ ^ 2) := by
      gcongr
      rw [← Real.rpow_natCast]
      exact Real.rpow_le_rpow_of_exponent_ge A C.le (Nat.sub_one_lt_floor _).le
    _ = c ^ 2 * ((1 : ℝ) - c⁻¹ ^ 2)⁻¹ / j ^ 2 := by
      have I : (c⁻¹ ^ 2) ^ (Real.log j / Real.log c) = (1 : ℝ) / j ^ 2 := by
        apply Real.log_injOn_pos (Real.rpow_pos_of_pos A _)
        · rw [Set.mem_Ioi]; positivity
        rw [Real.log_rpow A]
        simp only [one_div, Real.log_inv, Real.log_pow, mul_neg, neg_inj]
        field [(Real.log_pos hc).ne']
      rw [Real.rpow_sub A, I]
      simp
      ring
    _ ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2 := by gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
i :
  LE.le (α := ℝ) (∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (β := ℕ) (c ^ i) 2)
    (∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, 1 / HPow.hPow (β := ℕ) (c ^ i) 2)
⊢ ∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (β := ℕ) (c ^ i) 2 ≤
    HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹ / HPow.hPow (β := ℕ) j 2
have i₁ : Eq (α := ℝ) (∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, 1 / HPow.hPow (β := ℕ) (c ^ i) 2)
  (∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, HPow.hPow (β := ℕ) c⁻¹ 2 ^ i)
Tactic: calc
    (∑ i ∈ range N with j < c ^ i, (1 : ℝ) / (c ^ i) ^ 2) ≤
        ∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, (1 : ℝ) / (c ^ i) ^ 2 := by
      gcongr
      intro i hi
      simp only [mem_filter, mem_range] at hi
      simp only [hi.1, mem_Ico, and_true]
      apply Nat.floor_le_of_le
      apply le_of_lt
      rw [div_lt_iff₀ (Real.log_pos hc), ← Real.log_pow]
      exact Real.log_lt_log hj hi.2
    _ = ∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, (c⁻¹ ^ 2) ^ i := by
      simp [← pow_mul, mul_comm]
    _ ≤ (c⁻¹ ^ 2) ^ ⌊Real.log j / Real.log c⌋₊ / ((1 : ℝ) - c⁻¹ ^ 2) :=
      geom_sum_Ico_le_of_lt_one (sq_nonneg _) C
    _ ≤ (c⁻¹ ^ 2) ^ (Real.log j / Real.log c - 1) / ((1 : ℝ) - c⁻¹ ^ 2) := by
      gcongr
      rw [← Real.rpow_natCast]
      exact Real.rpow_le_rpow_of_exponent_ge A C.le (Nat.sub_one_lt_floor _).le
    _ = c ^ 2 * ((1 : ℝ) - c⁻¹ ^ 2)⁻¹ / j ^ 2 := by
      have I : (c⁻¹ ^ 2) ^ (Real.log j / Real.log c) = (1 : ℝ) / j ^ 2 := by
        apply Real.log_injOn_pos (Real.rpow_pos_of_pos A _)
        · rw [Set.mem_Ioi]; positivity
        rw [Real.log_rpow A]
        simp only [one_div, Real.log_inv, Real.log_pow, mul_neg, neg_inj]
        field [(Real.log_pos hc).ne']
      rw [Real.rpow_sub A, I]
      simp
      ring
    _ ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2 := by gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
N : ℕ
j : ℝ
hj : 0 < j
c : ℝ
hc : 1 < c
cpos : 0 < c
A : 0 < HPow.hPow (β := ℕ) c⁻¹ 2
B : HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ ≤ HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹
C : HPow.hPow (β := ℕ) c⁻¹ 2 < 1
i :
  LE.le (α := ℝ) (∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (β := ℕ) (c ^ i) 2)
    (∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, 1 / HPow.hPow (β := ℕ) (c ^ i) 2)
i₁ :
  Eq (α := ℝ) (∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, 1 / HPow.hPow (β := ℕ) (c ^ i) 2)
    (∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, HPow.hPow (β := ℕ) c⁻¹ 2 ^ i)
⊢ ∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (β := ℕ) (c ^ i) 2 ≤
    HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹ / HPow.hPow (β := ℕ) j 2
have i₂ : HPow.hPow (β := ℕ) c⁻¹ 2 ^ ⌊Real.log j / Real.log c⌋₊ / (1 - HPow.hPow (β := ℕ) c⁻¹ 2) ≤
  HPow.hPow (β := ℕ) c⁻¹ 2 ^ (Real.log j / Real.log c - 1) / (1 - HPow.hPow (β := ℕ) c⁻¹ 2)
Tactic: calc
    (∑ i ∈ range N with j < c ^ i, (1 : ℝ) / (c ^ i) ^ 2) ≤
        ∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, (1 : ℝ) / (c ^ i) ^ 2 := by
      gcongr
      intro i hi
      simp only [mem_filter, mem_range] at hi
      simp only [hi.1, mem_Ico, and_true]
      apply Nat.floor_le_of_le
      apply le_of_lt
      rw [div_lt_iff₀ (Real.log_pos hc), ← Real.log_pow]
      exact Real.log_lt_log hj hi.2
    _ = ∑ i ∈ Ico ⌊Real.log j / Real.log c⌋₊ N, (c⁻¹ ^ 2) ^ i := by
      simp [← pow_mul, mul_comm]
    _ ≤ (c⁻¹ ^ 2) ^ ⌊Real.log j / Real.log c⌋₊ / ((1 : ℝ) - c⁻¹ ^ 2) :=
      geom_sum_Ico_le_of_lt_one (sq_nonneg _) C
    _ ≤ (c⁻¹ ^ 2) ^ (Real.log j / Real.log c - 1) / ((1 : ℝ) - c⁻¹ ^ 2) := by
      gcongr
      rw [← Real.rpow_natCast]
      exact Real.rpow_le_rpow_of_exponent_ge A C.le (Nat.sub_one_lt_floor _).le
    _ = c ^ 2 * ((1 : ℝ) - c⁻¹ ^ 2)⁻¹ / j ^ 2 := by
      have I : (c⁻¹ ^ 2) ^ (Real.log j / Real.log c) = (1 : ℝ) / j ^ 2 := by
        apply Real.log_injOn_pos (Real.rpow_pos_of_pos A _)
        · rw [Set.mem_Ioi]; positivity
        rw [Real.log_rpow A]
        simp only [one_div, Real.log_inv, Real.log_pow, mul_neg, neg_inj]
        field [(Real.log_pos hc).ne']
      rw [Real.rpow_sub A, I]
      simp
      ring
    _ ≤ c ^ 3 * (c - 1)⁻¹ / j ^ 2 := by gcongr