awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂ :
  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)
⊢ ∑ 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) / (1 - HPow.hPow (β := ℕ) c⁻¹ 2) =
  HPow.hPow (β := ℕ) c 2 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ / HPow.hPow (β := ℕ) j 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₁ :
  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₂ :
  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)
i₃ :
  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
⊢ ∑ 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 * (1 - HPow.hPow (β := ℕ) c⁻¹ 2)⁻¹ / HPow.hPow (β := ℕ) j 2 ≤
  HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹ / HPow.hPow (β := ℕ) j 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 (hypothesis)
Goal:
c : ℝ
hc : 1 < c
i : ℕ
⊢ (1 - c⁻¹) * c ^ i ≤ (↑⌊c ^ i⌋₊ : ℝ)
have cpos : 0 < c
Tactic: have cpos : 0 < c := zero_lt_one.trans hc
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
⊢ (1 - c⁻¹) * c ^ i ≤ (↑⌊c ^ i⌋₊ : ℝ)
have inl : (1 - c⁻¹) * HPow.hPow (β := ℕ) c 0 ≤ (↑⌊HPow.hPow (β := ℕ) c 0⌋₊ : ℝ)
Tactic: rcases eq_or_ne i 0 with (rfl | hi)
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
inl : (1 - c⁻¹) * HPow.hPow (β := ℕ) c 0 ≤ (↑⌊HPow.hPow (β := ℕ) c 0⌋₊ : ℝ)
⊢ (1 - c⁻¹) * c ^ i ≤ (↑⌊c ^ i⌋₊ : ℝ)
have inr : ∀ (hi : i ≠ 0), (1 - c⁻¹) * c ^ i ≤ (↑⌊c ^ i⌋₊ : ℝ)
Tactic: rcases eq_or_ne i 0 with (rfl | hi)
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i ≠ 0
⊢ c ^ i - c ^ i * c⁻¹ ≤ c ^ i - 1
have h : 1 ≤ c ^ i * c⁻¹
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i ≠ 0
⊢ (1 - c⁻¹) * c ^ i ≤ (↑⌊c ^ i⌋₊ : ℝ)
have c₁ : (1 - c⁻¹) * c ^ i = c ^ i - c ^ i * c⁻¹
Tactic: calc
    (1 - c⁻¹) * c ^ i = c ^ i - c ^ i * c⁻¹ := by ring
    _ ≤ c ^ i - 1 := by
      gcongr
      simpa only [← div_eq_mul_inv, one_le_div cpos, pow_one] using le_self_pow₀ hc.le hi
    _ ≤ ⌊c ^ i⌋₊ := (Nat.sub_one_lt_floor _).le
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.FloorPow (goal)
Goal:
c : ℝ
hc : 1 < c
i : ℕ
cpos : 0 < c
hi : i ≠ 0
c₁ : (1 - c⁻¹) * c ^ i = c ^ i - c ^ i * c⁻¹
⊢ (1 - c⁻¹) * c ^ i ≤ (↑⌊c ^ i⌋₊ : ℝ)
have c₂ : c ^ i - c ^ i * c⁻¹ ≤ c ^ i - 1
Tactic: calc
    (1 - c⁻¹) * c ^ i = c ^ i - c ^ i * c⁻¹ := by ring
    _ ≤ c ^ i - 1 := by
      gcongr
      simpa only [← div_eq_mul_inv, one_le_div cpos, pow_one] using le_self_pow₀ hc.le hi
    _ ≤ ⌊c ^ i⌋₊ := (Nat.sub_one_lt_floor _).le
-- 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 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / 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 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (β := ℕ) j 2
have A : 0 < 1 - c⁻¹
Tactic: have A : 0 < 1 - c⁻¹ := sub_pos.2 (inv_lt_one_of_one_lt₀ 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 < 1 - c⁻¹
⊢ LE.le (α := ℝ) (∑ i ∈ range N with j < (↑⌊c ^ i⌋₊ : ℝ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2)
    (∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2)
have h : ∀ (k : ℕ) (hk : k ∈ range N), (↑⌊c ^ k⌋₊ : ℝ) ≤ c ^ k
Tactic: gcongr with k hk
-- 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 < 1 - c⁻¹
⊢ LE.le (α := ℝ) (∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2)
    (∑ i ∈ range N with j < c ^ i, HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (1 / HPow.hPow (β := ℕ) (c ^ i) 2))
have h : ∀ i ∈ {i ∈ range N | j < c ^ i},
  1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2 ≤
    HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (1 / HPow.hPow (β := ℕ) (c ^ i) 2)
Tactic: gcongr with 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 < 1 - c⁻¹
i : ℕ
h : i ∈ {i ∈ range N | j < c ^ i}
⊢ 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2 ≤
    HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (1 / HPow.hPow (β := ℕ) (c ^ i) 2)
have h : 1 * HPow.hPow (β := ℕ) (c ^ i) 2 ≤ HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2
Tactic: rw [mul_div_assoc', mul_one, div_le_div_iff₀]
-- 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 < 1 - c⁻¹
i : ℕ
h_1 : i ∈ {i ∈ range N | j < c ^ i}
h : 1 * HPow.hPow (β := ℕ) (c ^ i) 2 ≤ HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2
⊢ 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2 ≤
    HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (1 / HPow.hPow (β := ℕ) (c ^ i) 2)
have h₁ : 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2
Tactic: rw [mul_div_assoc', mul_one, div_le_div_iff₀]
-- 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 < 1 - c⁻¹
i : ℕ
h_1 : i ∈ {i ∈ range N | j < c ^ i}
h : 1 * HPow.hPow (β := ℕ) (c ^ i) 2 ≤ HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2
h₁ : 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2
⊢ 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2 ≤
    HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (1 / HPow.hPow (β := ℕ) (c ^ i) 2)
have h₂ : 0 < HPow.hPow (β := ℕ) (c ^ i) 2
Tactic: rw [mul_div_assoc', mul_one, div_le_div_iff₀]
-- 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 < 1 - c⁻¹
i : ℕ
h : i ∈ {i ∈ range N | j < c ^ i}
⊢ 0 < HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2
have h : LT.lt (α := ℝ) 0 (↑⌊c ^ i⌋₊ : ℝ)
Tactic: apply sq_pos_of_pos
-- 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 < 1 - c⁻¹
i : ℕ
h : i ∈ {i ∈ range N | j < c ^ i}
⊢ LT.lt (α := ℝ) 0 (↑⌊c ^ i⌋₊ : ℝ)
have h : LE.le (α := ℝ) 1 (↑⌊c ^ i⌋₊ : ℝ)
Tactic: refine zero_lt_one.trans_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 < 1 - c⁻¹
i : ℕ
h : i ∈ {i ∈ range N | j < c ^ i}
⊢ 1 * HPow.hPow (β := ℕ) (c ^ i) 2 ≤ HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2
have h : HPow.hPow (β := ℕ) (c ^ i) 2 ≤ HPow.hPow (β := ℕ) ((1 - c⁻¹)⁻¹ * (↑⌊c ^ i⌋₊ : ℝ)) 2
Tactic: rw [one_mul, ← mul_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 < 1 - c⁻¹
i : ℕ
h : i ∈ {i ∈ range N | j < c ^ i}
⊢ HPow.hPow (β := ℕ) (c ^ i) 2 ≤ HPow.hPow (β := ℕ) ((1 - c⁻¹)⁻¹ * (↑⌊c ^ i⌋₊ : ℝ)) 2
have h : c ^ i ≤ (1 - c⁻¹)⁻¹ * (↑⌊c ^ i⌋₊ : ℝ)
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 < 1 - c⁻¹
i : ℕ
h : i ∈ {i ∈ range N | j < c ^ i}
⊢ c ^ i ≤ (1 - c⁻¹)⁻¹ * (↑⌊c ^ i⌋₊ : ℝ)
have h : (1 - c⁻¹) * c ^ i ≤ (↑⌊c ^ i⌋₊ : ℝ)
Tactic: rw [← div_eq_inv_mul, le_div_iff₀ A, mul_comm]
-- 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 < 1 - c⁻¹
⊢ ∑ i ∈ range N with j < c ^ i, HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (1 / HPow.hPow (β := ℕ) (c ^ i) 2) ≤
    HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹) / HPow.hPow (β := ℕ) j 2
have rw : HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * ∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (β := ℕ) (c ^ i) 2 ≤
  HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹ / HPow.hPow (β := ℕ) j 2)
Tactic: rw [← mul_sum, ← mul_div_assoc']
-- 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 < 1 - c⁻¹
⊢ HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * ∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (β := ℕ) (c ^ i) 2 ≤
    HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹ / HPow.hPow (β := ℕ) j 2)
have hbc : ∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (β := ℕ) (c ^ i) 2 ≤
  HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹ / 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 < 1 - c⁻¹
⊢ HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹) / HPow.hPow (β := ℕ) j 2 =
    HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (β := ℕ) j 2
have e_a : HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹) =
  HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3
Tactic: congr 1
-- 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 < 1 - c⁻¹
⊢ ∑ i ∈ range N with j < (↑⌊c ^ i⌋₊ : ℝ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2 ≤
    HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (β := ℕ) j 2
have i : LE.le (α := ℝ) (∑ i ∈ range N with j < (↑⌊c ^ i⌋₊ : ℝ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2)
  (∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2)
Tactic: calc
    (∑ i ∈ range N with j < ⌊c ^ i⌋₊, (1 : ℝ) / (⌊c ^ i⌋₊ : ℝ) ^ 2) ≤
        ∑ i ∈ range N with j < c ^ i, (1 : ℝ) / (⌊c ^ i⌋₊ : ℝ) ^ 2 := by
      gcongr with k hk; exact Nat.floor_le (by positivity)
    _ ≤ ∑ i ∈ range N with j < c ^ i, (1 - c⁻¹)⁻¹ ^ 2 * ((1 : ℝ) / (c ^ i) ^ 2) := by
      gcongr with i
      rw [mul_div_assoc', mul_one, div_le_div_iff₀]; rotate_left
      · apply sq_pos_of_pos
        refine zero_lt_one.trans_le ?_
        simp only [Nat.le_floor, one_le_pow₀, hc.le, Nat.one_le_cast, Nat.cast_one]
      · exact sq_pos_of_pos (pow_pos cpos _)
      rw [one_mul, ← mul_pow]
      gcongr
      rw [← div_eq_inv_mul, le_div_iff₀ A, mul_comm]
      exact mul_pow_le_nat_floor_pow hc i
    _ ≤ (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹) / j ^ 2 := by
      rw [← mul_sum, ← mul_div_assoc']
      gcongr
      exact sum_div_pow_sq_le_div_sq N hj hc
    _ = c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2 := by
      congr 1
      field
-- 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 < 1 - c⁻¹
i :
  LE.le (α := ℝ) (∑ i ∈ range N with j < (↑⌊c ^ i⌋₊ : ℝ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2)
    (∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2)
⊢ ∑ i ∈ range N with j < (↑⌊c ^ i⌋₊ : ℝ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2 ≤
    HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (β := ℕ) j 2
have i₁ : LE.le (α := ℝ) (∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2)
  (∑ i ∈ range N with j < c ^ i, HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (1 / HPow.hPow (β := ℕ) (c ^ i) 2))
Tactic: calc
    (∑ i ∈ range N with j < ⌊c ^ i⌋₊, (1 : ℝ) / (⌊c ^ i⌋₊ : ℝ) ^ 2) ≤
        ∑ i ∈ range N with j < c ^ i, (1 : ℝ) / (⌊c ^ i⌋₊ : ℝ) ^ 2 := by
      gcongr with k hk; exact Nat.floor_le (by positivity)
    _ ≤ ∑ i ∈ range N with j < c ^ i, (1 - c⁻¹)⁻¹ ^ 2 * ((1 : ℝ) / (c ^ i) ^ 2) := by
      gcongr with i
      rw [mul_div_assoc', mul_one, div_le_div_iff₀]; rotate_left
      · apply sq_pos_of_pos
        refine zero_lt_one.trans_le ?_
        simp only [Nat.le_floor, one_le_pow₀, hc.le, Nat.one_le_cast, Nat.cast_one]
      · exact sq_pos_of_pos (pow_pos cpos _)
      rw [one_mul, ← mul_pow]
      gcongr
      rw [← div_eq_inv_mul, le_div_iff₀ A, mul_comm]
      exact mul_pow_le_nat_floor_pow hc i
    _ ≤ (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹) / j ^ 2 := by
      rw [← mul_sum, ← mul_div_assoc']
      gcongr
      exact sum_div_pow_sq_le_div_sq N hj hc
    _ = c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2 := by
      congr 1
      field
-- 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 < 1 - c⁻¹
i :
  LE.le (α := ℝ) (∑ i ∈ range N with j < (↑⌊c ^ i⌋₊ : ℝ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2)
    (∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2)
i₁ :
  LE.le (α := ℝ) (∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2)
    (∑ i ∈ range N with j < c ^ i, HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (1 / HPow.hPow (β := ℕ) (c ^ i) 2))
⊢ ∑ i ∈ range N with j < (↑⌊c ^ i⌋₊ : ℝ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2 ≤
    HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (β := ℕ) j 2
have i₂ : ∑ i ∈ range N with j < c ^ i, HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (1 / HPow.hPow (β := ℕ) (c ^ i) 2) ≤
  HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹) / HPow.hPow (β := ℕ) j 2
Tactic: calc
    (∑ i ∈ range N with j < ⌊c ^ i⌋₊, (1 : ℝ) / (⌊c ^ i⌋₊ : ℝ) ^ 2) ≤
        ∑ i ∈ range N with j < c ^ i, (1 : ℝ) / (⌊c ^ i⌋₊ : ℝ) ^ 2 := by
      gcongr with k hk; exact Nat.floor_le (by positivity)
    _ ≤ ∑ i ∈ range N with j < c ^ i, (1 - c⁻¹)⁻¹ ^ 2 * ((1 : ℝ) / (c ^ i) ^ 2) := by
      gcongr with i
      rw [mul_div_assoc', mul_one, div_le_div_iff₀]; rotate_left
      · apply sq_pos_of_pos
        refine zero_lt_one.trans_le ?_
        simp only [Nat.le_floor, one_le_pow₀, hc.le, Nat.one_le_cast, Nat.cast_one]
      · exact sq_pos_of_pos (pow_pos cpos _)
      rw [one_mul, ← mul_pow]
      gcongr
      rw [← div_eq_inv_mul, le_div_iff₀ A, mul_comm]
      exact mul_pow_le_nat_floor_pow hc i
    _ ≤ (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹) / j ^ 2 := by
      rw [← mul_sum, ← mul_div_assoc']
      gcongr
      exact sum_div_pow_sq_le_div_sq N hj hc
    _ = c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2 := by
      congr 1
      field
-- 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 < 1 - c⁻¹
i :
  LE.le (α := ℝ) (∑ i ∈ range N with j < (↑⌊c ^ i⌋₊ : ℝ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2)
    (∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2)
i₁ :
  LE.le (α := ℝ) (∑ i ∈ range N with j < c ^ i, 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2)
    (∑ i ∈ range N with j < c ^ i, HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (1 / HPow.hPow (β := ℕ) (c ^ i) 2))
i₂ :
  ∑ i ∈ range N with j < c ^ i, HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (1 / HPow.hPow (β := ℕ) (c ^ i) 2) ≤
    HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹) / HPow.hPow (β := ℕ) j 2
⊢ ∑ i ∈ range N with j < (↑⌊c ^ i⌋₊ : ℝ), 1 / HPow.hPow (α := ℝ) (β := ℕ) (↑⌊c ^ i⌋₊ : ℝ) 2 ≤
    HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (β := ℕ) j 2
have i₃ : HPow.hPow (β := ℕ) (1 - c⁻¹)⁻¹ 2 * (HPow.hPow (β := ℕ) c 3 * (c - 1)⁻¹) / HPow.hPow (β := ℕ) j 2 =
  HPow.hPow (β := ℕ) c 5 * HPow.hPow (β := ℕ) (c - 1)⁻¹ 3 / HPow.hPow (β := ℕ) j 2
Tactic: calc
    (∑ i ∈ range N with j < ⌊c ^ i⌋₊, (1 : ℝ) / (⌊c ^ i⌋₊ : ℝ) ^ 2) ≤
        ∑ i ∈ range N with j < c ^ i, (1 : ℝ) / (⌊c ^ i⌋₊ : ℝ) ^ 2 := by
      gcongr with k hk; exact Nat.floor_le (by positivity)
    _ ≤ ∑ i ∈ range N with j < c ^ i, (1 - c⁻¹)⁻¹ ^ 2 * ((1 : ℝ) / (c ^ i) ^ 2) := by
      gcongr with i
      rw [mul_div_assoc', mul_one, div_le_div_iff₀]; rotate_left
      · apply sq_pos_of_pos
        refine zero_lt_one.trans_le ?_
        simp only [Nat.le_floor, one_le_pow₀, hc.le, Nat.one_le_cast, Nat.cast_one]
      · exact sq_pos_of_pos (pow_pos cpos _)
      rw [one_mul, ← mul_pow]
      gcongr
      rw [← div_eq_inv_mul, le_div_iff₀ A, mul_comm]
      exact mul_pow_le_nat_floor_pow hc i
    _ ≤ (1 - c⁻¹)⁻¹ ^ 2 * (c ^ 3 * (c - 1)⁻¹) / j ^ 2 := by
      rw [← mul_sum, ← mul_div_assoc']
      gcongr
      exact sum_div_pow_sq_le_div_sq N hj hc
    _ = c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2 := by
      congr 1
      field
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
inst : NormedRing α
inst_1 : NormSMulClass ℤ α
inst_2 : Nontrivial α
⊢ Tendsto Nat.cast atTop (Bornology.cobounded α)
have rw : Tendsto (β := ℝ) (fun (x : ℕ) ↦ norm.{u_1} (E := α) (↑x : α)) atTop atTop
Tactic: rw [← tendsto_norm_atTop_iff_cobounded]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
α : Type u_1
inst : NormedRing α
inst_1 : NormSMulClass ℤ α
inst_2 : Nontrivial α
⊢ Tendsto Int.cast (atBot ⊔ atTop) (Bornology.cobounded α)
have rw : Tendsto (β := ℝ) (fun (x : ℤ) ↦ norm.{u_1} (E := α) (↑x : α)) (atBot ⊔ atTop) atTop
Tactic: rw [← tendsto_norm_atTop_iff_cobounded]
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (goal)
Goal:
r₁ r₂ : ℝ
h : |r₁| < |r₂|
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (n : ℕ) ↦ r₁ ^ n) fun (n : ℕ) ↦ r₂ ^ n
have refine : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℕ) ↦ ‖r₁ ^ x‖) fun (x : ℕ) ↦ ‖r₂ ^ x‖
Tactic: refine (IsLittleO.of_norm_left ?_).of_norm_right
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
f : ℕ → ℝ
R : ℝ
⊢ [∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x,
      ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x,
      ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x,
      ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x,
      ∃ a < R, ∃ (C : ℝ), (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a < R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n].TFAE
have A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
Tactic: have A : Ico 0 R ⊆ Ioo (-R) R :=
    fun x hx ↦ ⟨(neg_lt_zero.2 (hx.1.trans_lt hx.2)).trans_le hx.1, hx.2⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
⊢ [∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x,
      ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x,
      ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x,
      ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x,
      ∃ a < R, ∃ (C : ℝ), (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a < R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n].TFAE
have B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
Tactic: have B : Ioo 0 R ⊆ Ioo (-R) R := Subset.trans Ioo_subset_Ico_self A
-- Lean 4 proof step from Mathlib.Analysis.SpecificLimits.Normed (hypothesis)
Goal:
f : ℕ → ℝ
R : ℝ
A : Set.Ico 0 R ⊆ Set.Ioo (-R) R
B : Set.Ioo 0 R ⊆ Set.Ioo (-R) R
⊢ [∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x,
      ∃ a ∈ Set.Ioo 0 R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x,
      ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x,
      ∃ a ∈ Set.Ioo 0 R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x,
      ∃ a < R, ∃ (C : ℝ), (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a < R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n,
      ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in atTop, |f n| ≤ a ^ n].TFAE
have tfae_1_to_3 : ∀ (a : ∃ a ∈ Set.Ioo (-R) R, IsLittleO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x),
  ∃ a ∈ Set.Ioo (-R) R, IsBigO (F := ℝ) atTop f fun (x : ℕ) ↦ a ^ x
Tactic: tfae_have 1 → 3 := fun ⟨a, ha, H⟩ ↦ ⟨a, ha, H.isBigO⟩