mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.LSeries.Positivity

Goal state before:
pp: case refine_1
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
hxy : x < max x y + 1
hxy' : abscissaOfAbsConv a < ↑(max x y) + 1
hys : ↑(max x y) + 1 ∈ {s | x < s.re}
hfx : 0 < f (↑(max x y) + 1)
n : ℕ
x✝ : n ≠ 0
hs : IsOpen {s | x < s.re}
⊢ 0 ≤ (-1) ^ n * iteratedDeriv n f (↑(max x y) + 1)

Tactic:
simpa using

Goal state after:
case refine_1
a : ℕ → ℂ
ha₀ : 0 ≤ a
ha₁ : 0 < a 1
f : ℂ → ℂ
hf : Differentiable ℂ f
x : ℝ
hx : abscissaOfAbsConv a ≤ ↑x
hf' : Set.EqOn f (LSeries a) {s | x < s.re}
y : ℝ
hxy : x < max x y + 1
hxy' : abscissaOfAbsConv a < ↑(max x y) + 1
hys : ↑(max x y) + 1 ∈ {s | x < s.re}
hfx : 0 < f (↑(max x y) + 1)
n : ℕ
x✝ : n ≠ 0
hs : IsOpen {s | x < s.re}
⊢ 0 ≤ (-1) ^ n * iteratedDeriv n (LSeries a) (↑(max x y) + 1)
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case h.inr.inl.inr
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₁ : ↑1 = 1 → -(1 / 2) < ξ - ↑u
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
⊢ ∃ n, ↑u = ξ.convergent n

Tactic:
replace h₁ := lt_sub_iff_add_lt'.mp (h₁ rfl)
      have hξ₁ : ⌊ξ⌋ = u - 1 := by
        rw [floor_eq_iff, cast_sub, cast_one, sub_add_cancel]
        exact ⟨(((sub_lt_sub_iff_left _).mpr one_half_lt_one).trans h₁).le, ht⟩
      rcases eq_or_ne ξ ⌊ξ⌋ with Hξ | Hξ
      · rw [Hξ, hξ₁, cast_sub, cast_one, ← sub_eq_add_neg, sub_lt_sub_iff_left] at h₁
        exact False.elim (lt_irrefl _ <| h₁.trans one_half_lt_one)
      · have hξ₂ : ⌊(fract ξ)⁻¹⌋ = 1 := by
          rw [floor_eq_iff, cast_one, le_inv_comm₀ zero_lt_one (fract_pos.mpr Hξ), inv_one,
            one_add_one_eq_two, inv_lt_comm₀ (fract_pos.mpr Hξ) zero_lt_two]
          refine ⟨(fract_lt_one ξ).le, ?_⟩
          rw [fract, hξ₁, cast_sub, cast_one, lt_sub_iff_add_lt', sub_add]
          convert! h₁ using 1
          rw [sub_eq_add_neg]
          norm_num
        use 1
        simp [convergent, hξ₁, hξ₂, cast_sub, cast_one]

Goal state after:
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case refine_1
ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
⊢ IsCoprime q.num ↑q.den

Tactic:
exact isCoprime_iff_nat_coprime.mpr (natAbs_natCast q.den ▸ q.reduced)

Goal state after:
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
hq₀ : 0 < ↑q.den
hq₁ : 0 < ↑q.den * (2 * ↑q.den - 1)
hq₂ : 0 < 2 * (↑q.den * ↑q.den)
⊢ 1 / (2 * ↑q.den ^ 2) < (↑q.den * (2 * ↑q.den - 1))⁻¹

Tactic:
← one_div,

Goal state after:
ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
hq₀ : 0 < ↑q.den
hq₁ : 0 < ↑q.den * (2 * ↑q.den - 1)
hq₂ : 0 < 2 * (↑q.den * ↑q.den)
⊢ 1 / (2 * ↑q.den ^ 2) < 1 / (↑q.den * (2 * ↑q.den - 1))
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
hC' : ‖P.g x⁻¹ - P.g₀‖ ≤ C * ‖x⁻¹ ^ (-(r + P.k))‖
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
⊢ ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖

Tactic:
← one_div,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖P.g (1 / x) - P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖
⊢ ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: t : ℝ
ht : 0 < t
⊢ rexp (-π * t) < 1

Tactic:
simpa using

Goal state after:
t : ℝ
ht : 0 < t
⊢ 0 < π * t
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case refine_1
z τ : ℂ
hτ : 0 < τ.im
⊢ ∀ (i : ℤ), ‖jacobiTheta₂_term i z τ‖ ≤ ↑|i| ^ 0 * rexp (-π * (τ.im * ↑i ^ 2 - 2 * |z.im| * ↑|i|))

Tactic:
simpa using

Goal state after:
case refine_1
z τ : ℂ
hτ : 0 < τ.im
⊢ ∀ (i : ℤ), ‖jacobiTheta₂_term i z τ‖ ≤ rexp (-π * (τ.im * ↑i ^ 2 - 2 * |z.im| * ↑|i|))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
⊢ (↑n + a) ^ 0 * rexp (-π * (↑n + a ^ 2) * t) = rexp (-π * a ^ 2 * t) * rexp (-π * t) ^ n

Tactic:
← Real.exp_nat_mul,

Goal state after:
case e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
⊢ (↑n + a) ^ 0 * rexp (-π * (↑n + a ^ 2) * t) = rexp (-π * a ^ 2 * t) * rexp (↑n * (-π * t))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case refine_2.inr.inr.inl
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im = 0
⊢ (Summable fun x ↦ rexp (-(2 * π * ↑x * z.im))) → False

Tactic:
simpa using

Goal state after:
case refine_2.inr.inr.inl
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
hz : z.im = 0
⊢ 1 = 0 → False
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
step1 : mellin (fun t ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t ↦ ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s
step3 : mellin (fun t ↦ P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s
t : ℝ
ht : t ∈ Ioi 0
⊢ ↑t ^ ↑P.k ≠ 0

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
s : ℂ
step1 : mellin (fun t ↦ P.g (1 / t)) (-s) = mellin P.g s
step2 : mellin (fun t ↦ ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s
step3 : mellin (fun t ↦ P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s
t : ℝ
ht : t ∈ Ioi 0
⊢ ¬t ^ P.k = 0
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ ‖rexp (-π * t)‖ < 1

Tactic:
simpa using

Goal state after:
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
⊢ rexp (-π * t) < 1
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
r : ℝ
⊢ P.f =O[atTop] fun x ↦ x ^ r

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
r : ℝ
⊢ P.f =O[atTop] fun x ↦ x ^ r
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
r : ℝ
⊢ P.f =O[𝓝[>] 0] fun x ↦ x ^ r

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
hP : IsStrongFEPair P
r : ℝ
⊢ P.f =O[𝓝[>] 0] fun x ↦ x ^ r
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
n : ℕ
⊢ ↑n * rexp (-π * (↑n + a ^ 2) * t) = ↑n * rexp (-π * t) ^ n * rexp (-π * a ^ 2 * t)

Tactic:
← Real.exp_nat_mul,

Goal state after:
case e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
h0' : ‖rexp (-π * t)‖ < 1
n : ℕ
⊢ ↑n * rexp (-π * (↑n + a ^ 2) * t) = ↑n * rexp (↑n * (-π * t)) * rexp (-π * a ^ 2 * t)
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
⊢ ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-(π * q i) * t))) (?m.122 t)

Tactic:
simpa using

Goal state after:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
⊢ ∀ (t : ℝ), 0 < t → HasSum (fun i ↦ a i * cexp (-(↑π * ↑(q i) * ↑t))) (?m.122 t)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: case e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
⊢ a * rexp (-π * (↑n + a ^ 2) * t) = a * rexp (-π * a ^ 2 * t) * rexp (-π * t) ^ n

Tactic:
← Real.exp_nat_mul,

Goal state after:
case e'_5
a : ℝ
ha : 0 ≤ a
t : ℝ
ht : 0 < t
n : ℕ
⊢ a * rexp (-π * (↑n + a ^ 2) * t) = a * rexp (-π * a ^ 2 * t) * rexp (↑n * (-π * t))
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: a : ℝ
ha : 0 ≤ a
⊢ (fun t ↦ ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x ↦ 1

Tactic:
simpa only [inv_pow, one_pow] using! isBigO_one_aux.pow 2

Goal state after:
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
this : ∀ (i : ι), ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
⊢ Summable fun i ↦ ‖a i‖ / (π * q i) ^ s.re

Tactic:
simpa using

Goal state after:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
q : ι → ℝ
F : ℝ → ℂ
s : ℂ
hq : ∀ (i : ι), a i = 0 ∨ 0 < q i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-π * q i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / q i ^ s.re
hp : ∀ (i : ι), a i = 0 ∨ 0 < π * q i
this : ∀ (i : ι), ‖a i‖ / (π * q i) ^ s.re = π ^ (-s.re) * ‖a i‖ / q i ^ s.re
⊢ Summable fun i ↦ π ^ (-s.re) * (‖a i‖ / q i ^ s.re)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
⊢ -1 < (s - 1).re

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
⊢ 0 < s.re
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
⊢ -1 < (s - ↑P.k - 1).re

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
⊢ P.k < s.re
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
u : ℤ → ℝ := fun n ↦ 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
⊢ Summable u

Tactic:
simpa using

Goal state after:
z τ : ℂ
hτ : 0 < τ.im
T : ℝ
hT : 0 < T
hτ' : T < τ.im
S : ℝ
hz : |z.im| < S
V : Set (ℂ × ℂ) := {u | |u.im| < S} ×ˢ {v | T < v.im}
hVo : IsOpen V
u : ℤ → ℝ := fun n ↦ 2 * π * ↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
⊢ Summable fun n ↦ 2 * (π * (↑|n| * rexp (-π * (T * ↑n ^ 2 - 2 * (S * ↑|n|)))))
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ ↑P.k - 0 ≠ 0

Tactic:
simpa using

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ ¬P.k = 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a t : ℝ
ht : 0 < t
this :
  ∀ (n : ℤ), cexp (-(↑π * (↑n + ↑a) ^ 2 * ↑t)) = cexp (-(↑π * ↑a ^ 2 * ↑t)) * jacobiTheta₂_term n (↑a * I * ↑t) (I * ↑t)
⊢ HasSum (fun x ↦ ↑(rexp (-π * (↑x + a) ^ 2 * t))) (cexp (-↑π * ↑a ^ 2 * ↑t) * jacobiTheta₂ (↑a * I * ↑t) (I * ↑t))

Tactic:
simpa using

Goal state after:
a t : ℝ
ht : 0 < t
this :
  ∀ (n : ℤ), cexp (-(↑π * (↑n + ↑a) ^ 2 * ↑t)) = cexp (-(↑π * ↑a ^ 2 * ↑t)) * jacobiTheta₂_term n (↑a * I * ↑t) (I * ↑t)
⊢ HasSum (fun x ↦ cexp (-(↑π * ↑a ^ 2 * ↑t)) * jacobiTheta₂_term x (↑a * I * ↑t) (I * ↑t))
    (cexp (-(↑π * ↑a ^ 2 * ↑t)) * jacobiTheta₂ (↑a * I * ↑t) (I * ↑t))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a t : ℝ
ht : 0 < t
this : ∀ (n : ℤ), cexp (2 * ↑π * I * ↑a * ↑n) * cexp (-(↑π * ↑n ^ 2 * ↑t)) = jacobiTheta₂_term n (↑a) (I * ↑t)
⊢ HasSum (fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) (jacobiTheta₂ (↑a) (I * ↑t))

Tactic:
simpa using

Goal state after:
a t : ℝ
ht : 0 < t
this : ∀ (n : ℤ), cexp (2 * ↑π * I * ↑a * ↑n) * cexp (-(↑π * ↑n ^ 2 * ↑t)) = jacobiTheta₂_term n (↑a) (I * ↑t)
⊢ HasSum (fun n ↦ jacobiTheta₂_term n (↑a) (I * ↑t)) (jacobiTheta₂ (↑a) (I * ↑t))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case pos
t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
k : ℤ
⊢ HasSum (fun n ↦ if ↑n + ↑k = 0 then 0 else rexp (-π * (↑n + ↑k) ^ 2 * t)) (evenKernel (↑↑k) t - 1)

Tactic:
simpa using

Goal state after:
case pos
t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
k : ℤ
⊢ HasSum (fun n ↦ if n = -k then 0 else rexp (-(π * ↑(n + k) ^ 2 * t))) (evenKernel (↑↑k) t - 1)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a t : ℝ
ht : 0 < t
this✝ : (a : Prop) → Decidable a
h : ¬∃ n, ↑n = a
this : ∀ (n : ℤ), ↑n + a ≠ 0
⊢ HasSum (fun n ↦ if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t - 0)

Tactic:
simpa using

Goal state after:
a t : ℝ
ht : 0 < t
this✝ : (a : Prop) → Decidable a
h : ¬∃ n, ↑n = a
this : ∀ (n : ℤ), ↑n + a ≠ 0
⊢ HasSum (fun n ↦ rexp (-(π * (↑n + a) ^ 2 * t))) (evenKernel (↑a) t)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case neg
a t : ℝ
ht : 0 < t
this : (a : Prop) → Decidable a
h : ¬∃ n, ↑n = a
⊢ HasSum (fun n ↦ if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t - 0)

Tactic:
· suffices ∀ (n : ℤ), n + a ≠ 0 by simpa [this] using hasSum_int_evenKernel a ht
    contrapose! h
    let ⟨n, hn⟩ := h
    exact ⟨-n, by simpa [neg_eq_iff_add_eq_zero]⟩

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a t : ℝ
ht : 0 < t
⊢ HasSum (fun n ↦ if n = 0 then 0 else cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t)))
    (↑(cosKernel (↑a) t) - 1)

Tactic:
simpa using

Goal state after:
a t : ℝ
ht : 0 < t
⊢ HasSum (fun n ↦ if n = 0 then 0 else cexp (2 * ↑π * I * ↑a * ↑n) * cexp (-(↑π * ↑n ^ 2 * ↑t)))
    (↑(cosKernel (↑a) t) - 1)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: x : ℝ
⊢ oddKernel 0 x = 0

Tactic:
simpa using

Goal state after:
x : ℝ
⊢ oddKernel 0 x = 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: x : ℝ
⊢ sinKernel 0 x = 0

Tactic:
simpa using

Goal state after:
x : ℝ
⊢ sinKernel 0 x = 0
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
⊢ 0 < (-I * τ).re

Tactic:
simpa using

Goal state after:
z τ : ℂ
hτ : 0 < τ.im
⊢ 0 < τ.im
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
r p : ℝ
hp : 0 < p
hp' : (fun x ↦ cosKernel a x - 1) =O[atTop] fun x ↦ rexp (-p * x)
⊢ (fun x ↦ (ofReal ∘ cosKernel a) x - 1) =O[atTop] fun x ↦ x ^ r

Tactic:
simpa using

Goal state after:
a : UnitAddCircle
r p : ℝ
hp : 0 < p
hp' : (fun x ↦ cosKernel a x - 1) =O[atTop] fun x ↦ rexp (-p * x)
⊢ (fun x ↦ ↑(cosKernel a x) - 1) =O[atTop] fun x ↦ x ^ r
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: s : ℂ
⊢ completedRiemannZeta₀ (1 - s) = completedRiemannZeta₀ s

Tactic:
← completedHurwitzZetaEven₀_zero,

Goal state after:
s : ℂ
⊢ completedHurwitzZetaEven₀ 0 (1 - s) = completedRiemannZeta₀ s
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: s : ℂ
⊢ hurwitzZeta 0 s = riemannZeta s

Tactic:
simpa using

Goal state after:
s : ℂ
⊢ hurwitzZetaOdd 0 s = 0
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ riemannZeta s = ∑' (n : ℕ), 1 / ↑n ^ s

Tactic:
simpa using

Goal state after:
s : ℂ
hs : 1 < s.re
⊢ riemannZeta s = ∑' (n : ℕ), 1 / ↑n ^ s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a b : UnitAddCircle
this :
  ∀ (s : ℂ),
    completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
        ((if a = 0 then 1 else 0) - if b = 0 then 1 else 0) / s
⊢ DifferentiableAt ℂ (fun s ↦ completedHurwitzZetaEven a s - completedHurwitzZetaEven b s) 1

Tactic:
rw [funext this]

Goal state after:
a b : UnitAddCircle
this :
  ∀ (s : ℂ),
    completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
      completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
        ((if a = 0 then 1 else 0) - if b = 0 then 1 else 0) / s
⊢ DifferentiableAt ℂ
    (fun x ↦
      completedHurwitzZetaEven₀ a x - completedHurwitzZetaEven₀ b x -
        ((if a = 0 then 1 else 0) - if b = 0 then 1 else 0) / x)
    1
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case refine_2.refine_1
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
h : s ≠ 1
⊢ s / 2 ≠ ↑(1 / 2)

Tactic:
simpa using

Goal state after:
case refine_2.refine_1
a : UnitAddCircle
s : ℂ
hs : s ≠ 0
hs' : s ≠ 1 ∨ a ≠ 0
h : s ≠ 1
⊢ ¬s / 2 = 2⁻¹
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: ⊢ (abscissaOfAbsConv fun n ↦ ↑(μ n)) = 1

Tactic:
simpa using

Goal state after:
⊢ sInf (Set.Ioo 1 ⊤) = 1
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: n : ℕ
χ : DirichletCharacter ℂ n
this : (1 ⍟ fun x ↦ ↑(μ x)) = δ
⊢ (fun n_1 ↦ χ ↑n_1) * 1 ⍟ ((fun n_1 ↦ χ ↑n_1) * fun n ↦ ↑(μ n)) = δ

Tactic:
simpa using

Goal state after:
n : ℕ
χ : DirichletCharacter ℂ n
this : (1 ⍟ fun x ↦ ↑(μ x)) = δ
⊢ (fun x ↦ χ ↑x) * δ = δ
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: h : Summable ({p | Nat.Prime p}.indicator fun n ↦ 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n ↦ 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n ↦ 1 / ↑n)
p : ℕ
hp : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
hp₁ : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow.val
hp₂ : p ∉ k.primesBelow
hpp : Nat.Prime p
⊢ p ∈ {p | k ≤ p}

Tactic:
simpa using

Goal state after:
h : Summable ({p | Nat.Prime p}.indicator fun n ↦ 1 / ↑n)
k : ℕ
hk : ∑' (x : ℕ), ({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator (fun n ↦ 1 / ↑n) x < 1 / 2
h' : Summable (({p | Nat.Prime p} ∩ {p | k ≤ p}).indicator fun n ↦ 1 / ↑n)
p : ℕ
hp : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow \ k.primesBelow
hp₁ : p ∈ (4 ^ (k.primesBelow.card + 1)).succ.primesBelow.val
hp₂ : p ∉ k.primesBelow
hpp : Nat.Prime p
⊢ k ≤ p
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: N : ℕ
hn : N ≠ 0
χ : DirichletCharacter ℂ N
⊢ (abscissaOfAbsConv fun n ↦ χ ↑n) = 1

Tactic:
simpa using

Goal state after:
N : ℕ
hn : N ≠ 0
χ : DirichletCharacter ℂ N
⊢ sInf (Set.Ioo 1 ⊤) = 1
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
n : ℕ
⊢ ‖((fun n ↦ χ ↑n) * f) n‖ ≤ ‖f n‖

Tactic:
simpa using

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
n : ℕ
⊢ ‖χ ↑n‖ * ‖f n‖ ≤ ‖f n‖
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
h : L (fun n ↦ χ ↑n) s = 0
⊢ False

Tactic:
simpa using

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
h : L (fun n ↦ χ ↑n) s = 0
⊢ False
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: s : ℂ
hs : 1 < s.re
h : L (fun n ↦ ↑(ζ n)) s = 0
⊢ False

Tactic:
simpa using

Goal state after:
s : ℂ
hs : 1 < s.re
h : L (fun n ↦ ↑(ζ n)) s = 0
⊢ False
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: x : ℝ
hx : 1 < x
⊢ 1 < (↑x).re

Tactic:
simpa using

Goal state after:
x : ℝ
hx : 1 < x
⊢ 1 < x
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: x : ℝ
hx : 1 < x
hx' : 1 < (↑x).re
⊢ abscissaOfAbsConv 1 < ↑x

Tactic:
simpa using

Goal state after:
x : ℝ
hx : 1 < x
hx' : 1 < (↑x).re
⊢ 1 < ↑x
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: n : ℕ
⊢ ((fun n ↦ ↑(Λ n)) ⍟ fun n ↦ ↑(ζ n)) n = Complex.log ↑n

Tactic:
simpa using

Goal state after:
n : ℕ
⊢ (∑ x ∈ n.divisorsAntidiagonal, if x.2 = 0 then 0 else ↑(Λ x.1)) = Complex.log ↑n
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: s : ℂ
hs : 1 < s.re
hf : Summable fun x ↦ ‖term (logMul 1) s x‖
n : ℕ
⊢ ‖(fun n ↦ ↑(Λ n)) n‖ ≤ ‖Complex.log ↑n‖

Tactic:
simpa using

Goal state after:
s : ℂ
hs : 1 < s.re
hf : Summable fun x ↦ ‖term (logMul 1) s x‖
n : ℕ
⊢ Λ n ≤ Real.log ↑n
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: b p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_int 1 ↑b =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ ‖oddKernel (↑b) t‖ ≤ HurwitzKernelBounds.F_int 1 (↑b) t

Tactic:
simpa using

Goal state after:
b p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_int 1 ↑b =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
⊢ |∑' (b_1 : ℤ), (↑b_1 + b) * rexp (-(π * (↑b_1 + b) ^ 2 * t))| ≤ ∑' (n : ℤ), |↑n + b| * rexp (-(π * (↑n + b) ^ 2 * t))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun s ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : 0 ≠ 1
S_nhds : {1}ᶜ ∈ 𝓝 0
x : ℂ
⊢ x = 1 / x⁻¹

Tactic:
← one_div,

Goal state after:
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun s ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : 0 ≠ 1
S_nhds : {1}ᶜ ∈ 𝓝 0
x : ℂ
⊢ x = 1 / (1 / x)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case inr
a : UnitAddCircle
h : a ≠ 0 ∨ 0 ≠ 0
⊢ Function.update (fun s ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0 (if a = 0 then -1 / 2 else 0) 0 =
    completedHurwitzZetaEven a 0 / Gammaℝ 0

Tactic:
simpa using

Goal state after:
case inr
a : UnitAddCircle
h : a ≠ 0 ∨ 0 ≠ 0
⊢ ¬a = 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : (fun x ↦ ‖oddKernel a x‖) =O[atTop] fun x ↦ rexp (-v * x)
⊢ (fun x ↦ ‖(ofReal ∘ oddKernel a) x - 0‖) =O[atTop] fun x ↦ x ^ r

Tactic:
simpa using

Goal state after:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : (fun x ↦ ‖oddKernel a x‖) =O[atTop] fun x ↦ rexp (-v * x)
⊢ oddKernel a =O[atTop] fun x ↦ x ^ r
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : (fun x ↦ ‖sinKernel a x‖) =O[atTop] fun x ↦ rexp (-v * x)
⊢ (fun x ↦ ‖(ofReal ∘ sinKernel a) x - 0‖) =O[atTop] fun x ↦ x ^ r

Tactic:
simpa using

Goal state after:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : (fun x ↦ ‖sinKernel a x‖) =O[atTop] fun x ↦ rexp (-v * x)
⊢ sinKernel a =O[atTop] fun x ↦ x ^ r
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
⊢ Tendsto (fun s ↦ hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) (𝓝 1) (𝓝 (hurwitzZetaEven a 1))

Tactic:
simpa using

Goal state after:
a : UnitAddCircle
⊢ Tendsto (fun s ↦ hurwitzZetaEven a s - (s - 1)⁻¹ / s.Gammaℝ) (𝓝 1) (𝓝 (hurwitzZetaEven a 1))
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
hs : s ≠ 0
m n : ℕ
⊢ ↑(m * n) ^ (-s) = ↑m ^ (-s) * ↑n ^ (-s)

Tactic:
simpa using

Goal state after:
s : ℂ
hs : s ≠ 0
m n : ℕ
⊢ (↑m * ↑n) ^ (-s) = ↑m ^ (-s) * ↑n ^ (-s)