mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: K : Type u_4
inst✝¹ : Field K
inst✝ : AdmissibleAbsValues K
C' : ℝ
hC₀ : C' > 0
hC : ∀ (a b c d : K), mulHeight ![a * c, a * d + b * c, b * d] ≤ C' * mulHeight ![a, b] * mulHeight ![c, d]
a b c d : K
⊢ log (mulHeight ![a * c, a * d + b * c, b * d]) ≤ log (C' * mulHeight ![a, b] * mulHeight ![c, d])

Tactic:
exact log_le_log (by positivity) (hC ..)

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

Goal state before:
pp: M N : ℕ
inst✝¹ : NeZero M
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
h : χ ≠ 1
hχ : (changeLevel hMN) χ ≠ 1
p : ℕ
hp : p ∈ N.primeFactors
⊢ Continuous fun s ↦ 1 - χ ↑p * ↑p ^ (-s)

Tactic:
have : NeZero p := ⟨(Nat.prime_of_mem_primeFactors hp).ne_zero⟩
        fun_prop

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

Goal state before:
pp: case neg
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : j = 0 ∧ s = 1
⊢ 0 * LFunction (fun k ↦ 𝕖 (-0 * k)) s = 0 * expZeta (toAddCircle (-0)) s

Tactic:
zero_mul,

Goal state after:
case neg
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
s : ℂ
hs : Φ 0 = 0 ∨ s ≠ 1
j : ZMod N
h : j = 0 ∧ s = 1
⊢ 0 = 0 * expZeta (toAddCircle (-0)) s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ 1 < 2 * k

Tactic:
lia

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

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ∑' (b : ℕ), ↑(Real.sin (2 * π * x * ↑b)) / ↑b ^ (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:
refine Eq.trans ?_ <|
      (congr_arg ofReal (hasSum_one_div_nat_pow_mul_sin hk hx).tsum_eq).trans ?_

Goal state after:
case refine_1
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ∑' (b : ℕ), ↑(Real.sin (2 * π * x * ↑b)) / ↑b ^ (2 * ↑k + 1) =
    ↑(∑' (b : ℕ), 1 / ↑b ^ (2 * k + 1) * Real.sin (2 * π * ↑b * x))

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)))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ 1 < 2 * k + 1

Tactic:
lia

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

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ 2 * k = 2 * k - 1 + 1

Tactic:
lia

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

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ 1 ≤ 2 * k

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: 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
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ k + 1 ≠ 0

Tactic:
lia

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

Goal state before:
pp: x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
hk : 2 * n ≠ 0
⊢ n ≠ 0

Tactic:
lia

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

Goal state before:
pp: x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
hk : 2 * n + 1 ≠ 0
⊢ n + 1 ≠ 0

Tactic:
lia

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

Goal state before:
pp: k : ℕ
hk : k ≠ 0
⊢ 1 < 2 * k

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
hx : 1 ∈ Icc 0 1
this :
  ∀ {y : ℝ}, y ∈ Ico 0 1 → HasSum (fun n ↦ 1 / ↑n ^ k * (fourier n) ↑y) (-(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k y))
⊢ k ≠ 1

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
⊢ k ≠ 1

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
⊢ k ≠ 0

Tactic:
lia

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
this : riemannZeta (-2) = 0
⊢ -2 ≠ 1

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_6
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) = -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) + 0 * (fourier 0) ↑x

Tactic:
zero_mul,

Goal state after:
case e'_6
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
⊢ -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) = -(2 * ↑π * I) ^ k / ↑k ! * ↑(bernoulliFun k x) + 0
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ 2 ≤ 2 * k

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

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

pp: case e'_6
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) = -(2 * ↑π * I) ^ (2 * k)

Tactic:
· rw [pow_mul (-1 : ℂ), neg_one_sq, one_pow, one_mul]

Goal state after:
case e'_6
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) = -(2 * ↑π * I) ^ (2 * k)
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn✝ : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
hn : ↑n ^ (-x) < 1
⊢ 0 < n

Tactic:
lia

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn✝ : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
hn : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ ¬n = 0

Tactic:
lia

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

Goal state before:
pp: p : Nat.Primes
k : ℕ
⊢ ↑↑p ^ (1 / 2) / (1 / 2) * (↑↑p)⁻¹ ^ (k + 2) = 2 * (↑↑p)⁻¹ ^ (-1 / 2) * (↑↑p)⁻¹ ^ (k + 2)

Tactic:
by
      simp only [← div_mul, div_one, mul_comm, neg_div, Real.inv_rpow p.val.cast_nonneg,
        ← Real.rpow_neg p.val.cast_nonneg, neg_neg]

Goal state after:
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) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x) / 2 =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / ↑(2 * k)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))

Tactic:
bernoulliFun

Goal state after:
case e'_3
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
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! *
        ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))) /
      2 =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / 2 / ↑(2 * k)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ 2 ≤ 2 * k + 1

Tactic:
lia

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

Goal state before:
pp: case refine_1
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
hFF' : F₀ ∘ Subtype.val = F' ∘ ⇑prodNatEquiv.symm
hF'₀ : ∀ (p : Nat.Primes), F' (p, 0) = 0
⊢ Summable F'

Tactic:
have hF'₁ : F'' = F' ∘ (Prod.map _root_.id (· + 1)) := by
    ext1
    simp only [Function.comp_apply, Prod.map_fst, id_eq, Prod.map_snd, F'', F']

Goal state after:
case refine_1
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
hFF' : F₀ ∘ Subtype.val = F' ∘ ⇑prodNatEquiv.symm
hF'₀ : ∀ (p : Nat.Primes), F' (p, 0) = 0
hF'₁ : F'' = F' ∘ Prod.map id fun x ↦ x + 1
⊢ Summable F'
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
⊢ 4 ≠ 0

Tactic:
lia

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

Goal state before:
pp: case inl
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
⊢ (1 / ↑0) ^ 3 * ↑0 ^ 4 * 1 = ↑0

pp: case inr
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h✝ : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
x : ℝ
h : x ≠ 0
⊢ (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x

Tactic:
· rw [ofReal_zero, zero_pow (by lia), mul_zero, mul_one]

Goal state after:
case inr
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h✝ : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
x : ℝ
h : x ≠ 0
⊢ (1 / ↑x) ^ 3 * ↑x ^ 4 * 1 = ↑x
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
⊢ ∀ (x : ℝ), (fun x ↦ LSeries f ↑x) x = 0 x

Tactic:
simp [LSeries_eq_zero_of_abscissaOfAbsConv_eq_top h]

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

Goal state before:
pp: f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : (fun x ↦ LSeries f ↑x) =ᶠ[atTop] fun x ↦ LSeries g ↑x
⊢ (fun x ↦ LSeries (f - g) ↑x) =ᶠ[atTop] 0

Tactic:
rw [EventuallyEq, eventually_atTop] at h ⊢

Goal state after:
f g : ℕ → ℂ
hf : abscissaOfAbsConv f < ⊤
hg : abscissaOfAbsConv g < ⊤
h : ∃ a, ∀ (b : ℝ), a ≤ b → LSeries f ↑b = LSeries g ↑b
⊢ ∃ a, ∀ (b : ℝ), a ≤ b → LSeries (f - g) ↑b = 0 b
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
this : ∀ (α β γ δ : ℂ), α * I * β / γ * δ * I = I ^ 2 * α * β / γ * δ
⊢ -(-1 * (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x) / 2) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))

Tactic:
bernoulliFun

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
this : ∀ (α β γ δ : ℂ), α * I * β / γ * δ * I = I ^ 2 * α * β / γ * δ
⊢ -(-1 * (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! *
          ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) /
        2) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
⊢ 1 ≤ 2 * k

Tactic:
lia

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

Goal state before:
pp: a : ℤ
b₁ b₂ : ℕ
hb₁ : b₁ ≠ 0
hb₂ : b₂ ≠ 0
⊢ J(a | b₁ * b₂) = J(a | b₁) * J(a | b₂)

Tactic:
by
  rw [jacobiSym, ((perm_primeFactorsList_mul hb₁ hb₂).pmap _).prod_eq, List.pmap_append,
    List.prod_append]
  pick_goal 2
  · exact fun p hp =>
      (List.mem_append.mp hp).elim prime_of_mem_primeFactorsList prime_of_mem_primeFactorsList
  · rfl

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

Goal state before:
pp: case cons
a : ℤ
n : ℕ
l' : List ℕ
ih : (∀ n ∈ l', n ≠ 0) → J(a | l'.prod) = (List.map (fun n ↦ J(a | n)) l').prod
hl : ∀ n_1 ∈ n :: l', n_1 ≠ 0
⊢ J(a | (n :: l').prod) = (List.map (fun n ↦ J(a | n)) (n :: l')).prod

Tactic:
have hn := hl n List.mem_cons_self
    -- `n ≠ 0`
    have hl' := List.prod_ne_zero fun hf => hl 0 (List.mem_cons_of_mem _ hf) rfl
    -- `l'.prod ≠ 0`
    have h := fun m hm => hl m (List.mem_cons_of_mem _ hm)
    -- `∀ (m : ℕ), m ∈ l' → m ≠ 0`
    rw [List.map, List.prod_cons, List.prod_cons, mul_right' a hn hl', ih h]

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

Goal state before:
pp: a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun a ↦ { toFun := fun x ↦ qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a) b = qrSign b a * J(↑b | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
⊢ (rhs a) ↑p = legendreSym p ↑a

Tactic:
have hpo := pp.eq_two_or_odd'.resolve_left hp

Goal state after:
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun a ↦ { toFun := fun x ↦ qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a) b = qrSign b a * J(↑b | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
⊢ (rhs a) ↑p = legendreSym p ↑a
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case refine_2
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
t : ℝ
ht : t ∈ Set.Ioc 1 T
⊢ ‖S t - l * ↑t‖ * t ^ (-s - 1) ≤ ‖S t - l * ↑t‖ * t ^ (-1 - 1)

Tactic:
gcongr
      exact ht.1.le

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

Goal state before:
pp: case inl
a b : ℕ
ha2 : a % 2 = 1
hb2 : b % 2 = 1
ha1 : a % 4 = 1
⊢ (if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)) = J(↑a | b)

Tactic:
simpa [ha1] using jacobiSym.quadratic_reciprocity_one_mod_four' (Nat.odd_iff.mpr hb2) ha1

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

Goal state before:
pp: case inr.e_a.succ
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
a' : ℕ
ha₁' : ¬2 ∣ a'
ha₁ : Odd a'
e : ℕ
ha₂ : a = 2 ^ (e + 1) * a'
⊢ 8 ∣ 4 * a

Tactic:
use 2 ^ e * a'

Goal state after:
case h
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
a' : ℕ
ha₁' : ¬2 ∣ a'
ha₁ : Odd a'
e : ℕ
ha₂ : a = 2 ^ (e + 1) * a'
⊢ 4 * a = 8 * (2 ^ e * a')
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
⊢ (s - 1) * s * ∫ (t : ℝ) in Set.Ioi 1, ‖(S t - l * ↑t) * ↑t ^ (-↑s - 1)‖ =
    (s - 1) * s * ∫ (t : ℝ) in Set.Ioi 1, ‖S t - l * ↑t‖ * t ^ (-s - 1)

Tactic:
by
      congr 1
      refine setIntegral_congr_fun measurableSet_Ioi fun t ht ↦ ?_
      replace ht : 0 ≤ t := zero_le_one.trans ht.le
      rw [norm_mul, show (-(s : ℂ) - 1) = (-s - 1 : ℝ) by simp, ← ofReal_cpow ht, norm_real,
        Real.norm_of_nonneg (Real.rpow_nonneg ht _)]

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: n : ℕ
this : 1 ≤ 2 ^ n
⊢ 2 ^ (n + 1) - 1 = 2 * (2 ^ n - 1) + 1

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
n n✝ : ℕ
hmn✝ : 2 ≤ n✝
a✝ : mersenne n✝ % 4 = 3
⊢ (2 * mersenne n✝ + 1) % 4 = 3

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: k : ℕ
h : 3 ≤ 2 * k + 1
⊢ 1 ≤ k

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: k j : ℕ
hmn✝ : 1 ≤ j
a✝ : mersenne (2 * j + 1) % 3 = 1
⊢ 2 * (j + 1) = 2 * j + 1 + 1

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
k j : ℕ
hmn✝ : 1 ≤ j
a✝ : mersenne (2 * j + 1) % 3 = 1
⊢ (2 * (2 * mersenne (2 * j + 1) + 1) + 1) % 3 = 1

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
n n✝ : ℕ
hmn✝ : 3 ≤ n✝
a✝ : mersenne n✝ % 8 = 7
⊢ (2 * mersenne n✝ + 1) % 8 = 7

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
this : mersenne p % 8 = 7
⊢ mersenne p ≠ 2

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
this : mersenne p % 8 = 7
⊢ (if mersenne p % 2 = 0 then 0 else if mersenne p % 8 = 1 ∨ mersenne p % 8 = 7 then 1 else -1) = 1

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
odd : Odd p
⊢ 2 ≤ p

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x : X q
⊢ 1 * x = x

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x : X q
⊢ x * 1 = x

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
⊢ ↑0 = 0

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q x✝ : ℕ
⊢ ↑(x✝ + 1) = ↑x✝ + 1

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q n : ℕ
⊢ (↑↑n, 0) = ↑n

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q n : ℕ
⊢ (↑(Int.negSucc n), 0) = -↑(n + 1)

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x✝ : X q
⊢ 0 * x✝ = 0

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
x✝ : X q
⊢ x✝ * 0 = 0

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
n m : ℤ
⊢ ↑(n * m) = ↑n * ↑m

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q n : ℕ
⊢ ↑↑n = ↑n

Tactic:
ext <;> simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
⊢ (2, 1) * (2, -1) = 1

Tactic:
ext <;> simp

Goal state after:
case h₁
q : ℕ
⊢ 2 * 2 + -3 = 1
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz : z ∈ p.aroots ℂ
⊢ (Multiset.map (fun a ↦ max 1 ‖a‖) (map (castRingHom ℂ) p).roots).prod ≤ 1

Tactic:
grind [prod_max_one_norm_roots_le_mahlerMeasure_of_one_le_leadingCoeff,
        norm_leadingCoeff_eq_one_of_mahlerMeasure_eq_one]

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
w✝ : ℕ
h✝ : q = 2 * w✝ + 1
⊢ (q + 1) / 2 = q / 2 + 1

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
pow2 : 2 ^ ((q + 1) / 2) = 2
⊢ ω ^ ((q + 1) / 2) = -1

Tactic:
have := two_mul_ω_pow odd leg3

Goal state after:
q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
pow2 : 2 ^ ((q + 1) / 2) = 2
this : (2 * ω) ^ ((q + 1) / 2) = -2
⊢ ω ^ ((q + 1) / 2) = -1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
this : ω ^ ((q + 1) / 2) * ωb ^ ((q + 1) / 4) = -ωb ^ ((q + 1) / 4)
k : ℕ
hk : q + 1 = 4 * k
⊢ (q + 1) / 2 = (q + 1) / 4 + (q + 1) / 4

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
hq4 : 4 ∣ q + 1
this : ω ^ ((q + 1) / 2) * ωb ^ ((q + 1) / 4) = -ωb ^ ((q + 1) / 4)
div4 : (q + 1) / 2 = (q + 1) / 4 + (q + 1) / 4
⊢ ω ^ ((q + 1) / 4) + ωb ^ ((q + 1) / 4) = 0

Tactic:
rw [div4, pow_add, mul_assoc, ← mul_pow, ω_mul_ωb, one_pow, mul_one] at this

Goal state after:
q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
hq4 : 4 ∣ q + 1
this : ω ^ ((q + 1) / 4) = -ωb ^ ((q + 1) / 4)
div4 : (q + 1) / 2 = (q + 1) / 4 + (q + 1) / 4
⊢ ω ^ ((q + 1) / 4) + ωb ^ ((q + 1) / 4) = 0
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
w : 1 < p
p' : ℕ
hp' : p' = p - 2
⊢ p = p' + 2

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
w : 1 < p' + 2
hp' : p' = p' + 2 - 2
⊢ LucasLehmerTest (p' + 2) → Nat.Prime (mersenne (p' + 2))

Tactic:
have w : 1 < p' + 2 := Nat.lt_of_sub_eq_succ rfl

Goal state after:
p' : ℕ
w✝ : 1 < p' + 2
hp' : p' = p' + 2 - 2
w : 1 < p' + 2
⊢ LucasLehmerTest (p' + 2) → Nat.Prime (mersenne (p' + 2))
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
w : 3 ≤ p
hp : Nat.Prime (mersenne p)
this : Fact (Nat.Prime (mersenne p))
p' : ℕ
hp' : p' = p - 2
⊢ p = p' + 2

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
⊢ ↑(s (p' + 2 - 2)) = 0

Tactic:
← X.fst_intCast,

Goal state after:
p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
⊢ (↑(s (p' + 2 - 2))).1 = 0
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
⊢ p' + 2 ≠ 2

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
hp : 2 ≤ p
n✝ : ℕ
a✝ : ↑(sModNat (2 ^ p - 1) n✝) = sMod p n✝
⊢ 2 > 0

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
hp : 1 < p
h : sModNatTR (2 ^ p - 1) (p - 2) = 0
⊢ sMod p (p - 2) = 0

Tactic:
← sModNat_eq_sMod p _ hp,

Goal state after:
p : ℕ
hp : 1 < p
h : sModNatTR (2 ^ p - 1) (p - 2) = 0
⊢ ↑(sModNat (2 ^ p - 1) (p - 2)) = 0
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
hp : 1 < p
h : sModNatTR (2 ^ p - 1) (p - 2) ≠ 0
⊢ ¬sMod p (p - 2) = 0

Tactic:
← sModNat_eq_sMod p _ hp,

Goal state after:
p : ℕ
hp : 1 < p
h : sModNatTR (2 ^ p - 1) (p - 2) ≠ 0
⊢ ¬↑(sModNat (2 ^ p - 1) (p - 2)) = 0