mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
sum_eq : ∀ t ∈ univ \ {0}, (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t
t : F
| ∑ x, χ t * (χ x * (φ t * φ (1 - x)))

Tactic:
2,

Goal state after:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ φ : MulChar F R
h : χ * φ ≠ 1
ψ : AddChar F R
sum_eq : ∀ t ∈ univ \ {0}, (∑ x, χ x * φ (t - x)) * ψ t = (∑ y, χ (t * y) * φ (t - t * y)) * ψ t
t : F
| fun x ↦ χ t * (χ x * (φ t * φ (1 - x)))
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective ⇑(algebraMap F' FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
Hcard : ↑(Fintype.card F) ≠ 0
H : gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ ≠ 0
⊢ gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ *
      (jacobiSum (χ.ringHomComp (algebraMap F' FF')) (φ.ringHomComp (algebraMap F' FF')) *
        jacobiSum (χ⁻¹.ringHomComp (algebraMap F' FF')) (φ⁻¹.ringHomComp (algebraMap F' FF'))) =
    gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ * (algebraMap F' FF') ↑(Fintype.card F)

Tactic:
mul_mul_mul_comm,

Goal state after:
F : Type u_1
F' : Type u_2
inst✝² : Fintype F
inst✝¹ : Field F
inst✝ : Field F'
h : ringChar F' ≠ ringChar F
χ φ : MulChar F F'
hχ : χ ≠ 1
hφ : φ ≠ 1
hχφ : χ * φ ≠ 1
n : ℕ+
hp : Nat.Prime (ringChar F)
hc : Fintype.card F = ringChar F ^ ↑n
ψ : PrimitiveAddChar F F' := FiniteField.primitiveChar F F' h
FF' : Type u_2 := CyclotomicField (↑ψ.n) F'
χ' : MulChar F FF' := χ.ringHomComp (algebraMap F' FF')
φ' : MulChar F FF' := φ.ringHomComp (algebraMap F' FF')
hinj : Function.Injective ⇑(algebraMap F' FF')
Hχφ : χ' * φ' ≠ 1
Hχφ' : χ'⁻¹ * φ'⁻¹ ≠ 1
Hχ : χ' ≠ 1
Hφ : φ' ≠ 1
Hcard : ↑(Fintype.card F) ≠ 0
H : gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ ≠ 0
⊢ gaussSum (χ' * φ') ψ.char * jacobiSum (χ.ringHomComp (algebraMap F' FF')) (φ.ringHomComp (algebraMap F' FF')) *
      (gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ *
        jacobiSum (χ⁻¹.ringHomComp (algebraMap F' FF')) (φ⁻¹.ringHomComp (algebraMap F' FF'))) =
    gaussSum (χ' * φ') ψ.char * gaussSum (χ' * φ')⁻¹ ψ.char⁻¹ * (algebraMap F' FF') ↑(Fintype.card F)
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
a : 𝓞 K
ha : mulHeight ![↑a, ↑n] ≤ B
⊢ ∏ v, (⨆ i, v (![↑a, ↑n] i)) ^ v.mult ≤ ↑n ^ totalWeight K * B

Tactic:
rw [mulHeight_eq <| by simp [hn], mul_comm] at ha

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn : n ≠ 0
B : ℝ
a : 𝓞 K
ha : (∏ᶠ (v : FinitePlace K), ⨆ i, v (![↑a, ↑n] i)) * ∏ v, (⨆ i, v (![↑a, ↑n] i)) ^ v.mult ≤ B
⊢ ∏ v, (⨆ i, v (![↑a, ↑n] i)) ^ v.mult ≤ ↑n ^ totalWeight K * B
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case neg.refine_1
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : ¬χ = 1
hψ₀ : ¬ψ = 1
this : NeZero n
H : ∀ (x : F), ∃ z ∈ ℤ[μ], (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2
Hcs : ∀ (x : F), ⋯.choose ∈ ℤ[μ] ∧ (χ x - 1) * (ψ (1 - x) - 1) = ⋯.choose * (μ - 1) ^ 2
⊢ -↑q * z₁ + ∑ x ∈ univ \ {0, 1}, ⋯.choose ∈ ℤ[μ]

Tactic:
refine Subalgebra.add_mem _ (Subalgebra.mul_mem _ (Subalgebra.neg_mem _ ?_) hz₁) ?_
      · exact Subalgebra.natCast_mem ..
      · exact Subalgebra.sum_mem _ fun x _ ↦ (Hcs x).1

Goal state after:
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) }.coeff ↑i = g i

pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) }.degree < f.degree

Tactic:
Polynomial.coeff

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
⊢ (AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g)).coeff ↑i = g i

R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) }.degree < f.degree
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
m : ℕ
hm : f.natDegree ≤ m
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) }.coeff m = 0

Tactic:
Polynomial.coeff

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
m : ℕ
hm : f.natDegree ≤ m
⊢ (AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g)).coeff m = 0
Module: Mathlib.RingTheory.IsAdjoinRoot

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
m : ℕ
hm : f.natDegree ≤ m
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) }.coeff m = 0

Tactic:
rw [Polynomial.coeff]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
g : Fin f.natDegree →₀ R
a✝ : Nontrivial R
i : Fin f.natDegree
m : ℕ
hm : f.natDegree ≤ m
⊢ (AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g)).coeff m = 0
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : ¬χ = 1
hψ₀ : ¬ψ = 1
this : NeZero n
H : ∀ (x : F), ∃ z ∈ ℤ[μ], (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2
Hcs : ∀ (x : F), ⋯.choose ∈ ℤ[μ] ∧ (χ x - 1) * (ψ (1 - x) - 1) = ⋯.choose * (μ - 1) ^ 2
| 0 + 0 - ↑(n * q + 1) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)

Tactic:
2,

Goal state after:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : ¬χ = 1
hψ₀ : ¬ψ = 1
this : NeZero n
H : ∀ (x : F), ∃ z ∈ ℤ[μ], (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2
Hcs : ∀ (x : F), ⋯.choose ∈ ℤ[μ] ∧ (χ x - 1) * (ψ (1 - x) - 1) = ⋯.choose * (μ - 1) ^ 2
| ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : ¬χ = 1
hψ₀ : ¬ψ = 1
this : NeZero n
H : ∀ (x : F), ∃ z ∈ ℤ[μ], (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2
Hcs : ∀ (x : F), ⋯.choose ∈ ℤ[μ] ∧ (χ x - 1) * (ψ (1 - x) - 1) = ⋯.choose * (μ - 1) ^ 2
| ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1)

Tactic:
2,

Goal state after:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : ¬χ = 1
hψ₀ : ¬ψ = 1
this : NeZero n
H : ∀ (x : F), ∃ z ∈ ℤ[μ], (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2
Hcs : ∀ (x : F), ⋯.choose ∈ ℤ[μ] ∧ (χ x - 1) * (ψ (1 - x) - 1) = ⋯.choose * (μ - 1) ^ 2
| fun x ↦ (χ x - 1) * (ψ (1 - x) - 1)
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case neg.refine_2
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Fintype F
n : ℕ
hn : 2 < n
χ ψ : MulChar F R
μ : R
hχ : χ ^ n = 1
hψ : ψ ^ n = 1
hμ : IsPrimitiveRoot μ n
q : ℕ
hq : Fintype.card F = n * q + 1
z₁ : R
hz₁ : z₁ ∈ ℤ[μ]
Hz₁ : ↑n = z₁ * (μ - 1) ^ 2
hχ₀ : ¬χ = 1
hψ₀ : ¬ψ = 1
this : NeZero n
H : ∀ (x : F), ∃ z ∈ ℤ[μ], (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2
Hcs : ∀ (x : F), ⋯.choose ∈ ℤ[μ] ∧ (χ x - 1) * (ψ (1 - x) - 1) = ⋯.choose * (μ - 1) ^ 2
⊢ 0 + 0 - ↑(n * q + 1) + ∑ x ∈ univ \ {0, 1}, (χ x - 1) * (ψ (1 - x) - 1) =
    -1 + (-↑q * z₁ + ∑ x ∈ univ \ {0, 1}, ⋯.choose) * (μ - 1) ^ 2

Tactic:
conv => enter [1, 2, 2, x]; rw [(Hcs x).2]
      rw [← Finset.sum_mul, Nat.cast_add, Nat.cast_mul, Hz₁]
      ring

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : 1 < s.re
j : ZMod N
this : ↑j.val / ↑N ∈ Set.Icc 0 1
m : ℕ
⊢ Φ j / (↑↑N * ↑((↑j.val + ↑N * ↑m) / ↑N)) ^ s = Φ j / (↑N * (↑j.val + ↑N * ↑m) / ↑N) ^ s

Tactic:
simp only [ofReal_natCast, ofReal_div, ofReal_add, ofReal_mul, mul_div_assoc]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
H :
  (fun s ↦ (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s ↦
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
| ∏ p ∈ N.primeFactors, (1 - (↑p)⁻¹)

Tactic:
2,

Goal state after:
N : ℕ
inst✝ : NeZero N
H :
  (fun s ↦ (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s ↦
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
| fun p ↦ 1 - (↑p)⁻¹
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: case neg
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
h : χ.Odd
⊢ ↑N ^ (s - 1) * I * ZMod.completedLFunction (𝓕 ⇑χ) s = ↑N ^ (s - 1) * -1 / I * ZMod.completedLFunction (𝓕 ⇑χ) s

Tactic:
div_I,

Goal state after:
case neg
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ.IsPrimitive
s : ℂ
hN : N ≠ 1
h_sum : ∑ j, χ j = 0
ε : ℂ := I ^ if χ.Even then 0 else 1
h : χ.Odd
⊢ ↑N ^ (s - 1) * I * ZMod.completedLFunction (𝓕 ⇑χ) s = -(↑N ^ (s - 1) * -1 * I) * ZMod.completedLFunction (𝓕 ⇑χ) s
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case zero
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
⊢ ∀ (x : ℝ), f 0 x = 0

Tactic:
intro x

Goal state after:
case zero
m : ℕ
m0 : m ≠ 0
x✝ : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
x : ℝ
⊢ f 0 x = 0
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: case inl
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
⊢ Φ 0 * hurwitzZeta (toAddCircle 0) (1 - s) =
    Φ 0 *
      ((2 * ↑π) ^ (-s) * Gamma s *
        (cexp (-↑π * I * s / 2) * expZeta (toAddCircle 0) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle 0) s))

Tactic:
rcases hs' with hΦ | hs'

Goal state after:
case inl.inl
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hΦ : Φ 0 = 0
⊢ Φ 0 * hurwitzZeta (toAddCircle 0) (1 - s) =
    Φ 0 *
      ((2 * ↑π) ^ (-s) * Gamma s *
        (cexp (-↑π * I * s / 2) * expZeta (toAddCircle 0) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle 0) s))

case inl.inr
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : s ≠ 1
⊢ Φ 0 * hurwitzZeta (toAddCircle 0) (1 - s) =
    Φ 0 *
      ((2 * ↑π) ^ (-s) * Gamma s *
        (cexp (-↑π * I * s / 2) * expZeta (toAddCircle 0) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle 0) s))
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
| cexp (↑π * (I * s) / 2) * ∑ j, Φ j * expZeta (toAddCircle (-j)) s +
    cexp (-↑π * (I * s) / 2) * ∑ j, Φ (-j) * expZeta (toAddCircle (-j)) s

Tactic:
2,

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : Φ 0 = 0 ∨ s ≠ 1
this :
  ∀ (j : ZMod N),
    Φ j * hurwitzZeta (toAddCircle j) (1 - s) =
      Φ j *
        ((2 * ↑π) ^ (-s) * Gamma s *
          (cexp (-↑π * I * s / 2) * expZeta (toAddCircle j) s + cexp (↑π * I * s / 2) * expZeta (-toAddCircle j) s))
C : ℂ
| cexp (-↑π * (I * s) / 2) * ∑ j, Φ (-j) * expZeta (toAddCircle (-j)) s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n
h2 : 2 * ↑k ≠ 1
h3 : (2 * ↑k).Gammaℂ ≠ 0
⊢ hurwitzZetaEven (↑x) (1 - 2 * ↑k) =
    -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Tactic:
hurwitzZetaEven_one_sub _ h1 (Or.inr h2),

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n
h2 : 2 * ↑k ≠ 1
h3 : (2 * ↑k).Gammaℂ ≠ 0
⊢ 2 * (2 * ↑π) ^ (-(2 * ↑k)) * Complex.Gamma (2 * ↑k) * Complex.cos (↑π * (2 * ↑k) / 2) * cosZeta (↑x) (2 * ↑k) =
    -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
Module: Mathlib.NumberTheory.KummerDedekind

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
mem_norm_factors :
  normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
    normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
⊢ Multiset.map (fun a ↦ ↑a) (normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach =
    Multiset.map (fun a ↦ ↑a) {⟨normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)), mem_norm_factors⟩}

Tactic:
rw [Multiset.attach_map_val, Multiset.map_singleton, Subtype.coe_mk]

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
mem_norm_factors :
  normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
    normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
⊢ normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) =
    {normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))}
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case e_a.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k + 1 ≠ -↑n
h3 : (2 * ↑k + 1).Gammaℂ ≠ 0
⊢ ↑(Real.sin (↑k * π + 1 / 2 * π)) * (-↑1) ^ (k + 1) = -↑1

Tactic:
mul_comm (1 / 2),

Goal state after:
case e_a.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k + 1 ≠ -↑n
h3 : (2 * ↑k + 1).Gammaℂ ≠ 0
⊢ ↑(Real.sin (↑k * π + π * (1 / 2))) * (-↑1) ^ (k + 1) = -↑1
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
⊢ ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m

Tactic:
intro x

Goal state after:
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
x : ℝ
⊢ x ≥ y → (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
⊢ IsPreconnected U

Tactic:
let Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ (if Φ 0 = 0 then ∅ else {1})

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
hs₀ : s ≠ 0 ∨ ∑ j, Φ j = 0
hs₁ : s ≠ 1 ∨ Φ 0 = 0
F : ℂ → ℂ := fun t ↦ completedLFunction Φ (1 - t)
G : ℂ → ℂ := fun t ↦ ↑N ^ (t - 1) * completedLFunction (𝓕 Φ) t
U : Set ℂ := {t | (t ≠ 0 ∨ ∑ j, Φ j = 0) ∧ (t ≠ 1 ∨ Φ 0 = 0)}
hsU : s ∈ U
h2U : 2 ∈ U
hUo : IsOpen U
Uc : Set ℂ := (if ∑ j, Φ j = 0 then ∅ else {0}) ∪ if Φ 0 = 0 then ∅ else {1}
⊢ IsPreconnected U
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ (fun n ↦ 1 / ↑n ^ k * ((fourier ↑n) ↑x + (-1) ^ k * (fourier (-↑n)) ↑x)) = fun n ↦
    1 / ↑↑n ^ k * (fourier ↑n) ↑x + 1 / ↑(-↑n) ^ k * (fourier (-↑n)) ↑x

Tactic:
ext1 n

Goal state after:
case e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * ((fourier ↑n) ↑x + (-1) ^ k * (fourier (-↑n)) ↑x) =
    1 / ↑↑n ^ k * (fourier ↑n) ↑x + 1 / ↑(-↑n) ^ k * (fourier (-↑n)) ↑x
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case e'_5
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun n ↦ ↑(Λ n)) ↑y
⊢ term (fun n ↦ ↑(residueClass a n)) ↑y = {n | ↑n = a}.indicator (term (fun n ↦ ↑(Λ n)) ↑y)

Tactic:
ext1 n

Goal state after:
case e'_5
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun n ↦ ↑(Λ n)) ↑y
n : ℕ
⊢ term (fun n ↦ ↑(residueClass a n)) (↑y) n = {n | ↑n = a}.indicator (term (fun n ↦ ↑(Λ n)) ↑y) n
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ F₀ n
hF₀ : ∀ (p : Nat.Primes), F₀ ↑p = 0
⊢ (F₀ ∘ Subtype.val) ∘ ⇑prodNatEquiv = F'

Tactic:
ext1 n

Goal state after:
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ F₀ n
hF₀ : ∀ (p : Nat.Primes), F₀ ↑p = 0
n : Nat.Primes × ℕ
⊢ ((F₀ ∘ Subtype.val) ∘ ⇑prodNatEquiv) n = F' n
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_5
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x)) = fun n ↦
    1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x + (-1) ^ (2 * k + 1) * (fourier (-↑n)) ↑x)

Tactic:
ext1 n

Goal state after:
case e'_5
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x) =
    1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x + (-1) ^ (2 * k + 1) * (fourier (-↑n)) ↑x)
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
n : ℕ
⊢ ↑(residueClass a n) = (↑q.totient)⁻¹ * ∑ χ, χ a⁻¹ * χ ↑n * ↑(Λ n)

Tactic:
by
  rw [eq_inv_mul_iff_mul_eq₀ <| mod_cast (Nat.totient_pos.mpr q.pos_of_neZero).ne']
  simp +contextual only [residueClass, Set.indicator_apply, Set.mem_ofPred_eq, apply_ite,
    ofReal_zero, mul_zero, ← Finset.sum_mul, sum_char_inv_mul_char_eq ℂ ha n, eq_comm (a := a),
    ite_mul, zero_mul, ↓reduceIte, ite_self]

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

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
⊢ (fun n ↦ ↑(residueClass a n)) = (↑q.totient)⁻¹ • ∑ χ, χ a⁻¹ • fun n ↦ χ ↑n * ↑(Λ n)

Tactic:
ext1 n

Goal state after:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
n : ℕ
⊢ ↑(residueClass a n) = ((↑q.totient)⁻¹ • ∑ χ, χ a⁻¹ • fun n ↦ χ ↑n * ↑(Λ n)) n
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
hs₁ : s ≠ 1
| deriv (LFunction 1) s / LFunction 1 s + LFunction 1 s / ((s - 1) * LFunction 1 s)

Tactic:
2,

Goal state after:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
ha' : IsUnit a⁻¹
hs₁ : s ≠ 1
| LFunction 1 s / ((s - 1) * LFunction 1 s)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_3.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ (cexp (2 * ↑π * I * ↑x✝ * ↑x) - cexp (2 * ↑π * I * -↑x✝ * ↑x)) / 2 / I =
    (cexp (-(2 * ↑π * ↑x✝ * ↑x) * I) - cexp (2 * ↑π * ↑x✝ * ↑x * I)) * I / 2

Tactic:
div_I,

Goal state after:
case e'_3.e_a
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
x✝ : ℕ
⊢ -((cexp (2 * ↑π * I * ↑x✝ * ↑x) - cexp (2 * ↑π * I * -↑x✝ * ↑x)) / 2 * I) =
    (cexp (-(2 * ↑π * ↑x✝ * ↑x) * I) - cexp (2 * ↑π * ↑x✝ * ↑x * I)) * I / 2
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_3
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x) / 2 / I =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))

Tactic:
div_I,

Goal state after:
case e'_3
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
ofReal_two : ↑2 = 2
⊢ -((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x) / 2 * I) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))