awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
aux2 :
  Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))
⊢ ∑' (b : ℕ), term (b + 1) 1 = 1 - γ

Tactic:
have := term_tsum_one.tsum_eq
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
aux2 :
  Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))
this : ∑' (b : ℕ), term (b + 1) 1 = 1 - γ
⊢ γ = 1 - term_tsum 1

Tactic:
rw [← term_tsum, eq_sub_iff_add_eq, ← eq_sub_iff_add_eq'] at this

Premises used: eq_sub_iff_add_eq', ZetaAsymptotics.term_tsum, eq_sub_iff_add_eq
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
aux2 :
  Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))
this : γ = 1 - term_tsum 1
⊢ Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)

Tactic:
simpa only [this] using aux2
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
suffices :
  Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))
⊢ Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)

Tactic:
suffices aux2 : Tendsto (fun s : ℝ ↦ (∑' n : ℕ, 1 / (n + 1 : ℝ) ^ s) - 1 / (s - 1))
    (𝓝[>] 1) (𝓝 (1 - term_tsum 1)) by
    have := term_tsum_one.tsum_eq
    rw [← term_tsum, eq_sub_iff_add_eq, ← eq_sub_iff_add_eq'] at this
    simpa only [this] using aux2
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
hl :
  EventuallyEq (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ 1 - s * term_tsum s) fun (s : ℝ) ↦
    ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)
h : Tendsto (fun (s : ℝ) ↦ 1 - s * term_tsum s) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))
f₁ : ℝ → ℝ
⊢ Tendsto (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))

Tactic:
apply Tendsto.congr'

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
s : ℝ
hs : Membership.mem («γ» := Set ℝ) (Ioi 1) s
⊢ 1 - s * term_tsum s = ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)

Tactic:
(zeta_limit_aux1 hs).symm

Premises used: ZetaAsymptotics.zeta_limit_aux1, Eq.symm
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
h :
  ∀ (a : ℝ),
    Membership.mem («γ» := Set ℝ)
      {x : ℝ |
        Membership.mem («γ» := Set ℝ) (Ioi 1) x →
          Membership.mem («γ» := Set ℝ)
            {x : ℝ |
              (fun (x : ℝ) ↦
                  1 - x * term_tsum x =
                    (fun (s : ℝ) ↦ ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)) x)
                x}
            x}
      a
h₁ h₂ :
  ∀ (s : ℝ) (hs : Membership.mem («γ» := Set ℝ) (Ioi 1) s),
    1 - s * term_tsum s = ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)
⊢ EventuallyEq (β := ℝ) (𝓝[>] 1) (fun (s : ℝ) ↦ 1 - s * term_tsum s) fun (s : ℝ) ↦
    ∑' (n : ℕ), 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ^ s - 1 / (s - 1)

Tactic:
filter_upwards [self_mem_nhdsWithin] with s hs using (zeta_limit_aux1 hs).symm

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
h : Tendsto (fun (x : ℝ) ↦ x * term_tsum x) (𝓝[>] 1) (𝓝 (term_tsum 1))
⊢ Tendsto (fun (s : ℝ) ↦ 1 - s * term_tsum s) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))

Tactic:
apply tendsto_const_nhds.sub

Premises used: tendsto_const_nhds, Filter.Tendsto.sub
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
h : Tendsto (fun (x : ℝ) ↦ x * term_tsum x) (𝓝[>] 1) (𝓝 (1 * term_tsum 1))
⊢ Tendsto (fun (x : ℝ) ↦ x * term_tsum x) (𝓝[>] 1) (𝓝 (term_tsum 1))

Tactic:
rw [← one_mul (term_tsum 1)]

Premises used: ZetaAsymptotics.term_tsum, OfNat.ofNat, one_mul
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
h : Tendsto term_tsum (𝓝[>] 1) (𝓝 (term_tsum 1))
⊢ Tendsto (fun (x : ℝ) ↦ x * term_tsum x) (𝓝[>] 1) (𝓝 (1 * term_tsum 1))

Tactic:
apply (tendsto_id.mono_left nhdsWithin_le_nhds).mul

Premises used: Filter.tendsto_id, Filter.Tendsto.mul, nhdsWithin_le_nhds, Filter.Tendsto.mono_left
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
⊢ ContinuousWithinAt term_tsum (Ici 1) 1

Tactic:
have := continuousOn_term_tsum.continuousWithinAt self_mem_Ici
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this : ContinuousWithinAt term_tsum (Ici 1) 1
⊢ Tendsto term_tsum (𝓝[>] 1) (𝓝 (term_tsum 1))

Tactic:
Tendsto.mono_left this (nhdsWithin_mono _ Ioi_subset_Ici_self)

Premises used: Set.Ioi_subset_Ici_self, Filter.Tendsto.mono_left, nhdsWithin_mono
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
this : ContinuousWithinAt term_tsum (Ici 1) 1
⊢ Tendsto term_tsum (𝓝[>] 1) (𝓝 (term_tsum 1))

Tactic:
exact Tendsto.mono_left this (nhdsWithin_mono _ Ioi_subset_Ici_self)

Premises used: Set.Ioi_subset_Ici_self, Filter.Tendsto.mono_left, nhdsWithin_mono
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
this : ∃ (C : ℂ), Tendsto f (𝓝[≠] 1) (𝓝 C)
obtain :
  ∀ (C : ℂ) (hC : Tendsto f (𝓝[≠] 1) (𝓝 C)), Tendsto (fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)) (𝓝[≠] 1) (𝓝 (↑γ : ℂ))
⊢ Tendsto (fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)) (𝓝[≠] 1) (𝓝 (↑γ : ℂ))

Tactic:
obtain ⟨C, hC⟩ := this
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
suffices : Tendsto (fun (s : ℝ) ↦ f (↑s : ℂ)) (𝓝[>] 1) (𝓝 C)
⊢ Tendsto (fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)) (𝓝[≠] 1) (𝓝 (↑γ : ℂ))

Tactic:
suffices Tendsto (fun s : ℝ ↦ f s) _ _
      from (tendsto_nhds_unique this tendsto_riemannZeta_sub_one_div_nhds_right) ▸ hC
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
⊢ Tendsto (fun (s : ℝ) ↦ f (↑s : ℂ)) (𝓝[>] 1) (𝓝 C)

Tactic:
hC.comp (tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ ?_ ?_)

Premises used: tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
refine_1 : Tendsto Complex.ofReal (𝓝[>] 1) (𝓝 1)
refine_2 : ∀ᶠ (x : ℝ) in 𝓝[>] 1, Membership.mem («γ» := Set ℂ) {1}ᶜ (↑x : ℂ)
⊢ Tendsto (fun (s : ℝ) ↦ f (↑s : ℂ)) (𝓝[>] 1) (𝓝 C)

Tactic:
refine hC.comp (tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ ?_ ?_)

Premises used: tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within, Filter.Tendsto.comp
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
⊢ Tendsto Complex.ofReal (𝓝[>] 1) (𝓝 1)

Tactic:
(Complex.continuous_ofReal.tendsto 1).mono_left (nhdsWithin_le_nhds ..)

Premises used: Continuous.tendsto, nhdsWithin_le_nhds, Complex.continuous_ofReal, Filter.Tendsto.mono_left, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
⊢ Tendsto Complex.ofReal (𝓝[>] 1) (𝓝 1)

Tactic:
exact (Complex.continuous_ofReal.tendsto 1).mono_left (nhdsWithin_le_nhds ..)

Premises used: Continuous.tendsto, nhdsWithin_le_nhds, Complex.continuous_ofReal, Filter.Tendsto.mono_left, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
h : ∀ (a : ℝ) (ha : Membership.mem («γ» := Set ℝ) (Ioi 1) a), Membership.mem («γ» := Set ℂ) {1}ᶜ (↑a : ℂ)
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 1, Membership.mem («γ» := Set ℂ) {1}ᶜ (↑x : ℂ)

Tactic:
filter_upwards [self_mem_nhdsWithin] with a ha

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
a : ℝ
ha : Membership.mem («γ» := Set ℝ) (Ioi 1) a
h : ¬a = 1
⊢ Membership.mem («γ» := Set ℂ) {1}ᶜ (↑a : ℂ)

Tactic:
rw [mem_compl_singleton_iff, ← Complex.ofReal_one, Ne, Complex.ofReal_inj]

Premises used: Complex.ofReal_one, Ne, Set.mem_compl_singleton_iff, Complex.ofReal_inj
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
a : ℝ
ha : Membership.mem («γ» := Set ℝ) (Ioi 1) a
⊢ ¬a = 1

Tactic:
ne_of_gt ha

Premises used: ne_of_gt
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
a : ℝ
ha : Membership.mem («γ» := Set ℝ) (Ioi 1) a
⊢ ¬a = 1

Tactic:
exact ne_of_gt ha

Premises used: ne_of_gt
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
suffices : ∃ (C : ℂ), Tendsto f (𝓝[≠] 1) (𝓝 C)
⊢ Tendsto (fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)) (𝓝[≠] 1) (𝓝 (↑γ : ℂ))

Tactic:
suffices ∃ C, Tendsto f (𝓝[≠] 1) (𝓝 C) by
    obtain ⟨C, hC⟩ := this
    suffices Tendsto (fun s : ℝ ↦ f s) _ _
      from (tendsto_nhds_unique this tendsto_riemannZeta_sub_one_div_nhds_right) ▸ hC
    refine hC.comp (tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ ?_ ?_)
    · exact (Complex.continuous_ofReal.tendsto 1).mono_left (nhdsWithin_le_nhds ..)
    · filter_upwards [self_mem_nhdsWithin] with a ha
      rw [mem_compl_singleton_iff, ← Complex.ofReal_one, Ne, Complex.ofReal_inj]
      exact ne_of_gt ha
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
⊢ ∃ (C : ℂ), Tendsto f (𝓝[≠] 1) (𝓝 C)

Tactic:
⟨_, Complex.tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO ?_ ?_⟩

Premises used: Exists.intro, Complex.tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
refine_1 : ∀ᶠ (z : ℂ) in 𝓝[≠] 1, DifferentiableAt ℂ f z
refine_2 : Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] 1) (fun (z : ℂ) ↦ f z - f 1) fun (z : ℂ) ↦ (z - 1)⁻¹
⊢ ∃ (C : ℂ), Tendsto f (𝓝[≠] 1) (𝓝 C)

Tactic:
refine ⟨_, Complex.tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO ?_ ?_⟩
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
h : ∀ (s : ℂ) (hs : Membership.mem («γ» := Set ℂ) {1}ᶜ s), DifferentiableAt ℂ f s
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] 1, DifferentiableAt ℂ f z

Tactic:
filter_upwards [self_mem_nhdsWithin] with s hs

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
s : ℂ
hs : Membership.mem («γ» := Set ℂ) {1}ᶜ s
⊢ DifferentiableAt ℂ f s

Tactic:
(differentiableAt_riemannZeta hs).sub ((differentiableAt_const _).div ?_ ?_)

Premises used: DifferentiableAt.div, differentiableAt_riemannZeta, DifferentiableAt.sub, differentiableAt_const
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
s : ℂ
hs : Membership.mem («γ» := Set ℂ) {1}ᶜ s
h : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ s - 1) s
h₁ : s - 1 ≠ 0
⊢ DifferentiableAt ℂ f s

Tactic:
refine (differentiableAt_riemannZeta hs).sub ((differentiableAt_const _).div ?_ ?_)

Premises used: DifferentiableAt.div, differentiableAt_riemannZeta, DifferentiableAt.sub, differentiableAt_const
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
s : ℂ
hs : Membership.mem («γ» := Set ℂ) {1}ᶜ s
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ s - 1) s

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
s : ℂ
hs : Membership.mem («γ» := Set ℂ) {1}ᶜ s
h : ∀ (hs : s ≠ 1), s - 1 ≠ 0
h₁ h₂ h₃ h₄ : ∀ (hs : s - 1 ≠ 0), s - 1 ≠ 0
⊢ s - 1 ≠ 0

Tactic:
rwa [mem_compl_singleton_iff, ← sub_ne_zero] at hs

Premises used: sub_ne_zero, Set.mem_compl_singleton_iff
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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)⁻¹

Tactic:
Asymptotics.isLittleO_of_tendsto' ?_ ?_

Premises used: Asymptotics.isLittleO_of_tendsto'
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
refine_2 : ∀ᶠ (x : ℂ) in 𝓝[≠] 1, (x - 1)⁻¹ = 0 → f x - f 1 = 0
refine_2₁ : Tendsto (β := ℂ) (fun (x : ℂ) ↦ (f x - f 1) / (x - 1)⁻¹) (𝓝[≠] 1) (𝓝 0)
⊢ Asymptotics.IsLittleO (E := ℂ) (F := ℂ) (𝓝[≠] 1) (fun (z : ℂ) ↦ f z - f 1) fun (z : ℂ) ↦ (z - 1)⁻¹

Tactic:
refine Asymptotics.isLittleO_of_tendsto' ?_ ?_

Premises used: Asymptotics.isLittleO_of_tendsto'
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
h : ∀ (t : ℂ) (ht : Membership.mem («γ» := Set ℂ) {1}ᶜ t) (ht' : (t - 1)⁻¹ = 0), f t - f 1 = 0
⊢ ∀ᶠ (x : ℂ) in 𝓝[≠] 1, (x - 1)⁻¹ = 0 → f x - f 1 = 0

Tactic:
filter_upwards [self_mem_nhdsWithin] with t ht ht'

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
t : ℂ
ht : Membership.mem («γ» := Set ℂ) {1}ᶜ t
ht' : (t - 1)⁻¹ = 0
⊢ t = 1

Tactic:
rw [inv_eq_zero, sub_eq_zero] at ht'

Premises used: inv_eq_zero, sub_eq_zero
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
t : ℂ
ht : Membership.mem («γ» := Set ℂ) {1}ᶜ t
ht' : t = 1
⊢ f t - f 1 = 0

Tactic:
tauto
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
⊢ 𝓝 0 = 𝓝 (HSub.hSub (α := ℂ) 1 1 - f 1 * HSub.hSub (α := ℂ) 1 1)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
refine_2 :
  Tendsto (fun (x : ℂ) ↦ f x * (x - 1) - f 1 * (x - 1)) (𝓝[≠] 1)
    (𝓝 (HSub.hSub (α := ℂ) 1 1 - f 1 * HSub.hSub (α := ℂ) 1 1))
⊢ Tendsto (β := ℂ) (fun (x : ℂ) ↦ (f x - f 1) / (x - 1)⁻¹) (𝓝[≠] 1) (𝓝 0)

Tactic:
simp_rw [div_eq_mul_inv, inv_inv, sub_mul,
        (by ring_nf : 𝓝 (0 : ℂ) = 𝓝 ((1 - 1) - f 1 * (1 - 1)))]

Premises used: div_eq_mul_inv, sub_mul, inv_inv
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
refine_2 : Tendsto (fun (x : ℂ) ↦ f x * (x - 1)) (𝓝[≠] 1) (𝓝 (HSub.hSub (α := ℂ) 1 1))
refine_2₁ : Tendsto (fun (x : ℂ) ↦ f 1 * (x - 1)) (𝓝[≠] 1) (𝓝 (f 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))

Tactic:
apply Tendsto.sub

Premises used: Filter.Tendsto.sub
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
refine_2 :
  Tendsto (fun (x : ℂ) ↦ (x - 1) * riemannZeta x - (x - 1) * (1 / (x - 1))) (𝓝[≠] 1) (𝓝 (HSub.hSub (α := ℂ) 1 1))
⊢ Tendsto (fun (x : ℂ) ↦ f x * (x - 1)) (𝓝[≠] 1) (𝓝 (HSub.hSub (α := ℂ) 1 1))

Tactic:
simp_rw [mul_comm (f _), f, mul_sub]

Premises used: mul_sub, mul_comm
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
refine_2 : Tendsto (β := ℂ) (fun (x : ℂ) ↦ (x - 1) * (1 / (x - 1))) (𝓝[≠] 1) (𝓝 1)
⊢ Tendsto (fun (x : ℂ) ↦ (x - 1) * riemannZeta x - (x - 1) * (1 / (x - 1))) (𝓝[≠] 1) (𝓝 (HSub.hSub (α := ℂ) 1 1))

Tactic:
apply riemannZeta_residue_one.sub

Premises used: riemannZeta_residue_one, Filter.Tendsto.sub
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
⊢ Tendsto (β := ℂ) (fun (x : ℂ) ↦ (x - 1) * (1 / (x - 1))) (𝓝[≠] 1) (𝓝 1)

Tactic:
Tendsto.congr' ?_ (tendsto_const_nhds.mono_left nhdsWithin_le_nhds)

Premises used: tendsto_const_nhds, nhdsWithin_le_nhds, Filter.Tendsto.mono_left, Filter.Tendsto.congr'
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
refine_2 : EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (x : ℂ) ↦ 1) fun (x : ℂ) ↦ (x - 1) * (1 / (x - 1))
⊢ Tendsto (β := ℂ) (fun (x : ℂ) ↦ (x - 1) * (1 / (x - 1))) (𝓝[≠] 1) (𝓝 1)

Tactic:
refine Tendsto.congr' ?_ (tendsto_const_nhds.mono_left nhdsWithin_le_nhds)

Premises used: tendsto_const_nhds, nhdsWithin_le_nhds, Filter.Tendsto.mono_left, Filter.Tendsto.congr'
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
h : ∀ (x : ℂ) (hx : Membership.mem («γ» := Set ℂ) {1}ᶜ x), 1 = (x - 1) * (1 / (x - 1))
⊢ EventuallyEq (β := ℂ) (𝓝[≠] 1) (fun (x : ℂ) ↦ 1) fun (x : ℂ) ↦ (x - 1) * (1 / (x - 1))

Tactic:
filter_upwards [self_mem_nhdsWithin] with x hx

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
x : ℂ
hx : Membership.mem («γ» := Set ℂ) {1}ᶜ x
⊢ 1 = (x - 1) * (1 / (x - 1))

Tactic:
field [sub_ne_zero.mpr <| mem_compl_singleton_iff.mp hx]

Premises used: Iff.mpr, sub_ne_zero, Set.mem_compl_singleton_iff, Iff.mp
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun (x : ℂ) ↦ f 1 * (x - 1)) (𝓝[≠] 1) (𝓝 (f 1 * HSub.hSub (α := ℂ) 1 1))

Tactic:
((tendsto_id.sub tendsto_const_nhds).mono_left nhdsWithin_le_nhds).const_mul _

Premises used: Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.const_mul, nhdsWithin_le_nhds, Filter.Tendsto.mono_left, Filter.Tendsto.sub
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
f : (s : ℂ) → ℂ := fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)
⊢ Tendsto (fun (x : ℂ) ↦ f 1 * (x - 1)) (𝓝[≠] 1) (𝓝 (f 1 * HSub.hSub (α := ℂ) 1 1))

Tactic:
exact ((tendsto_id.sub tendsto_const_nhds).mono_left nhdsWithin_le_nhds).const_mul _

Premises used: Filter.tendsto_id, tendsto_const_nhds, Filter.Tendsto.const_mul, nhdsWithin_le_nhds, Filter.Tendsto.mono_left, Filter.Tendsto.sub
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
F : Type u_1
inst : Norm F
inst_1 : One F
inst_2 : NormOneClass F
⊢ Asymptotics.IsBigO.{0, 0, u_1} (E := ℂ) (F := F) (𝓝 1) (fun (s : ℂ) ↦ riemannZeta s - 1 / (s - 1)) fun (x : ℂ) ↦ 1

Tactic:
simpa only [Asymptotics.isBigO_one_nhds_ne_iff] using
     tendsto_riemannZeta_sub_one_div.isBigO_one (F := F)

Premises used: Filter.Tendsto.isBigO_one, tendsto_riemannZeta_sub_one_div, Asymptotics.isBigO_one_nhds_ne_iff
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
⊢ HasDerivAt Gammaℝ (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2) 1

Tactic:
have h := hasDerivAt_Gammaℝ_one
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
h : HasDerivAt Gammaℝ (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2) 1
⊢ 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

Premises used: Complex.Gammaℝ_one, slope_fun_def_field, hasDerivAt_iff_tendsto_slope
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
Goal:
h : Tendsto (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))
⊢ 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)
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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 (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1)
    (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))

Tactic:
rw [Gammaℝ_one, div_one] at this

Premises used: Complex.Gammaℝ_one, div_one
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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))

Tactic:
this.congr' ?_

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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))
refine : (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ =ᶠ[𝓝[≠] 1] fun (s : ℂ) ↦ 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)
⊢ Tendsto (fun (s : ℂ) ↦ 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1)
    (𝓝 (-((↑γ : ℂ) + Complex.log (4 * (↑π : ℂ))) / 2))

Tactic:
refine this.congr' ?_

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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))
apply : 1 ∈ re ⁻¹' Ioi 0
⊢ Membership.mem («γ» := Filter ℂ) (𝓝 1) {z : ℂ | 0 < z.re}

Tactic:
apply (continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds

Premises used: Complex.continuous_re, isOpen_Ioi, IsOpen.mem_nhds, Continuous.isOpen_preimage
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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))
⊢ 1 ∈ re ⁻¹' Ioi 0

Tactic:
simp only [mem_preimage, one_re, mem_Ioi, zero_lt_one]

Premises used: Set.mem_Ioi, zero_lt_one, Complex.one_re, Set.mem_preimage
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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}

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]
-- Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp
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}
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)
⊢ (fun (b : ℂ) ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ =ᶠ[𝓝[≠] 1] fun (s : ℂ) ↦ 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)

Tactic:
rw [EventuallyEq, eventually_nhdsWithin_iff]

Premises used: Filter.EventuallyEq, eventually_nhdsWithin_iff