awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
zero :
  ∑ n ∈ Finset.range 0, term (n + 1) 1 =
    log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
zero₁ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
zero₂ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic 0 + (↑(HAdd.hAdd (α := ℕ) 0 1) : ℚ)⁻¹) : ℝ) + 1
⊢ term_sum 1 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
have zero₃ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(HAdd.hAdd (α := ℚ) 0 (↑(HAdd.hAdd (α := ℕ) 0 1) : ℚ)⁻¹) : ℝ) + 1
Tactic: simp_rw [term_sum, Finset.sum_range_zero, harmonic_succ, harmonic_zero,
      Nat.cast_zero, zero_add, Nat.cast_one, inv_one, Rat.cast_one, log_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
zero :
  ∑ n ∈ Finset.range 0, term (n + 1) 1 =
    log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
zero₁ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
zero₂ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic 0 + (↑(HAdd.hAdd (α := ℕ) 0 1) : ℚ)⁻¹) : ℝ) + 1
zero₃ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(HAdd.hAdd (α := ℚ) 0 (↑(HAdd.hAdd (α := ℕ) 0 1) : ℚ)⁻¹) : ℝ) + 1
⊢ term_sum 1 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
have zero₄ : 0 = log (HAdd.hAdd (α := ℝ) 0 1) - (↑(HAdd.hAdd (α := ℚ) 0 (↑(HAdd.hAdd (α := ℕ) 0 1) : ℚ)⁻¹) : ℝ) + 1
Tactic: simp_rw [term_sum, Finset.sum_range_zero, harmonic_succ, harmonic_zero,
      Nat.cast_zero, zero_add, Nat.cast_one, inv_one, Rat.cast_one, log_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
zero :
  ∑ n ∈ Finset.range 0, term (n + 1) 1 =
    log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
zero₁ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
zero₂ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic 0 + (↑(HAdd.hAdd (α := ℕ) 0 1) : ℚ)⁻¹) : ℝ) + 1
zero₃ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(HAdd.hAdd (α := ℚ) 0 (↑(HAdd.hAdd (α := ℕ) 0 1) : ℚ)⁻¹) : ℝ) + 1
zero₄ : 0 = log (HAdd.hAdd (α := ℝ) 0 1) - (↑(HAdd.hAdd (α := ℚ) 0 (↑(HAdd.hAdd (α := ℕ) 0 1) : ℚ)⁻¹) : ℝ) + 1
⊢ term_sum 1 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
have zero₅ : 0 = log 1 - (↑(↑1 : ℚ)⁻¹ : ℝ) + 1
Tactic: simp_rw [term_sum, Finset.sum_range_zero, harmonic_succ, harmonic_zero,
      Nat.cast_zero, zero_add, Nat.cast_one, inv_one, Rat.cast_one, log_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
zero :
  ∑ n ∈ Finset.range 0, term (n + 1) 1 =
    log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
zero₁ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
zero₂ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic 0 + (↑(HAdd.hAdd (α := ℕ) 0 1) : ℚ)⁻¹) : ℝ) + 1
zero₃ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(HAdd.hAdd (α := ℚ) 0 (↑(HAdd.hAdd (α := ℕ) 0 1) : ℚ)⁻¹) : ℝ) + 1
zero₄ : 0 = log (HAdd.hAdd (α := ℝ) 0 1) - (↑(HAdd.hAdd (α := ℚ) 0 (↑(HAdd.hAdd (α := ℕ) 0 1) : ℚ)⁻¹) : ℝ) + 1
zero₅ : 0 = log 1 - (↑(↑1 : ℚ)⁻¹ : ℝ) + 1
⊢ term_sum 1 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
have zero₆ : 0 = log 1 - (↑1⁻¹ : ℝ) + 1
Tactic: simp_rw [term_sum, Finset.sum_range_zero, harmonic_succ, harmonic_zero,
      Nat.cast_zero, zero_add, Nat.cast_one, inv_one, Rat.cast_one, log_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
zero :
  ∑ n ∈ Finset.range 0, term (n + 1) 1 =
    log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
zero₁ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
zero₂ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic 0 + (↑(HAdd.hAdd (α := ℕ) 0 1) : ℚ)⁻¹) : ℝ) + 1
zero₃ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(HAdd.hAdd (α := ℚ) 0 (↑(HAdd.hAdd (α := ℕ) 0 1) : ℚ)⁻¹) : ℝ) + 1
zero₄ : 0 = log (HAdd.hAdd (α := ℝ) 0 1) - (↑(HAdd.hAdd (α := ℚ) 0 (↑(HAdd.hAdd (α := ℕ) 0 1) : ℚ)⁻¹) : ℝ) + 1
zero₅ : 0 = log 1 - (↑(↑1 : ℚ)⁻¹ : ℝ) + 1
zero₆ : 0 = log 1 - (↑1⁻¹ : ℝ) + 1
⊢ term_sum 1 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
have zero₇ : 0 = log 1 - (↑1 : ℝ) + 1
Tactic: simp_rw [term_sum, Finset.sum_range_zero, harmonic_succ, harmonic_zero,
      Nat.cast_zero, zero_add, Nat.cast_one, inv_one, Rat.cast_one, log_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
zero :
  ∑ n ∈ Finset.range 0, term (n + 1) 1 =
    log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
zero₁ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
zero₂ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic 0 + (↑(HAdd.hAdd (α := ℕ) 0 1) : ℚ)⁻¹) : ℝ) + 1
zero₃ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(HAdd.hAdd (α := ℚ) 0 (↑(HAdd.hAdd (α := ℕ) 0 1) : ℚ)⁻¹) : ℝ) + 1
zero₄ : 0 = log (HAdd.hAdd (α := ℝ) 0 1) - (↑(HAdd.hAdd (α := ℚ) 0 (↑(HAdd.hAdd (α := ℕ) 0 1) : ℚ)⁻¹) : ℝ) + 1
zero₅ : 0 = log 1 - (↑(↑1 : ℚ)⁻¹ : ℝ) + 1
zero₆ : 0 = log 1 - (↑1⁻¹ : ℝ) + 1
zero₇ : 0 = log 1 - (↑1 : ℝ) + 1
⊢ term_sum 1 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
have zero₈ : 0 = log 1 - 1 + 1
Tactic: simp_rw [term_sum, Finset.sum_range_zero, harmonic_succ, harmonic_zero,
      Nat.cast_zero, zero_add, Nat.cast_one, inv_one, Rat.cast_one, log_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
zero :
  ∑ n ∈ Finset.range 0, term (n + 1) 1 =
    log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
zero₁ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
zero₂ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic 0 + (↑(HAdd.hAdd (α := ℕ) 0 1) : ℚ)⁻¹) : ℝ) + 1
zero₃ : 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(HAdd.hAdd (α := ℚ) 0 (↑(HAdd.hAdd (α := ℕ) 0 1) : ℚ)⁻¹) : ℝ) + 1
zero₄ : 0 = log (HAdd.hAdd (α := ℝ) 0 1) - (↑(HAdd.hAdd (α := ℚ) 0 (↑(HAdd.hAdd (α := ℕ) 0 1) : ℚ)⁻¹) : ℝ) + 1
zero₅ : 0 = log 1 - (↑(↑1 : ℚ)⁻¹ : ℝ) + 1
zero₆ : 0 = log 1 - (↑1⁻¹ : ℝ) + 1
zero₇ : 0 = log 1 - (↑1 : ℝ) + 1
zero₈ : 0 = log 1 - 1 + 1
⊢ term_sum 1 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
have zero₉ : 0 = HSub.hSub (α := ℝ) 0 1 + 1
Tactic: simp_rw [term_sum, Finset.sum_range_zero, harmonic_succ, harmonic_zero,
      Nat.cast_zero, zero_add, Nat.cast_one, inv_one, Rat.cast_one, log_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
N : ℕ
hN : ∑ n ∈ Finset.range N, term (n + 1) 1 = log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) - (↑(harmonic (N + 1)) : ℝ) + 1
⊢ ∑ n ∈ Finset.range (N + 1), term (n + 1) 1 =
    log (HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 1) - (↑(harmonic (N + 1 + 1)) : ℝ) + 1
have succ : log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) - (↑(harmonic (N + 1)) : ℝ) + 1 +
    (log (HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 1) - log (↑(N + 1) : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 1) =
  log (HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 1) - (↑(harmonic (N + 1) + (↑(N + 1 + 1) : ℚ)⁻¹) : ℝ) + 1
Tactic: rw [Finset.sum_range_succ, hN, harmonic_succ (N + 1),
      term_one (by positivity : 0 < N + 1)]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
N : ℕ
hN : ∑ n ∈ Finset.range N, term (n + 1) 1 = log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) - (↑(harmonic (N + 1)) : ℝ) + 1
⊢ log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) - (↑(harmonic (N + 1)) : ℝ) + 1 +
      (log (HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 1) - log (↑(N + 1) : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 1) =
    log (HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 1) - (↑(harmonic (N + 1) + (↑(N + 1 + 1) : ℚ)⁻¹) : ℝ) + 1
have succ : log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) - (↑(harmonic (N + 1)) : ℝ) + 1 +
    (log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 + 1) - log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) -
      1 / (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 + 1)) =
  log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 + 1) - ((↑(harmonic (N + 1)) : ℝ) + (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1 + 1)⁻¹) + 1
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
N : ℕ
⊢ term_sum 1 N = log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) - (↑(harmonic (N + 1)) : ℝ) + 1
have zero : term_sum 1 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
Tactic: induction N with
  | zero =>
    simp_rw [term_sum, Finset.sum_range_zero, harmonic_succ, harmonic_zero,
      Nat.cast_zero, zero_add, Nat.cast_one, inv_one, Rat.cast_one, log_one, sub_add_cancel]
  | succ N hN =>
    unfold term_sum at hN ⊢
    rw [Finset.sum_range_succ, hN, harmonic_succ (N + 1),
      term_one (by positivity : 0 < N + 1)]
    push_cast
    ring_nf
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
N : ℕ
zero : term_sum 1 0 = log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - (↑(harmonic (HAdd.hAdd (α := ℕ) 0 1)) : ℝ) + 1
⊢ term_sum 1 N = log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) - (↑(harmonic (N + 1)) : ℝ) + 1
have succ : ∀ (N : ℕ) (hN : term_sum 1 N = log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) - (↑(harmonic (N + 1)) : ℝ) + 1),
  term_sum 1 (N + 1) = log (HAdd.hAdd (α := ℝ) (↑(N + 1) : ℝ) 1) - (↑(harmonic (N + 1 + 1)) : ℝ) + 1
Tactic: induction N with
  | zero =>
    simp_rw [term_sum, Finset.sum_range_zero, harmonic_succ, harmonic_zero,
      Nat.cast_zero, zero_add, Nat.cast_one, inv_one, Rat.cast_one, log_one, sub_add_cancel]
  | succ N hN =>
    unfold term_sum at hN ⊢
    rw [Finset.sum_range_succ, hN, harmonic_succ (N + 1),
      term_one (by positivity : 0 < N + 1)]
    push_cast
    ring_nf
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
⊢ HasSum (fun (n : ℕ) ↦ term (n + 1) 1) (1 - γ)
have rw : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, term (i + 1) 1) atTop (𝓝 (1 - γ))
Tactic: rw [hasSum_iff_tendsto_nat_of_nonneg (fun n ↦ term_nonneg (n + 1) 1)]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
⊢ Tendsto (fun (N : ℕ) ↦ term_sum 1 N) atTop (𝓝 (1 - γ))
have simp_rw : Tendsto (fun (N : ℕ) ↦ -(↑(harmonic (N + 1)) : ℝ) + log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) + 1) atTop (𝓝 (-γ + 1))
Tactic: simp_rw [term_sum_one, sub_eq_neg_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
⊢ Tendsto (fun (N : ℕ) ↦ -(↑(harmonic (N + 1)) : ℝ) + log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1) + 1) atTop (𝓝 (-γ + 1))
have refine : Tendsto (fun (N : ℕ) ↦ -(↑(harmonic (N + 1)) : ℝ) + log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)) atTop (𝓝 (-γ))
Tactic: refine Tendsto.add ?_ tendsto_const_nhds
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (hypothesis)
Goal:
⊢ Tendsto (fun (N : ℕ) ↦ -(↑(harmonic (N + 1)) : ℝ) + log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)) atTop (𝓝 (-γ))
have this : Tendsto (fun (x : ℕ) ↦ -(eulerMascheroniSeq' ∘ fun (a : ℕ) ↦ a + 1) x) atTop (𝓝 (-γ))
Tactic: have := (tendsto_eulerMascheroniSeq'.comp (tendsto_add_atTop_nat 1)).neg
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
this : Tendsto (fun (x : ℕ) ↦ -(eulerMascheroniSeq' ∘ fun (a : ℕ) ↦ a + 1) x) atTop (𝓝 (-γ))
⊢ Tendsto (fun (N : ℕ) ↦ -(↑(harmonic (N + 1)) : ℝ) + log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)) atTop (𝓝 (-γ))
have refine : ∀ (n : ℕ),
  -(eulerMascheroniSeq' ∘ fun (a : ℕ) ↦ a + 1) n =
    (fun (N : ℕ) ↦ -(↑(harmonic (N + 1)) : ℝ) + log (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)) n
Tactic: refine this.congr' (Eventually.of_forall (fun n ↦ ?_))
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
this : Tendsto (fun (x : ℕ) ↦ -(eulerMascheroniSeq' ∘ fun (a : ℕ) ↦ a + 1) x) atTop (𝓝 (-γ))
n : ℕ
⊢ -((↑(harmonic (n + 1)) : ℝ) - log (↑(n + 1) : ℝ)) = -(↑(harmonic (n + 1)) : ℝ) + log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have push_cast : -((↑(harmonic (n + 1)) : ℝ) - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) =
  -(↑(harmonic (n + 1)) : ℝ) + log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (hypothesis)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
x : ℝ
hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ 0 < x
have hx₁ : x ∈ Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: rw [uIcc_of_le (by simp only [le_add_iff_nonneg_right, zero_le_one])] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (hypothesis)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
⊢ term n s =
    1 / (s - 1) * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) (s - 1) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ (s - 1)) -
      (↑n : ℝ) / s * (1 / HPow.hPow (α := ℝ) (↑n : ℝ) s - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s)
have hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
Tactic: have hv : ∀ x ∈ uIcc (n : ℝ) (n + 1), 0 < x := by
    intro x hx
    rw [uIcc_of_le (by simp only [le_add_iff_nonneg_right, zero_le_one])] at hx
    exact (Nat.cast_pos.mpr hn).trans_le hx.1
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ Eq (α := ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / x ^ (s + 1))
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1)))
have refine : ∀ (x : ℝ) (hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)),
  (x - (↑n : ℝ)) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
Tactic: refine intervalIntegral.integral_congr (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ (x - (↑n : ℝ)) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
have rw : x / x ^ (s + 1) - (↑n : ℝ) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
Tactic: rw [sub_div, rpow_add_one (hv x hx).ne', mul_comm, ← div_div, div_self (hv x hx).ne',
        rpow_neg (hv x hx).le, rpow_neg (hv x hx).le, one_div, rpow_add_one (hv x hx).ne', mul_comm,
        div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
rw : x / x ^ (s + 1) - (↑n : ℝ) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
⊢ (x - (↑n : ℝ)) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
have rw₁ : x / (x ^ s * x) - (↑n : ℝ) / (x ^ s * x) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
Tactic: rw [sub_div, rpow_add_one (hv x hx).ne', mul_comm, ← div_div, div_self (hv x hx).ne',
        rpow_neg (hv x hx).le, rpow_neg (hv x hx).le, one_div, rpow_add_one (hv x hx).ne', mul_comm,
        div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
rw : x / x ^ (s + 1) - (↑n : ℝ) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₁ : x / (x ^ s * x) - (↑n : ℝ) / (x ^ s * x) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
⊢ (x - (↑n : ℝ)) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
have rw₂ : x / (x * x ^ s) - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
Tactic: rw [sub_div, rpow_add_one (hv x hx).ne', mul_comm, ← div_div, div_self (hv x hx).ne',
        rpow_neg (hv x hx).le, rpow_neg (hv x hx).le, one_div, rpow_add_one (hv x hx).ne', mul_comm,
        div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
rw : x / x ^ (s + 1) - (↑n : ℝ) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₁ : x / (x ^ s * x) - (↑n : ℝ) / (x ^ s * x) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₂ : x / (x * x ^ s) - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
⊢ (x - (↑n : ℝ)) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
have rw₃ : x / x / x ^ s - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
Tactic: rw [sub_div, rpow_add_one (hv x hx).ne', mul_comm, ← div_div, div_self (hv x hx).ne',
        rpow_neg (hv x hx).le, rpow_neg (hv x hx).le, one_div, rpow_add_one (hv x hx).ne', mul_comm,
        div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
rw : x / x ^ (s + 1) - (↑n : ℝ) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₁ : x / (x ^ s * x) - (↑n : ℝ) / (x ^ s * x) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₂ : x / (x * x ^ s) - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₃ : x / x / x ^ s - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
⊢ (x - (↑n : ℝ)) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
have rw₄ : 1 / x ^ s - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
Tactic: rw [sub_div, rpow_add_one (hv x hx).ne', mul_comm, ← div_div, div_self (hv x hx).ne',
        rpow_neg (hv x hx).le, rpow_neg (hv x hx).le, one_div, rpow_add_one (hv x hx).ne', mul_comm,
        div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
rw : x / x ^ (s + 1) - (↑n : ℝ) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₁ : x / (x ^ s * x) - (↑n : ℝ) / (x ^ s * x) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₂ : x / (x * x ^ s) - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₃ : x / x / x ^ s - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₄ : 1 / x ^ s - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
⊢ (x - (↑n : ℝ)) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
have rw₅ : 1 / x ^ s - (↑n : ℝ) / (x * x ^ s) = (x ^ s)⁻¹ - (↑n : ℝ) * x ^ (-(s + 1))
Tactic: rw [sub_div, rpow_add_one (hv x hx).ne', mul_comm, ← div_div, div_self (hv x hx).ne',
        rpow_neg (hv x hx).le, rpow_neg (hv x hx).le, one_div, rpow_add_one (hv x hx).ne', mul_comm,
        div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
rw : x / x ^ (s + 1) - (↑n : ℝ) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₁ : x / (x ^ s * x) - (↑n : ℝ) / (x ^ s * x) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₂ : x / (x * x ^ s) - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₃ : x / x / x ^ s - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₄ : 1 / x ^ s - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₅ : 1 / x ^ s - (↑n : ℝ) / (x * x ^ s) = (x ^ s)⁻¹ - (↑n : ℝ) * x ^ (-(s + 1))
⊢ (x - (↑n : ℝ)) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
have rw₆ : 1 / x ^ s - (↑n : ℝ) / (x * x ^ s) = (x ^ s)⁻¹ - (↑n : ℝ) * (x ^ (s + 1))⁻¹
Tactic: rw [sub_div, rpow_add_one (hv x hx).ne', mul_comm, ← div_div, div_self (hv x hx).ne',
        rpow_neg (hv x hx).le, rpow_neg (hv x hx).le, one_div, rpow_add_one (hv x hx).ne', mul_comm,
        div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
rw : x / x ^ (s + 1) - (↑n : ℝ) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₁ : x / (x ^ s * x) - (↑n : ℝ) / (x ^ s * x) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₂ : x / (x * x ^ s) - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₃ : x / x / x ^ s - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₄ : 1 / x ^ s - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₅ : 1 / x ^ s - (↑n : ℝ) / (x * x ^ s) = (x ^ s)⁻¹ - (↑n : ℝ) * x ^ (-(s + 1))
rw₆ : 1 / x ^ s - (↑n : ℝ) / (x * x ^ s) = (x ^ s)⁻¹ - (↑n : ℝ) * (x ^ (s + 1))⁻¹
⊢ (x - (↑n : ℝ)) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
have rw₇ : (x ^ s)⁻¹ - (↑n : ℝ) / (x * x ^ s) = (x ^ s)⁻¹ - (↑n : ℝ) * (x ^ (s + 1))⁻¹
Tactic: rw [sub_div, rpow_add_one (hv x hx).ne', mul_comm, ← div_div, div_self (hv x hx).ne',
        rpow_neg (hv x hx).le, rpow_neg (hv x hx).le, one_div, rpow_add_one (hv x hx).ne', mul_comm,
        div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
rw : x / x ^ (s + 1) - (↑n : ℝ) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₁ : x / (x ^ s * x) - (↑n : ℝ) / (x ^ s * x) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₂ : x / (x * x ^ s) - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₃ : x / x / x ^ s - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₄ : 1 / x ^ s - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₅ : 1 / x ^ s - (↑n : ℝ) / (x * x ^ s) = (x ^ s)⁻¹ - (↑n : ℝ) * x ^ (-(s + 1))
rw₆ : 1 / x ^ s - (↑n : ℝ) / (x * x ^ s) = (x ^ s)⁻¹ - (↑n : ℝ) * (x ^ (s + 1))⁻¹
rw₇ : (x ^ s)⁻¹ - (↑n : ℝ) / (x * x ^ s) = (x ^ s)⁻¹ - (↑n : ℝ) * (x ^ (s + 1))⁻¹
⊢ (x - (↑n : ℝ)) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
have rw₈ : (x ^ s)⁻¹ - (↑n : ℝ) / (x * x ^ s) = (x ^ s)⁻¹ - (↑n : ℝ) * (x ^ s * x)⁻¹
Tactic: rw [sub_div, rpow_add_one (hv x hx).ne', mul_comm, ← div_div, div_self (hv x hx).ne',
        rpow_neg (hv x hx).le, rpow_neg (hv x hx).le, one_div, rpow_add_one (hv x hx).ne', mul_comm,
        div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 1 < s
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
rw : x / x ^ (s + 1) - (↑n : ℝ) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₁ : x / (x ^ s * x) - (↑n : ℝ) / (x ^ s * x) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₂ : x / (x * x ^ s) - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₃ : x / x / x ^ s - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₄ : 1 / x ^ s - (↑n : ℝ) / (x * x ^ s) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
rw₅ : 1 / x ^ s - (↑n : ℝ) / (x * x ^ s) = (x ^ s)⁻¹ - (↑n : ℝ) * x ^ (-(s + 1))
rw₆ : 1 / x ^ s - (↑n : ℝ) / (x * x ^ s) = (x ^ s)⁻¹ - (↑n : ℝ) * (x ^ (s + 1))⁻¹
rw₇ : (x ^ s)⁻¹ - (↑n : ℝ) / (x * x ^ s) = (x ^ s)⁻¹ - (↑n : ℝ) * (x ^ (s + 1))⁻¹
rw₈ : (x ^ s)⁻¹ - (↑n : ℝ) / (x * x ^ s) = (x ^ s)⁻¹ - (↑n : ℝ) * (x ^ s * x)⁻¹
⊢ (x - (↑n : ℝ)) / x ^ (s + 1) = x ^ (-s) - (↑n : ℝ) * x ^ (-(s + 1))
have rw₉ : (x ^ s)⁻¹ - (↑n : ℝ) / (x ^ s * x) = (x ^ s)⁻¹ - (↑n : ℝ) * (x ^ s * x)⁻¹
Tactic: rw [sub_div, rpow_add_one (hv x hx).ne', mul_comm, ← div_div, div_self (hv x hx).ne',
        rpow_neg (hv x hx).le, rpow_neg (hv x hx).le, one_div, rpow_add_one (hv x hx).ne', mul_comm,
        div_eq_mul_inv]