mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ClassNumber.Finite

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr : abv ((Algebra.norm R) (r • a' - b' • q)) < abv ((Algebra.norm R) ((algebraMap R S) b'))
⊢ abv ((Algebra.norm R) (r • (b * a') - b' • (q * b))) = abv ((Algebra.norm R) (r • a' * b - b' • q * b))

Tactic:
mul_comm b a',

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : EuclideanDomain R
inst✝⁷ : CommRing S
inst✝⁶ : IsDomain S
inst✝⁵ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst✝² : Infinite R
inst✝¹ : DecidableEq R
inst✝ : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr : abv ((Algebra.norm R) (r • a' - b' • q)) < abv ((Algebra.norm R) ((algebraMap R S) b'))
⊢ abv ((Algebra.norm R) (r • (a' * b) - b' • (q * b))) = abv ((Algebra.norm R) (r • a' * b - b' • q * b))
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ (√x - 2) / log 2 ^ 2 + (x - √x) / log √x ^ 2 ≤ 4 * x / log x ^ 2 + √x / log 2 ^ 2

Tactic:
log_sqrt (by linarith),

Goal state after:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
⊢ (√x - 2) / log 2 ^ 2 + (x - √x) / (log x / 2) ^ 2 ≤ 4 * x / log x ^ 2 + √x / log 2 ^ 2
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
⊢ Fintype.card (Fin pb.dim) = Fintype.card (L →ₐ[K] E)

Tactic:
Fintype.card_fin,

Goal state after:
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun a b ↦ Classical.propDecidable (a = b)
⊢ pb.dim = Fintype.card (L →ₐ[K] E)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: d x y : ℤ
⊢ x * x - y * (d * y) = 1 ↔ x * x + -(y * (d * y)) = 1

Tactic:
ring_nf

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝¹ x✝ : Poly α
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
by ext; simp_rw [mul_apply, mul_comm]

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e_a
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) * ↑p ^ p ^ k =
    ↑(p ^ k.succ) ^ (p ^ k * (p - 1))
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))

Tactic:
cast_pow,

Goal state after:
case e_a
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) ≠ 2
hne : NeZero ↑(p ^ (k + 1))
mf : Module.Finite K L
se : Algebra.IsSeparable K L
hp2 : p = 2 → k ≠ 0
H :
  (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) * ↑p ^ p ^ k =
    (↑p ^ k.succ) ^ (p ^ k * (p - 1))
hnorm : (Algebra.norm K) (ζ ^ p ^ k - 1) = ↑p ^ p ^ k
⊢ (Algebra.norm K) ((aeval ζ) (derivative (cyclotomic (p ^ (k + 1)) K))) = ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n k : ℕ
⊢ yn a1 n ∣ yn a1 (n * (k + 1))

Tactic:
rw [Nat.mul_succ, yn_add]

Goal state after:
a : ℕ
a1 : 1 < a
n k : ℕ
⊢ yn a1 n ∣ xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case succ
a : ℕ
a1 : 1 < a
n k : ℕ
hx : xn a1 (n * (k + 1)) ≡ xn a1 n ^ (k + 1) [MOD yn a1 n ^ 2]
hy : yn a1 (n * (k + 1)) ≡ (k + 1) * xn a1 n ^ (k + 1 - 1) * yn a1 n [MOD yn a1 n ^ 3]
L :
  xn a1 (n * (k + 1)) * xn a1 n + d a1 * yn a1 (n * (k + 1)) * yn a1 n ≡ xn a1 n ^ (k + 1) * xn a1 n + 0 [MOD
    yn a1 n ^ 2]
⊢ (k + 1) * xn a1 n ^ k * yn a1 n * xn a1 n = (k + 1) * (xn a1 n ^ k * xn a1 n) * yn a1 n

Tactic:
ring_nf

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

Goal state before:
pp: case mp
d : ℤ
hd : d < 0
z : ℤ√d
⊢ z.norm = 0 → z = 0

Tactic:
intro h
    rw [norm_def, sub_eq_add_neg, mul_assoc] at h
    have left := mul_self_nonneg z.re
    have right := neg_nonneg.mpr (mul_nonpos_of_nonpos_of_nonneg hd.le (mul_self_nonneg z.im))
    obtain ⟨ha, hb⟩ := (add_eq_zero_iff_of_nonneg left right).mp h
    ext <;> apply eq_zero_of_mul_self_eq_zero
    · exact ha
    · rw [neg_eq_zero, mul_eq_zero] at hb
      exact hb.resolve_left hd.ne

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case re
a : ℕ
a1 : 1 < a
n : ℕ
⊢ (↑(xn a1 n) * ↑a + (↑a * ↑a - 1) * ↑(yn a1 n)) * ↑a + (↑a * ↑a - 1) * (↑(xn a1 n) + ↑(yn a1 n) * ↑a) + ↑(xn a1 n) =
    2 * ↑a * (↑(xn a1 n) * ↑a + (↑a * ↑a - 1) * ↑(yn a1 n))

Tactic:
ring_nf

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case im
a : ℕ
a1 : 1 < a
n : ℕ
⊢ ↑(xn a1 n) * ↑a + (↑a * ↑a - 1) * ↑(yn a1 n) + (↑(xn a1 n) + ↑(yn a1 n) * ↑a) * ↑a + ↑(yn a1 n) =
    2 * ↑a * (↑(xn a1 n) + ↑(yn a1 n) * ↑a)

Tactic:
ring_nf

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Duality

Goal state before:
pp: case refine_1
M : Type u_1
R : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommRing R
a : Mˣ
x✝ : ∃ χ, χ ↑a ≠ 1
χ : MulChar M R
hχ : ↑(χ.toUnitHom a) = ↑1
⊢ χ ↑a = 1

Tactic:
coe_toUnitHom

Goal state after:
case refine_1
M : Type u_1
R : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommRing R
a : Mˣ
x✝ : ∃ χ, χ ↑a ≠ 1
χ : MulChar M R
hχ : χ ↑a = ↑1
⊢ χ ↑a = 1
Module: Mathlib.NumberTheory.MulChar.Duality

Goal state before:
pp: case pos
M : Type u_1
R : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : CommRing R
inst✝² : Finite M
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
inst✝ : Nontrivial R
a : M
ha : a ≠ 1
hu : IsUnit a
⊢ ∃ χ, χ a ≠ 1

pp: case neg
M : Type u_1
R : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : CommRing R
inst✝² : Finite M
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
inst✝ : Nontrivial R
a : M
ha : a ≠ 1
hu : ¬IsUnit a
⊢ ∃ χ, χ a ≠ 1

Tactic:
· refine (exists_apply_ne_one_iff_exists_monoidHom hu.unit).mpr ?_
    refine CommGroup.exists_apply_ne_one_of_hasEnoughRootsOfUnity Mˣ R ?_
    contrapose ha
    rw [← hu.unit_spec, ha, Units.val_eq_one]

Goal state after:
case neg
M : Type u_1
R : Type u_2
inst✝⁴ : CommMonoid M
inst✝³ : CommRing R
inst✝² : Finite M
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
inst✝ : Nontrivial R
a : M
ha : a ≠ 1
hu : ¬IsUnit a
⊢ ∃ χ, χ a ≠ 1
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: case pos.right
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n ↦ ‖f (p ^ n)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
⊢ HasSum (fun m ↦ f ↑m) (∏ x ∈ insert p ({p ∈ s | Nat.Prime p}), ∑' (n : ℕ), f (x ^ n))

Tactic:
· have hp' : p ∉ {p ∈ s | p.Prime} := mt (mem_of_mem_filter p) hp
        rw [prod_insert hp', ← (equivProdNatFactoredNumbers hpp hp).hasSum_iff, Function.comp_def]
        conv =>
          enter [1, x]
          rw [equivProdNatFactoredNumbers_apply', factoredNumbers.map_prime_pow_mul hmul hpp hp]
        have : T3Space R := instT3Space -- speeds up the following
        apply (hsum hpp).of_norm.hasSum.mul ih.2
        -- `exact summable_mul_of_summable_norm (hsum hpp) ih.1` gives a time-out
        apply summable_mul_of_summable_norm (hsum hpp) ih.1

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x ↦ ‖f x‖
hf₀ : f 0 = 0
⊢ Tendsto (fun n ↦ ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) atTop (𝓝 (∑' (n : ℕ), f n))

Tactic:
by
  have := (eulerProduct_hasProd_mulIndicator hf₁ hmul hsum hf₀).tendsto_prod_nat
  let F : ℕ → R := fun p ↦ ∑' (e : ℕ), f (p ^ e)
  have H (n : ℕ) : ∏ i ∈ range n, Set.mulIndicator {p | Nat.Prime p} F i =
                     ∏ p ∈ primesBelow n, ∑' (e : ℕ), f (p ^ e) :=
    prod_mulIndicator_eq_prod_filter (range n) (fun _ ↦ F) (fun _ ↦ {p | Nat.Prime p}) id
  simpa only [F, H]

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

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n ↦ ‖term f (↑x) n‖
h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x ↦ term f x n) S
h₂ : IsOpen S
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Tactic:
have h₃ (n z) (hz : z ∈ S) : ‖term f z n‖ ≤ ‖term f x n‖ :=
    norm_term_le_of_re_le_re f (by simpa using! (hxy.trans hz).le) n

Goal state after:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n ↦ ‖term f (↑x) n‖
h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x ↦ term f x n) S
h₂ : IsOpen S
h₃ : ∀ (n : ℕ), ∀ z ∈ S, ‖term f z n‖ ≤ ‖term f (↑x) n‖
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
Module: Mathlib.NumberTheory.LSeries.Deriv

Goal state before:
pp: f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n ↦ ‖term f (↑x) n‖
h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x ↦ term f x n) S
h₂ : IsOpen S
h₃ : ∀ (n : ℕ), ∀ z ∈ S, ‖term f z n‖ ≤ ‖term f (↑x) n‖
H : HasSum (fun i ↦ deriv (fun x ↦ term f x i) s) (deriv (fun w ↦ ∑' (i : ℕ), term f w i) s)
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s

Tactic:
(hasDerivAt_term f _ _).deriv

Goal state after:
f : ℕ → ℂ
s : ℂ
h : abscissaOfAbsConv f < ↑s.re
x : ℝ
hxs : x < s.re
hf : LSeriesSummable f ↑x
y : ℝ
hxy : x < y
hys : y < s.re
S : Set ℂ := {z | y < z.re}
h₀ : Summable fun n ↦ ‖term f (↑x) n‖
h₁ : ∀ (n : ℕ), DifferentiableOn ℂ (fun x ↦ term f x n) S
h₂ : IsOpen S
h₃ : ∀ (n : ℕ), ∀ z ∈ S, ‖term f z n‖ ≤ ‖term f (↑x) n‖
H : HasSum (fun i ↦ -term (logMul f) s i) (deriv (fun w ↦ ∑' (i : ℕ), term f w i) s)
⊢ LSeriesSummable (logMul f) s ∧ HasDerivAt (LSeries f) (-LSeries (logMul f) s) s
Module: Mathlib.NumberTheory.LSeries.Positivity

Goal state before:
pp: 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}
⊢ 0 < f ↑y

Tactic:
have hfx : 0 < f (max x y + 1) := by
    simpa only [hf' hys, ofReal_add, ofReal_one] using positive ha₀ ha₁ hxy'

Goal state after:
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)
⊢ 0 < f ↑y
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

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

Tactic:
convert! h₁ using 1

Goal state after:
case e'_3
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
h₁ : ↑u + -(1 / 2) < ξ
hξ₁ : ⌊ξ⌋ = u - 1
Hξ : ξ ≠ ↑⌊ξ⌋
⊢ ↑u - (1 - 2⁻¹) = ↑u + -(1 / 2)
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)
⊢ 0 < 2 * (↑q.den * ↑q.den) - ↑q.den * (2 * ↑q.den - 1)

Tactic:
ring_nf

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)
⊢ 0 < ↑q.den
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: n : ℤ
z τ : ℂ
⊢ ‖cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)‖ = rexp (-π * ↑n ^ 2 * τ.im - 2 * π * ↑n * z.im)

Tactic:
Complex.norm_exp,

Goal state after:
n : ℤ
z τ : ℂ
⊢ rexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ).re = rexp (-π * ↑n ^ 2 * τ.im - 2 * π * ↑n * z.im)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: n : ℤ
z τ : ℂ
⊢ rexp (-(π * (2 * ↑n) * z.im) + -(π * ↑n ^ 2 * τ.im)) = rexp (-π * ↑n ^ 2 * τ.im - 2 * π * ↑n * z.im)

Tactic:
ring_nf

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

Goal state before:
pp: case convert_3.inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : IntegrableOn (fun x ↦ ↑(rexp (-(p i * x))) * ↑(p i * x) ^ (s - 1)) (Ioi 0) volume
t : ℝ
ht : 0 < t
⊢ 1 / ↑(p i) ^ (s - 1) * ↑(p i * t) ^ (s - 1) * ↑(rexp (-(p i * t))) = ↑t ^ (s - 1) * ↑(rexp (-(p i * t)))

Tactic:
ofReal_mul

Goal state after:
case convert_3.inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : IntegrableOn (fun x ↦ ↑(rexp (-(p i * x))) * ↑(p i * x) ^ (s - 1)) (Ioi 0) volume
t : ℝ
ht : 0 < t
⊢ 1 / ↑(p i) ^ (s - 1) * (↑(p i) * ↑t) ^ (s - 1) * ↑(rexp (-(p i * t))) = ↑t ^ (s - 1) * ↑(rexp (-(p i * 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 only [pow_zero, one_mul] using norm_jacobiTheta₂_term_le hτ le_rfl le_rfl

Goal state after:
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 + ↑n * (-π * t))

Tactic:
ring_nf

Goal state after:
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 (↑n * (-π * t) + -π * a ^ 2 * t)

Tactic:
ring_nf

Goal state after:
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 + ↑n * (-π * t))

Tactic:
ring_nf

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
i : ι
this : a i / ↑(π * q i) ^ s = ↑π ^ (-s) * a i / ↑(q i) ^ s
⊢ ↑π ^ (-s) * Complex.Gamma s * (a i / ↑(q i) ^ s) = Complex.Gamma s * (↑π ^ (-s) * a i / ↑(q i) ^ s)

Tactic:
ring_nf

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

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

Tactic:
enter [t]; rw [← mul_one (rexp _)]

Goal state after:
a : ℝ
ha : 0 ≤ a
aux' : (fun t ↦ ((1 - rexp (-π * t)) ^ 2)⁻¹) =O[atTop] fun x ↦ 1
ha' : 0 < a
t : ℝ
| rexp (-(π * a ^ 2) * t) * 1
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
x ξ : ℝ
⊢ cexp (-↑π * I * (I * ↑x + 2 * (↑ξ * I * ↑x))) = ↑(rexp (π * (x + 2 * ξ * x)))

Tactic:
ring_nf

Goal state after:
a : UnitAddCircle
x ξ : ℝ
⊢ cexp (-(↑π * I ^ 2 * ↑x) - ↑π * I ^ 2 * ↑x * ↑ξ * 2) = ↑(rexp (π * x + π * x * ξ * 2))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case inl
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)

Tactic:
evenKernel_undef _ hx,

Goal state after:
case inl
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ 0 = 1 / x ^ (1 / 2) * cosKernel a (1 / x)
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case e'_6
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs' : 0 < (s / 2).re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i ^ 2 = 0 then 0 else a i * ↑(rexp (-π * r i ^ 2 * t))) (F t)
i : ι
⊢ ↑|r i| ^ s = ↑|r i| ^ (↑2 * (s / 2))

Tactic:
ring_nf

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
n : ℤ
⊢ cexp (2 * ↑π * I * ↑n * (z + τ) + ↑π * I * ↑n ^ 2 * τ) =
    cexp (-↑π * I * (τ + 2 * z) + (2 * ↑π * I * (↑n + ↑1) * z + ↑π * I * (↑n + ↑1) ^ 2 * τ))

Tactic:
ring_nf

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

Goal state before:
pp: a t : ℝ
ht : 0 < t
n : ℤ
⊢ cexp (2 * ↑π * I * ↑a * ↑n + -(↑π * ↑n ^ 2 * ↑t)) = cexp (2 * ↑π * I * ↑n * ↑a + ↑π * I * ↑n ^ 2 * (I * ↑t))

Tactic:
ring_nf

Goal state after:
a t : ℝ
ht : 0 < t
n : ℤ
⊢ cexp (↑π * I * ↑a * ↑n * 2 - ↑π * ↑n ^ 2 * ↑t) = cexp (↑π * I * ↑a * ↑n * 2 + ↑π * I ^ 2 * ↑n ^ 2 * ↑t)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a t : ℝ
ht : 0 < t
⊢ HasSum (fun x ↦ ↑(2 * Real.cos (2 * π * a * (↑x + 1)) * rexp (-π * (↑x + 1) ^ 2 * t))) (↑(cosKernel (↑a) t) - 1)

Tactic:
have := (hasSum_int_cosKernel a ht).nat_add_neg

Goal state after:
a t : ℝ
ht : 0 < t
this :
  HasSum
    (fun n ↦
      cexp (2 * ↑π * I * ↑a * ↑↑n) * ↑(rexp (-π * ↑↑n ^ 2 * t)) +
        cexp (2 * ↑π * I * ↑a * ↑(-↑n)) * ↑(rexp (-π * ↑(-↑n) ^ 2 * t)))
    (↑(cosKernel (↑a) t) + cexp (2 * ↑π * I * ↑a * ↑0) * ↑(rexp (-π * ↑0 ^ 2 * t)))
⊢ HasSum (fun x ↦ ↑(2 * Real.cos (2 * π * a * (↑x + 1)) * rexp (-π * (↑x + 1) ^ 2 * t))) (↑(cosKernel (↑a) t) - 1)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case e_f
z τ : ℂ
n : ℤ
⊢ 2 * ↑π * I * -↑n * cexp (2 * ↑π * I * -↑n * -z + ↑π * I * (-↑n) ^ 2 * τ) =
    -(2 * ↑π * I * ↑n) * cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ)

Tactic:
ring_nf

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case e_f
z τ : ℂ
n : ℤ
⊢ -(↑2 * ↑π * -I * ↑↑n * cexp (↑2 * ↑π * -I * ↑↑n * (starRingEnd ℂ) z + ↑π * -I * ↑↑n ^ 2 * (starRingEnd ℂ) τ)) =
    ↑2 * ↑π * I * ↑↑n * cexp (↑2 * ↑π * I * ↑↑n * -(starRingEnd ℂ) z + ↑π * I * ↑↑n ^ 2 * -(starRingEnd ℂ) τ)

Tactic:
ring_nf

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
n : ℤ
⊢ cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ) = cexp (-↑π * (-I * τ) * ↑n ^ 2 + 2 * ↑π * (I * z) * ↑n)

Tactic:
ring_nf

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case e_a.e_f
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
n : ℤ
⊢ (↑n + I ^ 2 * z) ^ 2 / τ = I ^ 2 * (-z ^ 2 + ↑n * (z * 2 + -↑n)) / τ

Tactic:
ring_nf

Goal state after:
case e_a.e_f
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
n : ℤ
⊢ ↑n * I ^ 2 * z * τ⁻¹ * 2 + ↑n ^ 2 * τ⁻¹ + I ^ 4 * z ^ 2 * τ⁻¹ =
    ↑n * I ^ 2 * z * τ⁻¹ * 2 - ↑n ^ 2 * I ^ 2 * τ⁻¹ - I ^ 2 * z ^ 2 * τ⁻¹
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ hurwitzZetaEven a s = (hurwitzZetaEven a s + hurwitzZetaOdd a s + (hurwitzZetaEven a s + -hurwitzZetaOdd a s)) / 2

Tactic:
ring_nf

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ hurwitzZetaOdd a s = (hurwitzZetaEven a s + hurwitzZetaOdd a s - (hurwitzZetaEven a s + -hurwitzZetaOdd a s)) / 2

Tactic:
ring_nf

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case e_a.e_f
z τ : ℂ
hτ : 0 < τ.im
h2 : 0 < (-I * τ).re
n : ℤ
⊢ ↑n * -1 * z * τ⁻¹ * 2 + ↑n ^ 2 * τ⁻¹ + 1 * z ^ 2 * τ⁻¹ = ↑n * -1 * z * τ⁻¹ * 2 - ↑n ^ 2 * -1 * τ⁻¹ - -1 * z ^ 2 * τ⁻¹

Tactic:
ring_nf

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ cosZeta a s = (cosZeta a s + I * sinZeta a s + (cosZeta a s + I * -sinZeta a s)) / 2

Tactic:
ring_nf

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ (cexp (-↑π * I * z ^ 2 * τ⁻¹) * (-↑π * I * (↑2 * z ^ (2 - 1)) * τ⁻¹) * jacobiTheta₂ (z * τ⁻¹) (-1 * τ⁻¹) +
        cexp (-↑π * I * z ^ 2 * τ⁻¹) * (1 * τ⁻¹ * jacobiTheta₂' (z * τ⁻¹) (-1 * τ⁻¹))) *
      (1 / (-I * τ) ^ (1 / 2)) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 * τ⁻¹) * τ⁻¹ *
      (jacobiTheta₂' (z * τ⁻¹) (-1 * τ⁻¹) - 2 * ↑π * I * z * jacobiTheta₂ (z * τ⁻¹) (-1 * τ⁻¹))

Tactic:
ring_nf

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
x y z : ℂ
⊢ 2 * x * Complex.Gamma s * ((y + z) / 2) * cosZeta a s + 2 * x * Complex.Gamma s * ((z - y) * I / 2) * sinZeta a s =
    x * Complex.Gamma s * (z * (cosZeta a s + I * sinZeta a s) + y * (cosZeta a s + I * -sinZeta a s))

Tactic:
ring_nf

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

Goal state before:
pp: a x : ℝ
hx : 0 < x
h1 : HasSum (fun n ↦ jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
h2 : HasSum (fun n ↦ jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x))
n : ℤ
⊢ -↑π * (↑n + ↑a) ^ 2 = -↑π * ↑a ^ 2 + (2 * ↑π * ↑n * ↑a * -1 + ↑π * ↑n ^ 2 * -1)

Tactic:
ring_nf

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ completedRiemannZeta s = ↑π ^ (-s / 2) * Gamma (s / 2) * ∑' (n : ℕ), 1 / ↑n ^ s

Tactic:
have := (hasSum_nat_completedCosZeta 0 hs).tsum_eq.symm

Goal state after:
s : ℂ
hs : 1 < s.re
this : completedCosZeta (↑0) s = ∑' (b : ℕ), if b = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * π * 0 * ↑b)) / ↑b ^ s
⊢ completedRiemannZeta s = ↑π ^ (-s / 2) * Gamma (s / 2) * ∑' (n : ℕ), 1 / ↑n ^ s