awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
s : ℂ
hs : Membership.mem («γ» := Set ℂ) {1}ᶜ s
h : ∀ (hs : s ≠ 1), s - 1 ≠ 0
⊢ s - 1 ≠ 0
have h₁ : ∀ (hs : s - 1 ≠ 0), s - 1 ≠ 0
Tactic: rwa [mem_compl_singleton_iff, ← sub_ne_zero] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
⊢ Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] 1) (fun (z : ℂ) ↦ f z - f 1) fun (z : ℂ) ↦ (z - 1)⁻¹
have refine_2 : ∀ᶠ (x : ℂ) in 𝓝[≠] 1, (x - 1)⁻¹ = 0 → f x - f 1 = 0
Tactic: refine Asymptotics.isLittleO_of_tendsto' ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
refine_2 : ∀ᶠ (x : ℂ) in 𝓝[≠] 1, (x - 1)⁻¹ = 0 → f x - f 1 = 0
⊢ Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] 1) (fun (z : ℂ) ↦ f z - f 1) fun (z : ℂ) ↦ (z - 1)⁻¹
have refine_2₁ : Tendsto (β := ℂ) (fun (x : ℂ) ↦ (f x - f 1) / (x - 1)⁻¹) (𝓝[≠] 1) (𝓝 0)
Tactic: refine Asymptotics.isLittleO_of_tendsto' ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
⊢ ∀ᶠ (x : ℂ) in 𝓝[≠] 1, (x - 1)⁻¹ = 0 → f x - f 1 = 0
have h : ∀ (t : ℂ) (ht : Membership.mem («γ» := Set ℂ) {1}ᶜ t) (ht' : (t - 1)⁻¹ = 0), f t - f 1 = 0
Tactic: filter_upwards [self_mem_nhdsWithin] with t ht ht'
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (hypothesis)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
t : ℂ
ht : Membership.mem («γ» := Set ℂ) {1}ᶜ t
ht' : (t - 1)⁻¹ = 0
⊢ f t - f 1 = 0
have ht'₁ : t = 1
Tactic: rw [inv_eq_zero, sub_eq_zero] at ht'
Cleared hypotheses: ht'
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
⊢ Tendsto (β := ℂ) (fun (x : ℂ) ↦ (f x - f 1) / (x - 1)⁻¹) (𝓝[≠] 1) (𝓝 0)
have refine_2 : Tendsto (fun (x : ℂ) ↦ f x * (x - 1) - f 1 * (x - 1)) (𝓝[≠] 1)
  (𝓝 (HSub.hSub (α := ℂ) 1 1 - f 1 * HSub.hSub (α := ℂ) 1 1))
Tactic: simp_rw [div_eq_mul_inv, inv_inv, sub_mul,
        (by ring_nf : 𝓝 (0 : ℂ) = 𝓝 ((1 - 1) - f 1 * (1 - 1)))]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun (x : ℂ) ↦ f x * (x - 1) - f 1 * (x - 1)) (𝓝[≠] 1)
    (𝓝 (HSub.hSub (α := ℂ) 1 1 - f 1 * HSub.hSub (α := ℂ) 1 1))
have refine_2 : Tendsto (fun (x : ℂ) ↦ f x * (x - 1)) (𝓝[≠] 1) (𝓝 (HSub.hSub (α := ℂ) 1 1))
Tactic: apply Tendsto.sub
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
refine_2 : Tendsto (fun (x : ℂ) ↦ f x * (x - 1)) (𝓝[≠] 1) (𝓝 (HSub.hSub (α := ℂ) 1 1))
⊢ Tendsto (fun (x : ℂ) ↦ f x * (x - 1) - f 1 * (x - 1)) (𝓝[≠] 1)
    (𝓝 (HSub.hSub (α := ℂ) 1 1 - f 1 * HSub.hSub (α := ℂ) 1 1))
have refine_2₁ : Tendsto (fun (x : ℂ) ↦ f 1 * (x - 1)) (𝓝[≠] 1) (𝓝 (f 1 * HSub.hSub (α := ℂ) 1 1))
Tactic: apply Tendsto.sub
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun (x : ℂ) ↦ f x * (x - 1)) (𝓝[≠] 1) (𝓝 (HSub.hSub (α := ℂ) 1 1))
have refine_2 : Tendsto (fun (x : ℂ) ↦ (x - 1) * riemannZeta x - (x - 1) * (1 / (x - 1))) (𝓝[≠] 1) (𝓝 (HSub.hSub (α := ℂ) 1 1))
Tactic: simp_rw [mul_comm (f _), f, mul_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun (x : ℂ) ↦ (x - 1) * riemannZeta x - (x - 1) * (1 / (x - 1))) (𝓝[≠] 1) (𝓝 (HSub.hSub (α := ℂ) 1 1))
have refine_2 : Tendsto (β := ℂ) (fun (x : ℂ) ↦ (x - 1) * (1 / (x - 1))) (𝓝[≠] 1) (𝓝 1)
Tactic: apply riemannZeta_residue_one.sub
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
⊢ Tendsto (β := ℂ) (fun (x : ℂ) ↦ (x - 1) * (1 / (x - 1))) (𝓝[≠] 1) (𝓝 1)
have refine_2 : EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (x : ℂ) ↦ 1) fun (x : ℂ) ↦ (x - 1) * (1 / (x - 1))
Tactic: refine Tendsto.congr' ?_ (tendsto_const_nhds.mono_left nhdsWithin_le_nhds)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
⊢ EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (x : ℂ) ↦ 1) fun (x : ℂ) ↦ (x - 1) * (1 / (x - 1))
have h : ∀ (x : ℂ) (hx : Membership.mem («γ» := Set ℂ) {1}ᶜ x), 1 = (x - 1) * (1 / (x - 1))
Tactic: filter_upwards [self_mem_nhdsWithin] with x hx
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (hypothesis)
Goal:
⊢ Tendsto (fun (s : ℂ) ↦ 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1)
    (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
have h : HasDerivAt Gammaℝ (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2) 1
Tactic: have h := hasDerivAt_Gammaℝ_one
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (hypothesis)
Goal:
h : HasDerivAt Gammaℝ (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2) 1
⊢ Tendsto (fun (s : ℂ) ↦ 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1)
    (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
have h₁ : Tendsto (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
Tactic: rw [hasDerivAt_iff_tendsto_slope, slope_fun_def_field, Gammaℝ_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (hypothesis)
Goal:
h : Tendsto (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
⊢ Tendsto (fun (s : ℂ) ↦ 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1)
    (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
have this : Tendsto ((fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1)
  (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2 / Gammaℝ 1))
Tactic: have := h.div (hasDerivAt_Gammaℝ_one.continuousAt.tendsto.mono_left nhdsWithin_le_nhds)
    (Gammaℝ_one.trans_ne one_ne_zero)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (hypothesis)
Goal:
h : Tendsto (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this :
  Tendsto ((fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1)
    (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2 / Gammaℝ 1))
⊢ Tendsto (fun (s : ℂ) ↦ 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1)
    (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
have this₁ : Tendsto ((fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1) (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
Tactic: rw [Gammaℝ_one, div_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
h : Tendsto (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this :
  Tendsto ((fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1)
    (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
⊢ Tendsto (fun (s : ℂ) ↦ 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1)
    (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
have refine : (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ =ᶠ[𝓝[≠] 1] fun (s : ℂ) ↦ 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)
Tactic: refine this.congr' ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
h : Tendsto (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this :
  Tendsto ((fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1)
    (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
⊢ Membership.mem («γ» := Filter ℂ) (𝓝 1) {z : ℂ | 0 < z.re}
have apply : 1 ∈ re ⁻¹' Ioi 0
Tactic: apply (continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (hypothesis)
Goal:
h : Tendsto (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this :
  Tendsto ((fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1)
    (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
⊢ (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ =ᶠ[𝓝[≠] 1] fun (s : ℂ) ↦ 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)
have this₁ : Membership.mem («γ» := Filter ℂ) (𝓝 1) {z : ℂ | 0 < z.re}
Tactic: have : {z | 0 < re z} ∈ 𝓝 (1 : ℂ) := by
    apply (continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds
    simp only [mem_preimage, one_re, mem_Ioi, zero_lt_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
h : Tendsto (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this_1 :
  Tendsto ((fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1)
    (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this : Membership.mem («γ» := Filter ℂ) (𝓝 1) {z : ℂ | 0 < z.re}
⊢ (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ =ᶠ[𝓝[≠] 1] fun (s : ℂ) ↦ 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)
have rw : ∀ᶠ (x : ℂ) in 𝓝 1,
  Membership.mem («γ» := Set ℂ) {1}ᶜ x →
    HDiv.hDiv (α := ℂ → ℂ) (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) Gammaℝ x = 1 / (x - 1) - 1 / x.Gammaℝ / (x - 1)
Tactic: rw [EventuallyEq, eventually_nhdsWithin_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
h : Tendsto (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this_1 :
  Tendsto ((fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1)
    (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this : Membership.mem («γ» := Filter ℂ) (𝓝 1) {z : ℂ | 0 < z.re}
⊢ ∀ᶠ (x : ℂ) in 𝓝 1,
    Membership.mem («γ» := Set ℂ) {1}ᶜ x →
      HDiv.hDiv (α := ℂ → ℂ) (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) Gammaℝ x = 1 / (x - 1) - 1 / x.Gammaℝ / (x - 1)
have h₁ : ∀ (a : ℂ) (ha : 0 < a.re),
  Membership.mem («γ» := Set ℂ) {1}ᶜ a →
    HDiv.hDiv (α := ℂ → ℂ) (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) Gammaℝ a = 1 / (a - 1) - 1 / a.Gammaℝ / (a - 1)
Tactic: filter_upwards [this] with a ha _
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
h : Tendsto (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this_1 :
  Tendsto ((fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1)
    (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this : Membership.mem («γ» := Filter ℂ) (𝓝 1) {z : ℂ | 0 < z.re}
a : ℂ
ha : 0 < a.re
h_1 : Membership.mem («γ» := Set ℂ) {1}ᶜ a
⊢ HDiv.hDiv (α := ℂ → ℂ) (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) Gammaℝ a = 1 / (a - 1) - 1 / a.Gammaℝ / (a - 1)
have h₁ : (a.Gammaℝ - 1) / (a - 1) / a.Gammaℝ = 1 / (a - 1) - 1 / a.Gammaℝ / (a - 1)
Tactic: rw [Pi.div_apply, ← sub_div, div_right_comm, sub_div' (Gammaℝ_ne_zero_of_re_pos ha), one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
h : Tendsto (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this_1 :
  Tendsto ((fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1)
    (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this : Membership.mem («γ» := Filter ℂ) (𝓝 1) {z : ℂ | 0 < z.re}
a : ℂ
ha : 0 < a.re
h_1 : Membership.mem («γ» := Set ℂ) {1}ᶜ a
h₁ : (a.Gammaℝ - 1) / (a - 1) / a.Gammaℝ = 1 / (a - 1) - 1 / a.Gammaℝ / (a - 1)
⊢ HDiv.hDiv (α := ℂ → ℂ) (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) Gammaℝ a = 1 / (a - 1) - 1 / a.Gammaℝ / (a - 1)
have h₂ : (a.Gammaℝ - 1) / (a - 1) / a.Gammaℝ = (1 - 1 / a.Gammaℝ) / (a - 1)
Tactic: rw [Pi.div_apply, ← sub_div, div_right_comm, sub_div' (Gammaℝ_ne_zero_of_re_pos ha), one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
h : Tendsto (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this_1 :
  Tendsto ((fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1)
    (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this : Membership.mem («γ» := Filter ℂ) (𝓝 1) {z : ℂ | 0 < z.re}
a : ℂ
ha : 0 < a.re
h_1 : Membership.mem («γ» := Set ℂ) {1}ᶜ a
h₁ : (a.Gammaℝ - 1) / (a - 1) / a.Gammaℝ = 1 / (a - 1) - 1 / a.Gammaℝ / (a - 1)
h₂ : (a.Gammaℝ - 1) / (a - 1) / a.Gammaℝ = (1 - 1 / a.Gammaℝ) / (a - 1)
⊢ HDiv.hDiv (α := ℂ → ℂ) (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) Gammaℝ a = 1 / (a - 1) - 1 / a.Gammaℝ / (a - 1)
have h₃ : (a.Gammaℝ - 1) / a.Gammaℝ / (a - 1) = (1 - 1 / a.Gammaℝ) / (a - 1)
Tactic: rw [Pi.div_apply, ← sub_div, div_right_comm, sub_div' (Gammaℝ_ne_zero_of_re_pos ha), one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
h : Tendsto (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this_1 :
  Tendsto ((fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1)
    (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this : Membership.mem («γ» := Filter ℂ) (𝓝 1) {z : ℂ | 0 < z.re}
a : ℂ
ha : 0 < a.re
h_1 : Membership.mem («γ» := Set ℂ) {1}ᶜ a
h₁ : (a.Gammaℝ - 1) / (a - 1) / a.Gammaℝ = 1 / (a - 1) - 1 / a.Gammaℝ / (a - 1)
h₂ : (a.Gammaℝ - 1) / (a - 1) / a.Gammaℝ = (1 - 1 / a.Gammaℝ) / (a - 1)
h₃ : (a.Gammaℝ - 1) / a.Gammaℝ / (a - 1) = (1 - 1 / a.Gammaℝ) / (a - 1)
⊢ HDiv.hDiv (α := ℂ → ℂ) (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) Gammaℝ a = 1 / (a - 1) - 1 / a.Gammaℝ / (a - 1)
have h₄ : (a.Gammaℝ - 1) / a.Gammaℝ / (a - 1) = (1 * a.Gammaℝ - 1) / a.Gammaℝ / (a - 1)
Tactic: rw [Pi.div_apply, ← sub_div, div_right_comm, sub_div' (Gammaℝ_ne_zero_of_re_pos ha), one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
h : Tendsto (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this_1 :
  Tendsto ((fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1)
    (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
this : Membership.mem («γ» := Filter ℂ) (𝓝 1) {z : ℂ | 0 < z.re}
a : ℂ
ha : 0 < a.re
h_1 : Membership.mem («γ» := Set ℂ) {1}ᶜ a
h₁ : (a.Gammaℝ - 1) / (a - 1) / a.Gammaℝ = 1 / (a - 1) - 1 / a.Gammaℝ / (a - 1)
h₂ : (a.Gammaℝ - 1) / (a - 1) / a.Gammaℝ = (1 - 1 / a.Gammaℝ) / (a - 1)
h₃ : (a.Gammaℝ - 1) / a.Gammaℝ / (a - 1) = (1 - 1 / a.Gammaℝ) / (a - 1)
h₄ : (a.Gammaℝ - 1) / a.Gammaℝ / (a - 1) = (1 * a.Gammaℝ - 1) / a.Gammaℝ / (a - 1)
⊢ HDiv.hDiv (α := ℂ → ℂ) (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) Gammaℝ a = 1 / (a - 1) - 1 / a.Gammaℝ / (a - 1)
have h₅ : (a.Gammaℝ - 1) / a.Gammaℝ / (a - 1) = (a.Gammaℝ - 1) / a.Gammaℝ / (a - 1)
Tactic: rw [Pi.div_apply, ← sub_div, div_right_comm, sub_div' (Gammaℝ_ne_zero_of_re_pos ha), one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (hypothesis)
Goal:
⊢ Tendsto (fun (s : ℂ) ↦ riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1)
    (𝓝 (((↑γ : ℂ) - Complex.log (4 * (↑π : ℂ))) / 2))
have this : Tendsto (fun (x : ℂ) ↦ riemannZeta x - 1 / (x - 1) + (1 / (x - 1) - 1 / x.Gammaℝ / (x - 1))) (𝓝[≠] 1)
  (𝓝 ((↑γ : ℂ) + -((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
Tactic: have := tendsto_riemannZeta_sub_one_div.add tendsto_Gamma_term_aux
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (hypothesis)
Goal:
this :
  Tendsto (fun (x : ℂ) ↦ riemannZeta x - 1 / (x - 1) + (1 / (x - 1) - 1 / x.Gammaℝ / (x - 1))) (𝓝[≠] 1)
    (𝓝 ((↑γ : ℂ) + -((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
⊢ Tendsto (fun (s : ℂ) ↦ riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1)
    (𝓝 (((↑γ : ℂ) - Complex.log (4 * (↑π : ℂ))) / 2))
have this₁ : Tendsto (fun (x : ℂ) ↦ riemannZeta x - 1 / x.Gammaℝ / (x - 1)) (𝓝[≠] 1)
  (𝓝 ((↑γ : ℂ) + -((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
Tactic: simp_rw [sub_add_sub_cancel] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
this :
  Tendsto (fun (x : ℂ) ↦ riemannZeta x - 1 / x.Gammaℝ / (x - 1)) (𝓝[≠] 1)
    (𝓝 ((↑γ : ℂ) + -((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
⊢ Tendsto (fun (s : ℂ) ↦ riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1)
    (𝓝 (((↑γ : ℂ) - Complex.log (4 * (↑π : ℂ))) / 2))
have h : ((↑γ : ℂ) - Complex.log (4 * (↑π : ℂ))) / 2 = (↑γ : ℂ) + -((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2
Tactic: convert! this using 2
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (hypothesis)
Goal:
⊢ riemannZeta 1 = ((↑γ : ℂ) - Complex.log (4 * (↑π : ℂ))) / 2
have this : Tendsto (fun (s : ℂ) ↦ HurwitzZeta.hurwitzZetaEven 0 s - 1 / (s - 1) / s.Gammaℝ) (𝓝[≠] 1)
  (𝓝 (HurwitzZeta.hurwitzZetaEven 0 1))
Tactic: have := (HurwitzZeta.tendsto_hurwitzZetaEven_sub_one_div_nhds_one 0).mono_left
    <| nhdsWithin_le_nhds (s := {1}ᶜ)
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (hypothesis)
Goal:
this :
  Tendsto (fun (s : ℂ) ↦ HurwitzZeta.hurwitzZetaEven 0 s - 1 / (s - 1) / s.Gammaℝ) (𝓝[≠] 1)
    (𝓝 (HurwitzZeta.hurwitzZetaEven 0 1))
⊢ riemannZeta 1 = ((↑γ : ℂ) - Complex.log (4 * (↑π : ℂ))) / 2
have this₁ : Tendsto (fun (s : ℂ) ↦ riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 (riemannZeta 1))
Tactic: simp only [HurwitzZeta.hurwitzZetaEven_zero, div_right_comm _ _ (Gammaℝ _)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (hypothesis)
Goal:
⊢ completedRiemannZeta₀ 1 = ((↑γ : ℂ) - Complex.log (4 * (↑π : ℂ))) / 2 + 1
have this : completedRiemannZeta 1 = completedRiemannZeta₀ 1 - 1 / 1 - 1 / HSub.hSub (α := ℂ) 1 1
Tactic: have := completedRiemannZeta_eq 1
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (hypothesis)
Goal:
this : completedRiemannZeta 1 = completedRiemannZeta₀ 1 - 1 / 1 - 1 / HSub.hSub (α := ℂ) 1 1
⊢ completedRiemannZeta₀ 1 = ((↑γ : ℂ) - Complex.log (4 * (↑π : ℂ))) / 2 + 1
have this₁ : completedRiemannZeta 1 + 1 = completedRiemannZeta₀ 1
Tactic: rw [sub_self, div_zero, div_one, sub_zero, eq_sub_iff_add_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
this : completedRiemannZeta 1 + 1 = completedRiemannZeta₀ 1
⊢ completedRiemannZeta₀ 1 = ((↑γ : ℂ) - Complex.log (4 * (↑π : ℂ))) / 2 + 1
have rw : completedRiemannZeta 1 + 1 = ((↑γ : ℂ) - Complex.log (4 * (↑π : ℂ))) / 2 + 1
Tactic: rw [← this, completedRiemannZeta_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
this : completedRiemannZeta 1 + 1 = completedRiemannZeta₀ 1
rw : completedRiemannZeta 1 + 1 = ((↑γ : ℂ) - Complex.log (4 * (↑π : ℂ))) / 2 + 1
⊢ completedRiemannZeta₀ 1 = ((↑γ : ℂ) - Complex.log (4 * (↑π : ℂ))) / 2 + 1
have rw₁ : ((↑γ : ℂ) - Complex.log (4 * (↑π : ℂ))) / 2 + 1 = ((↑γ : ℂ) - Complex.log (4 * (↑π : ℂ))) / 2 + 1
Tactic: rw [← this, completedRiemannZeta_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
⊢ riemannZeta 1 ≠ 0
have suffices : (γ - Real.log (4 * π)) / 2 ≠ 0
Tactic: suffices (γ - (4 * π).log) / 2 ≠ 0 by
    simpa only [riemannZeta_one, ← ofReal_ne_zero, ofReal_log (by positivity : 0 ≤ 4 * π),
      push_cast]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
⊢ (γ - Real.log (4 * π)) / 2 ≠ 0
have refine_1 : γ < 1
Tactic: refine div_ne_zero (sub_lt_zero.mpr (lt_trans ?_ ?_ (b := 1))).ne two_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
refine_1 : γ < 1
⊢ (γ - Real.log (4 * π)) / 2 ≠ 0
have refine_2 : 1 < Real.log (4 * π)
Tactic: refine div_ne_zero (sub_lt_zero.mpr (lt_trans ?_ ?_ (b := 1))).ne two_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
⊢ 1 < Real.log (4 * π)
have refine_2 : rexp 1 < 4 * π
Tactic: rw [lt_log_iff_exp_lt (by positivity)]
-- Lean 4 proof step from Mathlib.NumberTheory.Harmonic.ZetaAsymp (goal)
Goal:
⊢ ∀ᶠ (s : ℂ) in 𝓝 1, riemannZeta s ≠ 0
have h : ∀ (a : ℂ), (Membership.mem («γ» := Set ℂ) {1}ᶜ a → (a - 1) * riemannZeta a ≠ 0) → riemannZeta a ≠ 0
Tactic: filter_upwards [eventually_nhdsWithin_iff.1 <| riemannZeta_residue_one.eventually_ne one_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
⊢ log
      (HMul.hMul (α := ℝ)
        (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal))
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x) 1)) =
    HAdd.hAdd (α := ℝ)
      (Multiset.sum (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ log⁺ ((v : (a : K) → ℝ) x)) archAbsVal))
      (∑ᶠ (v : (↑nonarchAbsVal : Type u_1)), log⁺ (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x))
have H : mulHeight₁ x ≠ 0
Tactic: have H : mulHeight₁ x ≠ 0 := mulHeight₁_ne_zero x
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
H : mulHeight₁ x ≠ 0
⊢ log
      (HMul.hMul (α := ℝ)
        (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal))
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x) 1)) =
    HAdd.hAdd (α := ℝ)
      (Multiset.sum (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ log⁺ ((v : (a : K) → ℝ) x)) archAbsVal))
      (∑ᶠ (v : (↑nonarchAbsVal : Type u_1)), log⁺ (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x))
have H₁ : HMul.hMul (α := ℝ) (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal))
    (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x) 1) ≠
  0
Tactic: rw [mulHeight₁_eq] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
H :
  HMul.hMul (α := ℝ)
      (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x) 1) ≠
    0
a : ℝ
ha :
  Membership.mem (γ := Multiset ℝ) (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal)
    a
⊢ a ≠ 0
have contrapose : ∀ (ha : a = 0), a ∉ Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal
Tactic: contrapose ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
H :
  HMul.hMul (α := ℝ)
      (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x) 1) ≠
    0
a : ℝ
ha : a = 0
⊢ a ∉ Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal
have rw : 0 ∉ Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal
Tactic: rw [ha]
-- Lean 4 proof step from Mathlib.NumberTheory.Height.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : AdmissibleAbsValues K
x : K
H :
  HMul.hMul (α := ℝ)
      (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal))
      (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x) 1) ≠
    0
⊢ log
      (HMul.hMul (α := ℝ)
        (Multiset.prod (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal))
        (∏ᶠ (v : (↑nonarchAbsVal : Type u_1)), max (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x) 1)) =
    HAdd.hAdd (α := ℝ)
      (Multiset.sum (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ log⁺ ((v : (a : K) → ℝ) x)) archAbsVal))
      (∑ᶠ (v : (↑nonarchAbsVal : Type u_1)), log⁺ (((↑v : AbsoluteValue K ℝ) : (a : K) → ℝ) x))
have this : ∀ (a : ℝ),
  Membership.mem (γ := Multiset ℝ) (Multiset.map (fun (v : AbsoluteValue K ℝ) ↦ max ((v : (a : K) → ℝ) x) 1) archAbsVal)
      a →
    a ≠ 0
Tactic: have : ∀ a ∈ archAbsVal.map (fun v ↦ max (v x) 1), a ≠ 0 := by
    intro a ha
    contrapose ha
    rw [ha]
    exact Multiset.prod_eq_zero_iff.not.mp <| left_ne_zero_of_mul H