awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Int (goal)
Goal:
n : ℕ
hn : n ≠ 0
rw : (↑(padicNorm 2 (harmonic n)) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
rw₁ : (↑(HPow.hPow (α := ℚ) (↑2 : ℚ) (-padicValRat 2 (harmonic n))) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
⊢ norm (E := ℚ_[2]) (↑(harmonic n) : ℚ_[2]) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
have rw₂ : (↑(HPow.hPow (α := ℚ) (β := ℤ) (↑2 : ℚ) (- -(↑(Nat.log 2 n) : ℤ))) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
Tactic: rw [Padic.eq_padicNorm, padicNorm.eq_zpow_of_nonzero (harmonic_pos hn).ne',
    padicValRat_two_harmonic, neg_neg, zpow_natCast, Rat.cast_pow, Rat.cast_natCast, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Int (goal)
Goal:
n : ℕ
hn : n ≠ 0
rw : (↑(padicNorm 2 (harmonic n)) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
rw₁ : (↑(HPow.hPow (α := ℚ) (↑2 : ℚ) (-padicValRat 2 (harmonic n))) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
rw₂ : (↑(HPow.hPow (α := ℚ) (β := ℤ) (↑2 : ℚ) (- -(↑(Nat.log 2 n) : ℤ))) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
⊢ norm (E := ℚ_[2]) (↑(harmonic n) : ℚ_[2]) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
have rw₃ : (↑(HPow.hPow (α := ℚ) (β := ℤ) (↑2 : ℚ) (↑(Nat.log 2 n) : ℤ)) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
Tactic: rw [Padic.eq_padicNorm, padicNorm.eq_zpow_of_nonzero (harmonic_pos hn).ne',
    padicValRat_two_harmonic, neg_neg, zpow_natCast, Rat.cast_pow, Rat.cast_natCast, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Int (goal)
Goal:
n : ℕ
hn : n ≠ 0
rw : (↑(padicNorm 2 (harmonic n)) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
rw₁ : (↑(HPow.hPow (α := ℚ) (↑2 : ℚ) (-padicValRat 2 (harmonic n))) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
rw₂ : (↑(HPow.hPow (α := ℚ) (β := ℤ) (↑2 : ℚ) (- -(↑(Nat.log 2 n) : ℤ))) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
rw₃ : (↑(HPow.hPow (α := ℚ) (β := ℤ) (↑2 : ℚ) (↑(Nat.log 2 n) : ℤ)) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
⊢ norm (E := ℚ_[2]) (↑(harmonic n) : ℚ_[2]) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
have rw₄ : (↑(HPow.hPow (α := ℚ) (↑2 : ℚ) (Nat.log 2 n)) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
Tactic: rw [Padic.eq_padicNorm, padicNorm.eq_zpow_of_nonzero (harmonic_pos hn).ne',
    padicValRat_two_harmonic, neg_neg, zpow_natCast, Rat.cast_pow, Rat.cast_natCast, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Int (goal)
Goal:
n : ℕ
hn : n ≠ 0
rw : (↑(padicNorm 2 (harmonic n)) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
rw₁ : (↑(HPow.hPow (α := ℚ) (↑2 : ℚ) (-padicValRat 2 (harmonic n))) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
rw₂ : (↑(HPow.hPow (α := ℚ) (β := ℤ) (↑2 : ℚ) (- -(↑(Nat.log 2 n) : ℤ))) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
rw₃ : (↑(HPow.hPow (α := ℚ) (β := ℤ) (↑2 : ℚ) (↑(Nat.log 2 n) : ℤ)) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
rw₄ : (↑(HPow.hPow (α := ℚ) (↑2 : ℚ) (Nat.log 2 n)) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
⊢ norm (E := ℚ_[2]) (↑(harmonic n) : ℚ_[2]) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
have rw₅ : HPow.hPow (α := ℝ) (↑(↑2 : ℚ) : ℝ) (Nat.log 2 n) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
Tactic: rw [Padic.eq_padicNorm, padicNorm.eq_zpow_of_nonzero (harmonic_pos hn).ne',
    padicValRat_two_harmonic, neg_neg, zpow_natCast, Rat.cast_pow, Rat.cast_natCast, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Int (goal)
Goal:
n : ℕ
hn : n ≠ 0
rw : (↑(padicNorm 2 (harmonic n)) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
rw₁ : (↑(HPow.hPow (α := ℚ) (↑2 : ℚ) (-padicValRat 2 (harmonic n))) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
rw₂ : (↑(HPow.hPow (α := ℚ) (β := ℤ) (↑2 : ℚ) (- -(↑(Nat.log 2 n) : ℤ))) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
rw₃ : (↑(HPow.hPow (α := ℚ) (β := ℤ) (↑2 : ℚ) (↑(Nat.log 2 n) : ℤ)) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
rw₄ : (↑(HPow.hPow (α := ℚ) (↑2 : ℚ) (Nat.log 2 n)) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
rw₅ : HPow.hPow (α := ℝ) (↑(↑2 : ℚ) : ℝ) (Nat.log 2 n) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
⊢ norm (E := ℚ_[2]) (↑(harmonic n) : ℚ_[2]) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
have rw₆ : HPow.hPow (α := ℝ) (↑2 : ℝ) (Nat.log 2 n) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
Tactic: rw [Padic.eq_padicNorm, padicNorm.eq_zpow_of_nonzero (harmonic_pos hn).ne',
    padicValRat_two_harmonic, neg_neg, zpow_natCast, Rat.cast_pow, Rat.cast_natCast, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Int (goal)
Goal:
n : ℕ
hn : n ≠ 0
rw : (↑(padicNorm 2 (harmonic n)) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
rw₁ : (↑(HPow.hPow (α := ℚ) (↑2 : ℚ) (-padicValRat 2 (harmonic n))) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
rw₂ : (↑(HPow.hPow (α := ℚ) (β := ℤ) (↑2 : ℚ) (- -(↑(Nat.log 2 n) : ℤ))) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
rw₃ : (↑(HPow.hPow (α := ℚ) (β := ℤ) (↑2 : ℚ) (↑(Nat.log 2 n) : ℤ)) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
rw₄ : (↑(HPow.hPow (α := ℚ) (↑2 : ℚ) (Nat.log 2 n)) : ℝ) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
rw₅ : HPow.hPow (α := ℝ) (↑(↑2 : ℚ) : ℝ) (Nat.log 2 n) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
rw₆ : HPow.hPow (α := ℝ) (↑2 : ℝ) (Nat.log 2 n) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
⊢ norm (E := ℚ_[2]) (↑(harmonic n) : ℚ_[2]) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
have rw₇ : HPow.hPow (α := ℝ) 2 (Nat.log 2 n) = HPow.hPow (α := ℝ) 2 (Nat.log 2 n)
Tactic: rw [Padic.eq_padicNorm, padicNorm.eq_zpow_of_nonzero (harmonic_pos hn).ne',
    padicValRat_two_harmonic, neg_neg, zpow_natCast, Rat.cast_pow, Rat.cast_natCast, Nat.cast_ofNat]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Int (goal)
Goal:
n : ℕ
h : 2 ≤ n
⊢ ¬(harmonic n).isInt = true
have apply : 1 < padicNorm 2 (harmonic n)
Tactic: apply padicNorm.not_int_of_not_padic_int 2
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.Int (goal)
Goal:
n : ℕ
h : 2 ≤ n
⊢ 1 < padicNorm 2 (harmonic n)
have rw : 1 < HPow.hPow (α := ℚ) (↑2 : ℚ) (Nat.log 2 n)
Tactic: rw [padicNorm.eq_zpow_of_nonzero (harmonic_pos (ne_zero_of_lt h)).ne',
      padicValRat_two_harmonic, neg_neg, zpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
⊢ 0 ≤ term n s
have rw : LE.le (α := ℝ) 0
  (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)))
    fun (x : ℝ) ↦ (x - (↑n : ℝ)) / x ^ (s + 1))
Tactic: rw [term, intervalIntegral.integral_of_le (by simp)]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s : ℝ
⊢ LE.le (α := ℝ) 0
    (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)))
      fun (x : ℝ) ↦ (x - (↑n : ℝ)) / x ^ (s + 1))
have refine : ∀ (x : ℝ) (hx : x ∈ Ioc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)), 0 ≤ (x - (↑n : ℝ)) / x ^ (s + 1)
Tactic: refine setIntegral_nonneg measurableSet_Ioc (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s x : ℝ
hx : x ∈ Ioc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ 0 ≤ (x - (↑n : ℝ)) / x ^ (s + 1)
have refine_1 : 0 ≤ x - (↑n : ℝ)
Tactic: refine div_nonneg ?_ (rpow_nonneg ?_ _)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s x : ℝ
hx : x ∈ Ioc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
refine_1 : 0 ≤ x - (↑n : ℝ)
⊢ 0 ≤ (x - (↑n : ℝ)) / x ^ (s + 1)
have refine_2 : 0 ≤ x
Tactic: refine div_nonneg ?_ (rpow_nonneg ?_ _)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s x : ℝ
hx : x ∈ Ioc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ 0 ≤ x - (↑n : ℝ)
have linarith : x - (↑n : ℝ) < 0 → x - (↑n : ℝ) - 0 + ((↑n : ℝ) - x) = 0
Tactic: linarith [hx.1]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
s x : ℝ
hx : x ∈ Ioc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ 0 ≤ x
have linarith : x < 0 → HSub.hSub (α := ℝ) 0 (↑n : ℝ) + (x - 0) + ((↑n : ℝ) - x) = 0
Tactic: linarith [hx.1]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
⊢ (↑n : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
have linarith : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < (↑n : ℝ) → -1 + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - (↑n : ℝ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - (↑n : ℝ)) / x ^ (s + 1)) volume (↑n : ℝ)
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have rw : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ (x - (↑n : ℝ)) / x ^ (s + 1))
  (Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) volume
Tactic: rw [intervalIntegrable_iff_integrableOn_Icc_of_le (by linarith)]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ (x - (↑n : ℝ)) / x ^ (s + 1))
    (Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) volume
have refine_1 : ∀ (x : ℝ) (hx : x ∈ Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x - (↑n : ℝ)) x
Tactic: refine (continuousOn_of_forall_continuousAt fun x hx ↦ ContinuousAt.div ?_ ?_ ?_).integrableOn_Icc
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
refine_1 :
  ∀ (x : ℝ) (hx : x ∈ Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)),
    ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x - (↑n : ℝ)) x
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ (x - (↑n : ℝ)) / x ^ (s + 1))
    (Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) volume
have refine_2 : ∀ (x : ℝ) (hx : x ∈ Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ (s + 1)) x
Tactic: refine (continuousOn_of_forall_continuousAt fun x hx ↦ ContinuousAt.div ?_ ?_ ?_).integrableOn_Icc
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
refine_1 :
  ∀ (x : ℝ) (hx : x ∈ Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)),
    ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x - (↑n : ℝ)) x
refine_2 :
  ∀ (x : ℝ) (hx : x ∈ Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ (s + 1)) x
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ (x - (↑n : ℝ)) / x ^ (s + 1))
    (Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) volume
have refine_3 : ∀ (x : ℝ) (hx : x ∈ Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)), x ^ (s + 1) ≠ 0
Tactic: refine (continuousOn_of_forall_continuousAt fun x hx ↦ ContinuousAt.div ?_ ?_ ?_).integrableOn_Icc
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ 0 ≤ s + 1
have linarith : s + 1 < 0 → -1 + (0 - s) + (s + 1 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (hypothesis)
Goal:
n : ℕ
hn : 0 < n
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
⊢ term n 1 = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
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
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ term n 1 = ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / HPow.hPow (β := ℕ) x 2
have simp_rw : Eq (α := ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1)
  (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / HPow.hPow (β := ℕ) x 2)
Tactic: simp_rw [term, one_add_one_eq_two, ← Nat.cast_two (R := ℝ), rpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
simp_rw :
  Eq (α := ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1)
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / HPow.hPow (β := ℕ) x 2)
⊢ term n 1 = ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / HPow.hPow (β := ℕ) x 2
have simp_rw₁ : Eq (α := ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / HPow.hPow (β := ℝ) x 2)
  (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / HPow.hPow (β := ℕ) x 2)
Tactic: simp_rw [term, one_add_one_eq_two, ← Nat.cast_two (R := ℝ), rpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
simp_rw :
  Eq (α := ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / x ^ HAdd.hAdd (α := ℝ) 1 1)
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / HPow.hPow (β := ℕ) x 2)
simp_rw₁ :
  Eq (α := ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / HPow.hPow (β := ℝ) x 2)
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / HPow.hPow (β := ℕ) x 2)
⊢ term n 1 = ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / HPow.hPow (β := ℕ) x 2
have simp_rw₂ : Eq (α := ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / HPow.hPow (β := ℝ) x (↑2 : ℝ))
  (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (x - (↑n : ℝ)) / HPow.hPow (β := ℕ) x 2)
Tactic: simp_rw [term, one_add_one_eq_two, ← Nat.cast_two (R := ℝ), rpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x - (↑n : ℝ) / HPow.hPow (β := ℕ) x 2 =
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2)
have simp_rw : ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x - (↑n : ℝ) * (1 / HPow.hPow (β := ℕ) x 2) =
  (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x) -
    HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2)
Tactic: simp_rw [← mul_one_div (n : ℝ)]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x - (↑n : ℝ) * (1 / HPow.hPow (β := ℕ) x 2) =
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2)
have rw : HSub.hSub (α := ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x)
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (↑n : ℝ) * (1 / HPow.hPow (β := ℕ) x 2)) =
  (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x) -
    HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2)
Tactic: rw [intervalIntegral.integral_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
rw :
  HSub.hSub (α := ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x)
      (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (↑n : ℝ) * (1 / HPow.hPow (β := ℕ) x 2)) =
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2)
⊢ ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x - (↑n : ℝ) * (1 / HPow.hPow (β := ℕ) x 2) =
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2)
have hf : IntervalIntegrable (HDiv.hDiv (α := ℝ) 1) volume (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: rw [intervalIntegral.integral_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
rw :
  HSub.hSub (α := ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x)
      (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, (↑n : ℝ) * (1 / HPow.hPow (β := ℕ) x 2)) =
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2)
hf : IntervalIntegrable (HDiv.hDiv (α := ℝ) 1) volume (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x - (↑n : ℝ) * (1 / HPow.hPow (β := ℕ) x 2) =
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2)
have hg : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (↑n : ℝ) * (1 / HPow.hPow (β := ℕ) x 2)) volume (↑n : ℝ)
  (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: rw [intervalIntegral.integral_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2) =
    log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2)
have e_a : ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ)
have e_a : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≠ 0
Tactic: rw [integral_one_div_of_pos, log_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
e_a : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≠ 0
⊢ ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ)
have e_a₁ : Ne (α := ℝ) (↑n : ℝ) 0
Tactic: rw [integral_one_div_of_pos, log_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
e_a : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≠ 0
e_a₁ : Ne (α := ℝ) (↑n : ℝ) 0
⊢ ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ)
have e_a₂ : LT.lt (α := ℝ) 0 (↑n : ℝ)
Tactic: rw [integral_one_div_of_pos, log_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
e_a : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≠ 0
e_a₁ : Ne (α := ℝ) (↑n : ℝ) 0
e_a₂ : LT.lt (α := ℝ) 0 (↑n : ℝ)
⊢ ∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / x = log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ)
have e_a₃ : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: rw [integral_one_div_of_pos, log_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2) =
    log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, HPow.hPow (β := ℝ) x (-2))
have e_a : Eq (α := ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2)
  (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, HPow.hPow (β := ℝ) x (-2))
Tactic: congr 2
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ Eq (α := ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, 1 / HPow.hPow (β := ℕ) x 2)
    (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, HPow.hPow (β := ℝ) x (-2))
have e_a : ∀ (x : ℝ) (hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)),
  1 / HPow.hPow (β := ℕ) x 2 = HPow.hPow (β := ℝ) x (-2)
Tactic: refine intervalIntegral.integral_congr (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ 1 / HPow.hPow (β := ℕ) x 2 = HPow.hPow (β := ℝ) x (-2)
have e_a : 0 ≤ x
Tactic: rw [rpow_neg, one_div, ← Nat.cast_two (R := ℝ), rpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
⊢ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, HPow.hPow (β := ℝ) x (-2)) =
    log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      (↑n : ℝ) * (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have rw : log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
    (↑n : ℝ) *
      ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ HAdd.hAdd (α := ℝ) (-2) 1 -
          HPow.hPow (α := ℝ) (↑n : ℝ) (HAdd.hAdd (α := ℝ) (-2) 1)) /
        HAdd.hAdd (α := ℝ) (-2) 1) =
  log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
    (↑n : ℝ) * (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: rw [integral_rpow]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
rw :
  log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      (↑n : ℝ) *
        ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ HAdd.hAdd (α := ℝ) (-2) 1 -
            HPow.hPow (α := ℝ) (↑n : ℝ) (HAdd.hAdd (α := ℝ) (-2) 1)) /
          HAdd.hAdd (α := ℝ) (-2) 1) =
    log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      (↑n : ℝ) * (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : ℝ) in (↑n : ℝ)..HAdd.hAdd (α := ℝ) (↑n : ℝ) 1, HPow.hPow (β := ℝ) x (-2)) =
    log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - log (↑n : ℝ) -
      (↑n : ℝ) * (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) - 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
have rw₁ : LT.lt (α := ℝ) (-1) (-2) ∨ Ne (α := ℝ) (-2) (-1) ∧ 0 ∉ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: rw [integral_rpow]