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

Goal state before:
pp: K : Type u
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst✝³ : NeZero n₁
inst✝² : NeZero n₂
inst✝¹ : IsCyclotomicExtension {n₁} ℚ ↥F₁
inst✝ : IsCyclotomicExtension {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : ℤ[hζ₁.toInteger] = ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : ℤ[hζ₂.toInteger] = ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr ↥F₁) (NumberField.discr ↥F₂)
this : IsGalois ℚ ↥F₁
⊢ F₁.LinearDisjoint ↥F₂

Tactic:
apply linearDisjoint_of_isGalois_isCoprime_discr

Goal state after:
K : Type u
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst✝³ : NeZero n₁
inst✝² : NeZero n₂
inst✝¹ : IsCyclotomicExtension {n₁} ℚ ↥F₁
inst✝ : IsCyclotomicExtension {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : ℤ[hζ₁.toInteger] = ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : ℤ[hζ₂.toInteger] = ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr ↥F₁) (NumberField.discr ↥F₂)
this : IsGalois ℚ ↥F₁
⊢ IsCoprime (NumberField.discr ↥F₁) (NumberField.discr ↥F₂)
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝²¹ : CommRing A
inst✝²⁰ : Field K
inst✝¹⁹ : CommRing B
inst✝¹⁸ : Field L
inst✝¹⁷ : Algebra A K
inst✝¹⁶ : Algebra B L
inst✝¹⁵ : Algebra A B
inst✝¹⁴ : Algebra K L
inst✝¹³ : Algebra A L
inst✝¹² : IsScalarTower A K L
inst✝¹¹ : IsScalarTower A B L
inst✝¹⁰ : IsDomain A
inst✝⁹ : IsFractionRing A K
inst✝⁸ : FiniteDimensional K L
inst✝⁷ : Algebra.IsSeparable K L
inst✝⁶ : IsIntegralClosure B A L
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this✝ : Ideal.map (algebraMap A B) p ∣ a ^ e
this : ∀ x ∈ a, (intTrace A B) x ∈ p
⊢ (↑(P ^ (e - 1)))⁻¹⁻¹ = (↑a / ↑(Ideal.map (algebraMap A B) p))⁻¹

Tactic:
simp only [inv_inv, ha, FractionalIdeal.coeIdeal_mul, inv_div,
          mul_div_assoc]

Goal state after:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝²¹ : CommRing A
inst✝²⁰ : Field K
inst✝¹⁹ : CommRing B
inst✝¹⁸ : Field L
inst✝¹⁷ : Algebra A K
inst✝¹⁶ : Algebra B L
inst✝¹⁵ : Algebra A B
inst✝¹⁴ : Algebra K L
inst✝¹³ : Algebra A L
inst✝¹² : IsScalarTower A K L
inst✝¹¹ : IsScalarTower A B L
inst✝¹⁰ : IsDomain A
inst✝⁹ : IsFractionRing A K
inst✝⁸ : FiniteDimensional K L
inst✝⁷ : Algebra.IsSeparable K L
inst✝⁶ : IsIntegralClosure B A L
inst✝⁵ : IsFractionRing B L
inst✝⁴ : IsDedekindDomain A
inst✝³ : IsDedekindDomain B
inst✝² : IsTorsionFree A B
inst✝¹ : Module.Finite A B
p : Ideal A
inst✝ : p.IsMaximal
P : Ideal B
e : ℕ
he : e ≠ 0
hp : p ≠ ⊥
hP : P ^ e ∣ Ideal.map (algebraMap A B) p
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P ^ (e - 1) * a
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this✝ : Ideal.map (algebraMap A B) p ∣ a ^ e
this : ∀ x ∈ a, (intTrace A B) x ∈ p
⊢ ↑(P ^ (e - 1)) = ↑(P ^ (e - 1)) * (↑a / ↑a)
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
this : B.det v ≠ 0
⊢ ⊤ ≤ Submodule.span ℝ ↑(unitLattice K)

Tactic:
← isUnit_iff_ne_zero,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
this : IsUnit (B.det v)
⊢ ⊤ ≤ Submodule.span ℝ ↑(unitLattice K)
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (⊤ ⊓ (MonoidHom.toAdditive (QuotientGroup.mk' (torsion K))).toIntLinearMap.ker).FG

Tactic:
inf_of_le_right le_top,

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (MonoidHom.toAdditive (QuotientGroup.mk' (torsion K))).toIntLinearMap.ker.FG
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : Fin (rank K)
⊢ Additive.ofMul ↑(Quotient.out (Additive.toMul ((basisModTorsion K) i))) = (basisModTorsion K) i

Tactic:
← Equiv.eq_symm_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i : Fin (rank K)
⊢ ↑(Quotient.out (Additive.toMul ((basisModTorsion K) i))) = Additive.ofMul.symm ((basisModTorsion K) i)
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum

Goal state before:
pp: F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : Fintype F
inst✝³ : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst✝² : Field F'
inst✝¹ : Fintype F'
inst✝ : DecidableEq F'
hF' : ringChar F' ≠ 2
h : ringChar F' ≠ ringChar F
χ : MulChar F F' := (quadraticChar F).ringHomComp (algebraMap ℤ F')
⊢ χ ≠ 1

Tactic:
obtain ⟨a, ha⟩ := quadraticChar_exists_neg_one' hF

Goal state after:
F : Type u_1
inst✝⁵ : Field F
inst✝⁴ : Fintype F
inst✝³ : DecidableEq F
hF : ringChar F ≠ 2
F' : Type u_2
inst✝² : Field F'
inst✝¹ : Fintype F'
inst✝ : DecidableEq F'
hF' : ringChar F' ≠ 2
h : ringChar F' ≠ ringChar F
χ : MulChar F F' := (quadraticChar F).ringHomComp (algebraMap ℤ F')
a : Fˣ
ha : (quadraticChar F) ↑a = -1
⊢ χ ≠ 1
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsTorsionFree A B
inst✝⁴ : Module.Finite A B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝² : p.IsMaximal
inst✝¹ : Finite (A ⧸ p)
P Q : Ideal B
inst✝ : P.IsMaximal
hPQ : IsCoprime P Q
hP : P * Q = Ideal.map (algebraMap A B) p
⊢ ¬P ∣ differentIdeal A B

Tactic:
have : P.LiesOver p := by
    constructor
    refine ‹p.IsMaximal›.eq_of_le ?_ ?_
    · simpa using ‹P.IsMaximal›.ne_top
    · rw [← Ideal.map_le_iff_le_comap, ← hP]
      exact Ideal.mul_le_left
  exact not_dvd_differentIdeal_of_isCoprime_of_isSeparable A P Q hPQ hP

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity

Goal state before:
pp: case inl
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
hp : p ≠ 2
inst✝ : Fact (Nat.Prime p)
hq : p ≠ 2
⊢ legendreSym p ↑p = (-1) ^ (p / 2 * (p / 2)) * legendreSym p ↑p

pp: case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
h : p ≠ q
⊢ legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q

Tactic:
· rw [(eq_zero_iff p p).mpr (mod_cast natCast_self p), mul_zero]

Goal state after:
case inr
p q : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact (Nat.Prime q)
hp : p ≠ 2
hq : q ≠ 2
h : p ≠ q
⊢ legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q
Module: Mathlib.RingTheory.DedekindDomain.Different

Goal state before:
pp: A : Type u_1
B : Type u_3
inst✝¹¹ : CommRing A
inst✝¹⁰ : CommRing B
inst✝⁹ : Algebra A B
inst✝⁸ : IsDomain A
inst✝⁷ : IsDedekindDomain A
inst✝⁶ : IsDedekindDomain B
inst✝⁵ : IsTorsionFree A B
inst✝⁴ : Module.Finite A B
inst✝³ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
p : Ideal A
inst✝² : p.IsMaximal
hp : p ≠ ⊥
P : Ideal B
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
H : ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P)
a : Ideal B
ha : Ideal.map (algebraMap A B) p = P * a
hPa : ¬P ∣ a
K : Type u_1 := FractionRing A
L : Type u_3 := FractionRing B
hp' : ¬Ideal.map (algebraMap A B) p = ⊥
habot : a ≠ ⊥
hPbot : P ≠ ⊥
this : ∀ x ∈ a, (intTrace A B) x ∈ p
hP : (↑P)⁻¹ = ↑a / ↑(Ideal.map (algebraMap A B) p)
x : L
hx : ∀ a_1 ∈ Ideal.map (algebraMap A B) p, ∃ x' ∈ a, (algebraMap B L) x' = x * (algebraMap B L) a_1
y : A
hy : y ∈ p
hy' : (algebraMap A K) y ∈ ↑p
z : B
hz : z ∈ a
hz' : (algebraMap B L) z = x * (algebraMap B L) ((algebraMap A B) y)
⊢ (algebraMap A K) ((intTrace A B) z) ∈ ↑p

Tactic:
exact ⟨Algebra.intTrace A B z, this z hz, rfl⟩

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

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
this✝¹ : Nonempty { j // x j ≠ 0 }
this✝ : HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x ↑i)
v : ↑nonarchAbsVal
i : ι
hi : x i ≠ 0
this : Nonempty ι
j : ι
h : x j ≠ 0
⊢ ↑v (x j) ≤ ⨆ i, ↑v (x ↑i)

Tactic:
exact Finite.le_ciSup_of_le ⟨j, h⟩ le_rfl

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : ι → K
hx : x ≠ 0
⊢ HasFiniteMulSupport fun v ↦ ⨆ i, ↑v (x i)

Tactic:
by
  have : Nonempty {j // x j ≠ 0} := nonempty_subtype.mpr <| ne_iff.mp hx
  suffices (fun v : nonarchAbsVal ↦ ⨆ i : {j // x j ≠ 0}, v.val (x i)).HasFiniteMulSupport by
    convert! this with v
    obtain ⟨i, hi⟩ : ∃ j, x j ≠ 0 := Function.ne_iff.mp hx
    have : Nonempty ι := .intro i
    refine le_antisymm (ciSup_le fun j ↦ ?_) (ciSup_le fun ⟨j, hj⟩ ↦ Finite.le_ciSup_of_le j le_rfl)
    rcases eq_or_ne (x j) 0 with h | h
    · rw [h, v.val.map_zero]
      exact Real.iSup_nonneg' ⟨⟨i, hi⟩, v.val.nonneg ..⟩
    · exact Finite.le_ciSup_of_le ⟨j, h⟩ le_rfl
  fun_prop (disch := grind)

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case succ
N : ℕ
hN : termSum 1 N = log (↑N + 1) - ↑(harmonic (N + 1)) + 1
⊢ termSum 1 (N + 1) = log (↑(N + 1) + 1) - ↑(harmonic (N + 1 + 1)) + 1

Tactic:
unfold termSum at hN ⊢
    rw [Finset.sum_range_succ, hN, harmonic_succ (N + 1),
      term_one (by positivity : 0 < N + 1)]
    push_cast
    ring_nf

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
x y : K
⊢ logHeight₁ (x / y) = logHeight ![x, y]

Tactic:
rw [logHeight₁_eq_log_mulHeight₁, logHeight_eq_log_mulHeight, mulHeight₁_div_eq_mulHeight x y]

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: case hh
s : ℝ
hs : 1 < s
⊢ Tendsto (fun n ↦ (1 / ↑(n + 1)) ^ (s - 1)) atTop (𝓝 0)

Tactic:
rw [show 𝓝 (0 : ℝ) = 𝓝 (0 ^ (s - 1)) by rw [zero_rpow]; linarith]
        refine Tendsto.rpow_const ?_ (Or.inr <| by linarith)
        exact (tendsto_const_div_atTop_nhds_zero_nat _).comp (tendsto_add_atTop_nat _)

Goal state after:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case inr.inr
K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : (fun j ↦ (eval x) (p j)) ≠ 0
H₀ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ ⨆ j, (p j).coeff.sum fun x c ↦ v c
H₁ : 0 ≤ (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod
H₂ : 0 ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod
H₃ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i))
H₄ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
HH₁ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ (⨆ i, v (x i)) ^ N
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ j, f j
⊢ (mulHeight fun j ↦ (eval x) (p j)) ≤ max (mulHeightBound p) 1 * mulHeight x ^ N

Tactic:
simp only [mulHeight_eq hx, mulHeight_eq h₀, mulHeightBound_eq]

Goal state after:
case inr.inr
K : Type u_4
inst✝³ : Field K
ι : Type u_5
ι' : Type u_6
inst✝² : AdmissibleAbsValues K
inst✝¹ : Finite ι'
inst✝ : Finite ι
N : ℕ
p : ι' → MvPolynomial ι K
hp : ∀ (i : ι'), (p i).IsHomogeneous N
x : ι → K
hx : x ≠ 0
h₀ : (fun j ↦ (eval x) (p j)) ≠ 0
H₀ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ ⨆ j, (p j).coeff.sum fun x c ↦ v c
H₁ : 0 ≤ (Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod
H₂ : 0 ≤ (Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod
H₃ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i))
H₄ : 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)
HH₁ : ∀ (v : AbsoluteValue K ℝ), 0 ≤ (⨆ i, v (x i)) ^ N
HH₂ : ∀ (f : ι' → ℝ) (j : ι'), f j ≤ ⨆ j, f j
⊢ (Multiset.map (fun v ↦ ⨆ i, v ((eval x) (p i))) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v ((eval x) (p i)) ≤
    max
        ((Multiset.map (fun v ↦ ⨆ j, (p j).coeff.sum fun x c ↦ v c) archAbsVal).prod *
          ∏ᶠ (v : ↑nonarchAbsVal), ⨆ j, max (⨆ s, ↑v (coeff (↑s) (p j))) 1)
        1 *
      ((Multiset.map (fun v ↦ ⨆ i, v (x i)) archAbsVal).prod * ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (x i)) ^ N
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
z : ℂ
hz : 1 < z.re
⊢ 1 < ((starRingEnd ℂ) z).re

Tactic:
rwa [conj_re]

Goal state after:
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
| gaussSum (χ * φ) ψ * jacobiSum χ φ = ∑ x ∈ univ \ {0}, ∑ x_1, χ x_1 * φ (x - x_1) * ψ x + ∑ x, χ x * φ (0 - x) * ψ 0

Tactic:
enter [2, 2, 2, x]
    rw [zero_sub, neg_eq_neg_one_mul x, map_mul, mul_left_comm (χ x) (φ (-1)),
      ← MulChar.mul_apply, ψ.map_zero_eq_one, mul_one]

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
x : F
| φ (-1) * (χ * φ) x
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℝ
hs : s > 1
⊢ (↑(s - 1)⁻¹ * riemannZeta₁ ↑s).re = (s - 1)⁻¹ * (riemannZeta₁ ↑s).re

Tactic:
re_ofReal_mul

Goal state after:
s : ℝ
hs : s > 1
⊢ (s - 1)⁻¹ * (riemannZeta₁ ↑s).re = (s - 1)⁻¹ * (riemannZeta₁ ↑s).re
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: case neg
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
⊢ ∃ z ∈ ℤ[μ], jacobiSum χ ψ = -1 + z * (μ - 1) ^ 2

Tactic:
rw [jacobiSum_eq_aux, MulChar.sum_eq_zero_of_ne_one hχ₀, MulChar.sum_eq_zero_of_ne_one hψ₀, hq]
    have : NeZero n := ⟨by lia⟩
    have H := MulChar.exists_apply_sub_one_mul_apply_sub_one hχ hψ hμ
    have Hcs x := (H x).choose_spec
    refine ⟨-q * z₁ + ∑ x ∈ (univ \ {0, 1} : Finset F), (H x).choose, ?_, ?_⟩
    · refine Subalgebra.add_mem _ (Subalgebra.mul_mem _ (Subalgebra.neg_mem _ ?_) hz₁) ?_
      · exact Subalgebra.natCast_mem ..
      · exact Subalgebra.sum_mem _ fun x _ ↦ (Hcs x).1
    · 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
j : ZMod N
s : ℂ
hs : 1 < s.re
⊢ LFunction (fun k ↦ 𝕖 (j * k)) s = ∑' (b : ℕ), cexp (2 * ↑π * I * ↑(↑j.val / ↑N) * ↑b) / ↑b ^ s

Tactic:
LFunction_eq_LSeries _ hs,

Goal state after:
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
⊢ LSeries (fun x ↦ 𝕖 (j * ↑x)) s = ∑' (b : ℕ), cexp (2 * ↑π * I * ↑(↑j.val / ↑N) * ↑b) / ↑b ^ s
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hjs : j ≠ 0 ∨ s ≠ 1
U : Set ℂ := if j = 0 then {z | z ≠ 1} else Set.univ
V : Set ℂ := {z | 1 < z.re}
hUo : IsOpen U
f : ℂ → ℂ := LFunction fun k ↦ 𝕖 (j * k)
g : ℂ → ℂ := expZeta (toAddCircle j)
hU : ∀ {u : ℂ}, u ∈ U ↔ u ≠ 1 ∨ j ≠ 0
hf : AnalyticOnNhd ℂ f U
hg : AnalyticOnNhd ℂ g U
hUc : IsPreconnected U
hV : V ∈ 𝓝 2
⊢ 2 ∈ U

Tactic:
simp [U]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case hf
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)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
x : ℝ
⊢ HasDerivAt (fun x ↦ bernoulliFun (k + 1) (↑m * x)) (↑(k + 1) * bernoulliFun k (↑m * x) * ↑m) x

Tactic:
exact (hasDerivAt_bernoulliFun _ _).comp _ (hasDerivAt_const_mul ..)

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

Goal state before:
pp: case refine_2
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ↑((-1) ^ (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
        Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Tactic:
push_cast
      congr 1
      have : (Polynomial.bernoulli (2 * k + 1)).map (algebraMap ℚ ℂ) = _ :=
        (Polynomial.map_map (algebraMap ℚ ℝ) ofRealHom _).symm
      rw [this, ← ofRealHom_eq_coe, ← ofRealHom_eq_coe]
      apply Polynomial.map_aeval_eq_aeval_map (by simp)

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

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ sinZeta (↑x) (2 * ↑k + 1) =
    (-1) ^ (k + 1) / (2 * ↑k + 1) / (2 * ↑k + 1).Gammaℂ *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Tactic:
rw [sinZeta_two_mul_nat_add_one hk hx]
  congr 1
  have : (2 * k + 1)! = (2 * k + 1) * Complex.Gamma (2 * k + 1) := by
    rw [(by simp : Complex.Gamma (2 * k + 1) = Complex.Gamma (↑(2 * k) + 1)),
       Complex.Gamma_nat_eq_factorial, ← Nat.cast_ofNat (R := ℂ), ← Nat.cast_mul,
      ← Nat.cast_add_one, ← Nat.cast_mul, ← Nat.factorial_succ]
  simp_rw [this, Gammaℂ, cpow_neg, ← div_div, div_inv_eq_mul, div_mul_eq_mul_div, div_div]
  rw [(by simp : 2 * (k : ℂ) + 1 = ↑(2 * k + 1)), cpow_natCast]
  ring

Goal state after:
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
⊢ Complex.sin (↑π * (↑↑k + ↑(1 / 2))) * (-↑1) ^ (k + 1) = -↑1

Tactic:
← ofReal_add,

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
⊢ Complex.sin (↑π * ↑(↑k + 1 / 2)) * (-↑1) ^ (k + 1) = -↑1
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : hurwitzZetaOdd (↑x) (1 - 2 * ↑k) = 0
⊢ hurwitzZetaEven (↑x) (1 - 2 * ↑k) =
    -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))

Tactic:
hurwitzZetaEven_one_sub_two_mul_nat hk hx

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : hurwitzZetaOdd (↑x) (1 - 2 * ↑k) = 0
⊢ -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k))) =
    -1 / (2 * ↑k) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k)))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case inr
k : ℕ
hk : k ≠ 0
⊢ riemannZeta (-↑k) = -↑(bernoulli' (k + 1)) / (↑k + 1)

Tactic:
· rw [← hurwitzZeta_zero, ← QuotientAddGroup.mk_zero, hurwitzZeta_neg_nat hk
      (left_mem_Icc.mpr zero_le_one), ofReal_zero, Polynomial.eval_zero_map,
      Polynomial.bernoulli_eval_zero, Algebra.algebraMap_eq_smul_one, Rat.smul_one_eq_cast,
      div_mul_eq_mul_div, neg_one_mul, bernoulli_eq_bernoulli'_of_ne_one (by simp [hk])]

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

Goal state before:
pp: f g : ℕ → ℂ
s a b : ℂ
hf : LSeriesHasSum f s a
hg : LSeriesHasSum g s b
⊢ LSeriesHasSum (f + g) s (a + b)

Tactic:
simpa [LSeriesHasSum, term_add] using! HasSum.add hf hg

Goal state after:
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
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * completedLFunction (𝓕 Φ) s

Tactic:
have hUo : IsOpen U := (isOpen_compl_singleton.union isOpen_const).inter
    (isOpen_compl_singleton.union isOpen_const)

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
⊢ completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * completedLFunction (𝓕 Φ) 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) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x) / 2 = ↑(Real.cos (2 * π * ↑n * x))

Tactic:
ofReal_cos,

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) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x) / 2 = cos ↑(2 * π * ↑n * x)
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
⊢ ‖L (fun n ↦ 1 ↑n) (1 + ↑x) ^ 3 * L (fun n ↦ χ ↑n) (1 + ↑x + I * ↑y) ^ 4 *
        L (fun n ↦ (χ ^ 2) ↑n) (1 + ↑x + 2 * I * ↑y)‖ ≥
    1

Tactic:
by
  have ⟨h₀, h₁, h₂⟩ := one_lt_re_one_add hx y
  have H₀ := summable_neg_log_one_sub_mul_prime_cpow (N := N) 1 h₀
  have H₁ := summable_neg_log_one_sub_mul_prime_cpow χ h₁
  have H₂ := summable_neg_log_one_sub_mul_prime_cpow (χ ^ 2) h₂
  have hsum₀ := (hasSum_re H₀.hasSum).summable.mul_left 3
  have hsum₁ := (hasSum_re H₁.hasSum).summable.mul_left 4
  have hsum₂ := (hasSum_re H₂.hasSum).summable
  rw [← LSeries_eulerProduct_exp_log _ h₀, ← LSeries_eulerProduct_exp_log χ h₁,
    ← LSeries_eulerProduct_exp_log _ h₂]
  simp only [← exp_nat_mul, Nat.cast_ofNat, ← exp_add, norm_exp, add_re, mul_re,
    re_ofNat, im_ofNat, zero_mul, sub_zero, Real.one_le_exp_iff]
  rw [re_tsum H₀, re_tsum H₁, re_tsum H₂, ← tsum_mul_left, ← tsum_mul_left,
    ← hsum₀.tsum_add hsum₁, ← (hsum₀.add hsum₁).tsum_add hsum₂]
  simpa only [neg_add_rev, neg_re, mul_neg, χ.pow_apply' two_ne_zero, ge_iff_le, add_re, one_re,
    ofReal_re, ofReal_add, ofReal_one] using
      tsum_nonneg fun (p : Nat.Primes) ↦ χ.re_log_comb_nonneg p.prop.two_le h₀ y

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
x : ℝ
hx : 0 < x
y : ℝ
⊢ ‖LFunctionTrivChar N (1 + ↑x) ^ 3 * LFunction χ (1 + ↑x + I * ↑y) ^ 4 * LFunction (χ ^ 2) (1 + ↑x + 2 * I * ↑y)‖ ≥ 1

Tactic:
have ⟨h₀, h₁, h₂⟩ := one_lt_re_one_add hx y
  rw [LFunctionTrivChar, DirichletCharacter.LFunction_eq_LSeries 1 h₀,
    χ.LFunction_eq_LSeries h₁, (χ ^ 2).LFunction_eq_LSeries h₂]
  exact norm_LSeries_product_ge_one χ hx y

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

Goal state before:
pp: case refine_1
q : ℕ
a : ZMod q
inst✝ : NeZero q
⊢ ContinuousOn (fun s ↦ -deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s)
    {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Tactic:
refine (continuousOn_neg_logDeriv_LFunctionTrivChar₁ q).mono fun s hs ↦ ?_

Goal state after:
case refine_1
q : ℕ
a : ZMod q
inst✝ : NeZero q
s : ℂ
hs : s ∈ {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}
⊢ s ∈ {s | s = 1 ∨ LFunctionTrivChar q s ≠ 0}