awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
hf : HasDerivAt f (-log (↑π : ℂ) / 2 / (↑√π : ℂ)) 1
refine_2 :
  ∀ (this : HasDerivAt (𝕜 := ℂ) (Gamma ∘ fun (s : ℂ) ↦ s / 2) (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) * (1 / 2)) 1),
    HasDerivAt g (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1
refine_1 : HasDerivAt (fun (s : ℂ) ↦ s / 2) (1 / 2) 1
⊢ HasDerivAt g (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1

Tactic:
have := hasDerivAt_Gamma_one_half.comp 1 (?_ : HasDerivAt (fun s : ℂ ↦ s / 2) (1 / 2) 1)
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
hf : HasDerivAt f (-log (↑π : ℂ) / 2 / (↑√π : ℂ)) 1
this : HasDerivAt (𝕜 := ℂ) (Gamma ∘ fun (s : ℂ) ↦ s / 2) (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) * (1 / 2)) 1
refine_2 refine_2₁ refine_2₂ refine_2₃ :
  ∀ (this : HasDerivAt (𝕜 := ℂ) (Gamma ∘ fun (s : ℂ) ↦ s / 2) (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1),
    HasDerivAt g (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1
⊢ HasDerivAt g (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1

Tactic:
rwa [mul_one_div] at this

Premises used: mul_one_div
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
hf : HasDerivAt f (-log (↑π : ℂ) / 2 / (↑√π : ℂ)) 1
⊢ HasDerivAt (fun (s : ℂ) ↦ s / 2) (1 / 2) 1

Tactic:
(hasDerivAt_id _).div_const _

Premises used: HasDerivAt.div_const
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
hf : HasDerivAt f (-log (↑π : ℂ) / 2 / (↑√π : ℂ)) 1
⊢ HasDerivAt (fun (s : ℂ) ↦ s / 2) (1 / 2) 1

Tactic:
exact (hasDerivAt_id _).div_const _

Premises used: HasDerivAt.div_const
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
hf : HasDerivAt f (-log (↑π : ℂ) / 2 / (↑√π : ℂ)) 1
⊢ HasDerivAt g (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1

Tactic:
have hg : HasDerivAt g (-√π * (γ + 2 * log 2) / 2) 1 := by
    have := hasDerivAt_Gamma_one_half.comp 1 (?_ : HasDerivAt (fun s : ℂ ↦ s / 2) (1 / 2) 1)
    · rwa [mul_one_div] at this
    · exact (hasDerivAt_id _).div_const _
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
hf : HasDerivAt f (-log (↑π : ℂ) / 2 / (↑√π : ℂ)) 1
hg : HasDerivAt g (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1
⊢ HasDerivAt Gammaℝ (-((↑γ : ℂ) + log (4 * (↑π : ℂ))) / 2) 1

Tactic:
HasDerivAt.congr_deriv (hf.mul hg) ?_

Premises used: HasDerivAt.mul, HasDerivAt.congr_deriv
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
hf : HasDerivAt f (-log (↑π : ℂ) / 2 / (↑√π : ℂ)) 1
hg : HasDerivAt g (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1
refine :
  -log (↑π : ℂ) / 2 / (↑√π : ℂ) * Gamma (1 / 2) + f 1 * (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) =
    -((↑γ : ℂ) + log (4 * (↑π : ℂ))) / 2
⊢ HasDerivAt Gammaℝ (-((↑γ : ℂ) + log (4 * (↑π : ℂ))) / 2) 1

Tactic:
refine HasDerivAt.congr_deriv (hf.mul hg) ?_

Premises used: HasDerivAt.mul, HasDerivAt.congr_deriv
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
hf : HasDerivAt f (-log (↑π : ℂ) / 2 / (↑√π : ℂ)) 1
hg : HasDerivAt g (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1
simp :
  -log (↑π : ℂ) / 2 / (↑√π : ℂ) * Gamma (1 / 2) + (↑π : ℂ) ^ (-1 / 2) * (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) =
    -((↑γ : ℂ) + log (4 * (↑π : ℂ))) / 2
⊢ -log (↑π : ℂ) / 2 / (↑√π : ℂ) * Gamma (1 / 2) + f 1 * (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) =
    -((↑γ : ℂ) + log (4 * (↑π : ℂ))) / 2

Tactic:
simp only [f]
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
hf : HasDerivAt f (-log (↑π : ℂ) / 2 / (↑√π : ℂ)) 1
hg : HasDerivAt g (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1
⊢ HPow.hPow (α := ℝ) (β := ℕ) (↑2 : ℝ) 2 ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
hf : HasDerivAt f (-log (↑π : ℂ) / 2 / (↑√π : ℂ)) 1
hg : HasDerivAt g (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1
⊢ π ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
hf : HasDerivAt f (-log (↑π : ℂ) / 2 / (↑√π : ℂ)) 1
hg : HasDerivAt g (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1
⊢ 0 ≤ HPow.hPow (α := ℝ) (β := ℕ) 2 2 * π

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
hf : HasDerivAt f (-log (↑π : ℂ) / 2 / (↑√π : ℂ)) 1
hg : HasDerivAt g (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1
rw : -((↑γ : ℂ) + log (↑(HPow.hPow (α := ℝ) (β := ℕ) 2 2 * π) : ℂ)) / 2 = -((↑γ : ℂ) + log (4 * (↑π : ℂ))) / 2
⊢ -log (↑π : ℂ) / 2 / (↑√π : ℂ) * Gamma (1 / 2) + (↑π : ℂ) ^ (-1 / 2) * (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) =
    -((↑γ : ℂ) + log (4 * (↑π : ℂ))) / 2

Tactic:
rw [Gamma_one_half_eq, aux, div_mul_cancel₀ _ aux2, neg_div _ (1 : ℂ), cpow_neg, aux,
    mul_div_assoc, ← mul_assoc, mul_neg, inv_mul_cancel₀ aux2, neg_one_mul, ← neg_div,
    ← _root_.add_div, ← neg_add, add_comm, add_assoc, ← ofReal_log Real.pi_pos.le, ← ofReal_ofNat,
    ← ofReal_log zero_le_two,
    ← ofReal_mul, ← Nat.cast_ofNat (R := ℝ), ← Real.log_pow, ← ofReal_add,
    ← Real.log_mul (by positivity) (by positivity),
    Nat.cast_ofNat, ofReal_ofNat, ofReal_log (by positivity)]

Premises used: Nat.cast_ofNat, div_mul_cancel₀, neg_div, add_assoc, Complex.ofReal_log, mul_assoc, mul_div_assoc, neg_one_mul, neg_add, Complex.ofReal_add, Complex.cpow_neg, Real.pi_pos, LT.lt.le, add_comm, zero_le_two, Real.log_pow, Complex.ofReal_ofNat, OfNat.ofNat, inv_mul_cancel₀, Real.log_mul, Complex.Gamma_one_half_eq, Complex.ofReal_mul, mul_neg, add_div
-- Module: Mathlib.NumberTheory.Harmonic.GammaDeriv
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ (↑π : ℂ) ^ (-s / 2)
g : (s : ℂ) → ℂ := fun (s : ℂ) ↦ Gamma (s / 2)
aux : (↑π : ℂ) ^ (1 / 2) = (↑√π : ℂ)
aux2 : (↑√π : ℂ) ≠ 0
hf : HasDerivAt f (-log (↑π : ℂ) / 2 / (↑√π : ℂ)) 1
hg : HasDerivAt g (-(↑√π : ℂ) * ((↑γ : ℂ) + 2 * log 2) / 2) 1
⊢ -((↑γ : ℂ) + log (↑(HPow.hPow (α := ℝ) (β := ℕ) 2 2 * π) : ℂ)) / 2 = -((↑γ : ℂ) + log (4 * (↑π : ℂ))) / 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Harmonic.Int
Goal:
n : ℕ
Hn : n ≠ 0
⊢ (Finset.range n).Nonempty

Tactic:
rw [← Finset.nonempty_range_iff] at Hn

Premises used: Finset.nonempty_range_iff
-- Module: Mathlib.NumberTheory.Harmonic.Int
Goal:
n : ℕ
Hn : (Finset.range n).Nonempty
⊢ LT.lt (α := ℚ) 0 (∑ i ∈ Finset.range n, (↑(i + 1) : ℚ)⁻¹)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Harmonic.Int
Goal:
⊢ padicValRat 2 (harmonic 0) = -(↑(Nat.log 2 0) : ℤ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Harmonic.Int
Goal:
n : ℕ
ih : padicValRat 2 (harmonic n) = -(↑(Nat.log 2 n) : ℤ)
succ :
  ∀ (ih : padicValRat 2 (harmonic 0) = -(↑(Nat.log 2 0) : ℤ)),
    padicValRat 2 (harmonic (HAdd.hAdd (α := ℕ) 0 1)) = -(↑(Nat.log 2 (HAdd.hAdd (α := ℕ) 0 1)) : ℤ)
succ₁ : ∀ (hn : n ≠ 0), padicValRat 2 (harmonic (n + 1)) = -(↑(Nat.log 2 (n + 1)) : ℤ)
⊢ padicValRat 2 (harmonic (n + 1)) = -(↑(Nat.log 2 (n + 1)) : ℤ)

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Harmonic.Int
Goal:
ih : padicValRat 2 (harmonic 0) = -(↑(Nat.log 2 0) : ℤ)
⊢ padicValRat 2 (harmonic (HAdd.hAdd (α := ℕ) 0 1)) = -(↑(Nat.log 2 (HAdd.hAdd (α := ℕ) 0 1)) : ℤ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Harmonic.Int
Goal:
n : ℕ
ih : padicValRat 2 (harmonic n) = -(↑(Nat.log 2 n) : ℤ)
hn : n ≠ 0
succ : padicValRat 2 (harmonic n + (↑(n + 1) : ℚ)⁻¹) = -(↑(Nat.log 2 (n + 1)) : ℤ)
⊢ padicValRat 2 (harmonic (n + 1)) = -(↑(Nat.log 2 (n + 1)) : ℤ)

Tactic:
rw [harmonic_succ]

Premises used: harmonic_succ
-- Module: Mathlib.NumberTheory.Harmonic.Int
Goal:
n : ℕ
ih : padicValRat 2 (harmonic n) = -(↑(Nat.log 2 n) : ℤ)
hn : n ≠ 0
rw : ¬Nat.log 2 n = padicValNat 2 (n + 1)
⊢ padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1) : ℚ)⁻¹

Tactic:
rw [ih, padicValRat.inv, padicValRat.of_nat, Ne, neg_inj, Nat.cast_inj]

Premises used: Ne, Nat.cast_inj, padicValRat.of_nat, neg_inj, padicValRat.inv
-- Module: Mathlib.NumberTheory.Harmonic.Int
Goal:
n : ℕ
ih : padicValRat 2 (harmonic n) = -(↑(Nat.log 2 n) : ℤ)
hn : n ≠ 0
⊢ ¬Nat.log 2 n = padicValNat 2 (n + 1)

Tactic:
Nat.log_ne_padicValNat_succ hn

Premises used: Nat.log_ne_padicValNat_succ
-- Module: Mathlib.NumberTheory.Harmonic.Int
Goal:
n : ℕ
ih : padicValRat 2 (harmonic n) = -(↑(Nat.log 2 n) : ℤ)
hn : n ≠ 0
⊢ ¬Nat.log 2 n = padicValNat 2 (n + 1)

Tactic:
exact Nat.log_ne_padicValNat_succ hn

Premises used: Nat.log_ne_padicValNat_succ
-- Module: Mathlib.NumberTheory.Harmonic.Int
Goal:
n : ℕ
ih : padicValRat 2 (harmonic n) = -(↑(Nat.log 2 n) : ℤ)
hn : n ≠ 0
⊢ padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1) : ℚ)⁻¹

Tactic:
have key : padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1))⁻¹ := by
      rw [ih, padicValRat.inv, padicValRat.of_nat, Ne, neg_inj, Nat.cast_inj]
      exact Nat.log_ne_padicValNat_succ hn
-- Module: Mathlib.NumberTheory.Harmonic.Int
Goal:
n : ℕ
ih : padicValRat 2 (harmonic n) = -(↑(Nat.log 2 n) : ℤ)
hn : n ≠ 0
key : padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1) : ℚ)⁻¹
succ : max (Nat.log 2 n) (padicValNat 2 n.succ) = Nat.log 2 (n + 1)
⊢ padicValRat 2 (harmonic n + (↑(n + 1) : ℚ)⁻¹) = -(↑(Nat.log 2 (n + 1)) : ℤ)

Tactic:
rw [padicValRat.add_eq_min (harmonic_succ n ▸ (harmonic_pos n.succ_ne_zero).ne')
        (harmonic_pos hn).ne' (inv_ne_zero (Nat.cast_ne_zero.mpr n.succ_ne_zero)) key, ih,
        padicValRat.inv, padicValRat.of_nat, min_neg_neg, neg_inj, ← Nat.cast_max, Nat.cast_inj]

Premises used: Iff.mpr, Nat.cast_max, Nat.cast_inj, min_neg_neg, LT.lt.ne', harmonic_pos, Nat.succ_ne_zero, padicValRat.of_nat, neg_inj, inv_ne_zero, padicValRat.add_eq_min, padicValRat.inv, Nat.cast_ne_zero
-- Module: Mathlib.NumberTheory.Harmonic.Int
Goal:
n : ℕ
ih : padicValRat 2 (harmonic n) = -(↑(Nat.log 2 n) : ℤ)
hn : n ≠ 0
key : padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1) : ℚ)⁻¹
⊢ max (Nat.log 2 n) (padicValNat 2 n.succ) = Nat.log 2 (n + 1)

Tactic:
Nat.max_log_padicValNat_succ_eq_log_succ n

Premises used: Nat.max_log_padicValNat_succ_eq_log_succ
-- Module: Mathlib.NumberTheory.Harmonic.Int
Goal:
n : ℕ
ih : padicValRat 2 (harmonic n) = -(↑(Nat.log 2 n) : ℤ)
hn : n ≠ 0
key : padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1) : ℚ)⁻¹
⊢ max (Nat.log 2 n) (padicValNat 2 n.succ) = Nat.log 2 (n + 1)

Tactic:
exact Nat.max_log_padicValNat_succ_eq_log_succ n

Premises used: Nat.max_log_padicValNat_succ_eq_log_succ
-- Module: Mathlib.NumberTheory.Harmonic.Int
Goal:
n : ℕ
zero : padicValRat 2 (harmonic 0) = -(↑(Nat.log 2 0) : ℤ)
succ :
  ∀ (n : ℕ) (ih : padicValRat 2 (harmonic n) = -(↑(Nat.log 2 n) : ℤ)),
    padicValRat 2 (harmonic (n + 1)) = -(↑(Nat.log 2 (n + 1)) : ℤ)
⊢ padicValRat 2 (harmonic n) = -(↑(Nat.log 2 n) : ℤ)

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    rcases eq_or_ne n 0 with rfl | hn
    · simp
    rw [harmonic_succ]
    have key : padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1))⁻¹ := by
      rw [ih, padicValRat.inv, padicValRat.of_nat, Ne, neg_inj, Nat.cast_inj]
      exact Nat.log_ne_padicValNat_succ hn
    rw [padicValRat.add_eq_min (harmonic_succ n ▸ (harmonic_pos n.succ_ne_zero).ne')
        (harmonic_pos hn).ne' (inv_ne_zero (Nat.cast_ne_zero.mpr n.succ_ne_zero)) key, ih,
        padicValRat.inv, padicValRat.of_nat, min_neg_neg, neg_inj, ← Nat.cast_max, Nat.cast_inj]
    exact Nat.max_log_padicValNat_succ_eq_log_succ n

Premises used: Nat.max_log_padicValNat_succ_eq_log_succ, Nat.cast_max, Nat.cast_inj, min_neg_neg, harmonic_succ, padicValRat.of_nat, neg_inj, eq_or_ne, padicValRat.inv, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Harmonic.Int
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)
rw₇ 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)

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]

Premises used: zpow_natCast, Nat.cast_ofNat, Padic.eq_padicNorm, neg_neg, padicNorm.eq_zpow_of_nonzero, padicValRat_two_harmonic, LT.lt.ne', harmonic_pos, Rat.cast_natCast, Rat.cast_pow
-- Module: Mathlib.NumberTheory.Harmonic.Int
Goal:
n : ℕ
h : 2 ≤ n
apply : 1 < padicNorm 2 (harmonic n)
⊢ ¬(harmonic n).isInt = true

Tactic:
apply padicNorm.not_int_of_not_padic_int 2

Premises used: padicNorm.not_int_of_not_padic_int, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Harmonic.Int
Goal:
n : ℕ
h : 2 ≤ n
rw : 1 < HPow.hPow (α := ℚ) (↑2 : ℚ) (Nat.log 2 n)
⊢ 1 < padicNorm 2 (harmonic n)

Tactic:
rw [padicNorm.eq_zpow_of_nonzero (harmonic_pos (ne_zero_of_lt h)).ne',
      padicValRat_two_harmonic, neg_neg, zpow_natCast]

Premises used: zpow_natCast, ne_zero_of_lt, neg_neg, padicNorm.eq_zpow_of_nonzero, padicValRat_two_harmonic, LT.lt.ne', harmonic_pos
-- Module: Mathlib.NumberTheory.Harmonic.Int
Goal:
n : ℕ
h : 2 ≤ n
⊢ 1 < HPow.hPow (α := ℚ) (↑2 : ℚ) (Nat.log 2 n)

Tactic:
one_lt_pow₀ one_lt_two (Nat.log_pos one_lt_two h).ne'

Premises used: Nat.log_pos, LT.lt.ne', one_lt_two, one_lt_pow₀
-- Module: Mathlib.NumberTheory.Harmonic.Int
Goal:
n : ℕ
h : 2 ≤ n
⊢ 1 < HPow.hPow (α := ℚ) (↑2 : ℚ) (Nat.log 2 n)

Tactic:
exact one_lt_pow₀ one_lt_two (Nat.log_pos one_lt_two h).ne'

Premises used: Nat.log_pos, LT.lt.ne', one_lt_two, one_lt_pow₀
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
⊢ (↑n : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
rw :
  LE.le (α := ℝ) 0
    (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)))
      fun (x : ℝ) ↦ (x - (↑n : ℝ)) / x ^ (s + 1))
⊢ 0 ≤ term n s

Tactic:
rw [term, intervalIntegral.integral_of_le (by simp)]

Premises used: intervalIntegral.integral_of_le, ZetaAsymptotics.term
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
⊢ LE.le (α := ℝ) 0
    (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)))
      fun (x : ℝ) ↦ (x - (↑n : ℝ)) / x ^ (s + 1))

Tactic:
setIntegral_nonneg measurableSet_Ioc (fun x hx ↦ ?_)

Premises used: MeasureTheory.setIntegral_nonneg, measurableSet_Ioc
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s : ℝ
refine : ∀ (x : ℝ) (hx : x ∈ Ioc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)), 0 ≤ (x - (↑n : ℝ)) / x ^ (s + 1)
⊢ LE.le (α := ℝ) 0
    (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)))
      fun (x : ℝ) ↦ (x - (↑n : ℝ)) / x ^ (s + 1))

Tactic:
refine setIntegral_nonneg measurableSet_Ioc (fun x hx ↦ ?_)

Premises used: MeasureTheory.setIntegral_nonneg, measurableSet_Ioc
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s x : ℝ
hx : x ∈ Ioc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ 0 ≤ (x - (↑n : ℝ)) / x ^ (s + 1)

Tactic:
div_nonneg ?_ (rpow_nonneg ?_ _)

Premises used: div_nonneg, Real.rpow_nonneg
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s x : ℝ
hx : x ∈ Ioc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
refine_1 : 0 ≤ x - (↑n : ℝ)
refine_2 : 0 ≤ x
⊢ 0 ≤ (x - (↑n : ℝ)) / x ^ (s + 1)

Tactic:
refine div_nonneg ?_ (rpow_nonneg ?_ _)

Premises used: div_nonneg, Real.rpow_nonneg
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s x : ℝ
hx : x ∈ Ioc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
linarith : x - (↑n : ℝ) < 0 → x - (↑n : ℝ) - 0 + ((↑n : ℝ) - x) = 0
⊢ 0 ≤ x - (↑n : ℝ)

Tactic:
linarith [hx.1]

Premises used: And.left
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
s x : ℝ
hx : x ∈ Ioc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
linarith : x < 0 → HSub.hSub (α := ℝ) 0 (↑n : ℝ) + (x - 0) + ((↑n : ℝ) - x) = 0
⊢ 0 ≤ x

Tactic:
linarith [hx.1]

Premises used: And.left
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
linarith : HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 < (↑n : ℝ) → -1 + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 - (↑n : ℝ)) = 0
⊢ (↑n : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
rw :
  IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ (x - (↑n : ℝ)) / x ^ (s + 1))
    (Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) volume
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ (x - (↑n : ℝ)) / x ^ (s + 1)) volume (↑n : ℝ)
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
rw [intervalIntegrable_iff_integrableOn_Icc_of_le (by linarith)]

Premises used: intervalIntegrable_iff_integrableOn_Icc_of_le
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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

Tactic:
(continuousOn_of_forall_continuousAt fun x hx ↦ ContinuousAt.div ?_ ?_ ?_).integrableOn_Icc

Premises used: continuousOn_of_forall_continuousAt, ContinuousOn.integrableOn_Icc, ContinuousAt.div
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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
refine_3 : ∀ (x : ℝ) (hx : x ∈ Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)), x ^ (s + 1) ≠ 0
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ (x - (↑n : ℝ)) / x ^ (s + 1))
    (Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) volume

Tactic:
refine (continuousOn_of_forall_continuousAt fun x hx ↦ ContinuousAt.div ?_ ?_ ?_).integrableOn_Icc

Premises used: continuousOn_of_forall_continuousAt, ContinuousOn.integrableOn_Icc, ContinuousAt.div
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x - (↑n : ℝ)) x

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
linarith : s + 1 < 0 → -1 + (0 - s) + (s + 1 - 0) = 0
⊢ 0 ≤ s + 1

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ x ^ (s + 1)) x

Tactic:
apply continuousAt_id.rpow_const (Or.inr <| by linarith)

Premises used: ContinuousAt.rpow_const, continuousAt_id, Or.inr
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ x ^ (s + 1) ≠ 0

Tactic:
(rpow_pos_of_pos ((Nat.cast_pos.mpr hn).trans_le hx.1) _).ne'

Premises used: Iff.mpr, Real.rpow_pos_of_pos, Nat.cast_pos, LT.lt.ne', And.left, LT.lt.trans_le
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
s : ℝ
hs : 0 < s
x : ℝ
hx : x ∈ Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ x ^ (s + 1) ≠ 0

Tactic:
exact (rpow_pos_of_pos ((Nat.cast_pos.mpr hn).trans_le hx.1) _).ne'

Premises used: Iff.mpr, Real.rpow_pos_of_pos, Nat.cast_pos, LT.lt.ne', And.left, LT.lt.trans_le
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
x : ℝ
hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ (↑n : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
simp only [le_add_iff_nonneg_right, zero_le_one]

Premises used: le_add_iff_nonneg_right, zero_le_one
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
x : ℝ
hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ 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

Premises used: Set.uIcc_of_le
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
x : ℝ
hx : x ∈ Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ 0 < x

Tactic:
(Nat.cast_pos.mpr hn).trans_le hx.1

Premises used: Iff.mpr, Nat.cast_pos, And.left, LT.lt.trans_le
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
x : ℝ
hx : x ∈ Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ 0 < x

Tactic:
exact (Nat.cast_pos.mpr hn).trans_le hx.1

Premises used: Iff.mpr, Nat.cast_pos, And.left, LT.lt.trans_le
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
⊢ ∀ 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
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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)
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

Tactic:
simp_rw [term, one_add_one_eq_two, ← Nat.cast_two (R := ℝ), rpow_natCast]

Premises used: one_add_one_eq_two, ZetaAsymptotics.term, Nat.cast_two, Real.rpow_natCast
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
n : ℕ
hn : 0 < n
hv : ∀ x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1), 0 < x
x : ℝ
hx : x ∈ uIcc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ (x - (↑n : ℝ)) / HPow.hPow (β := ℕ) x 2 = 1 / x - (↑n : ℝ) / HPow.hPow (β := ℕ) x 2

Tactic:
field