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
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ

Tactic:
rw [gaussSum_mul _ _ ψ, sum_eq_sum_sdiff_singleton_add (mem_univ (0 : F))]

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
⊢ gaussSum (χ * φ) ψ * jacobiSum χ φ = ∑ x ∈ univ \ {0}, ∑ x_1, χ x_1 * φ (x - x_1) * ψ x + ∑ x, χ x * φ (0 - x) * ψ 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 : ℕ), f.natDegree ≤ m → { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) }.coeff m = 0

Tactic:
intro m hm

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
⊢ { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) }.coeff m = 0
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)
⊢ Φ j * LFunction (fun k ↦ 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s

Tactic:
simp only [neg_ne_zero, not_or, not_not] at h

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
⊢ Φ j * LFunction (fun k ↦ 𝕖 (-j * k)) s = Φ j * expZeta (toAddCircle (-j)) s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

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

Tactic:
suffices hurwitzZetaOdd x (1 - 2 * k) = 0 by
    rw [hurwitzZeta, this, add_zero, hurwitzZetaEven_one_sub_two_mul_nat hk hx]
  obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hk
  rw [Nat.cast_succ, show (1 : ℂ) - 2 * (k + 1) = -2 * k - 1 by ring,
    hurwitzZetaOdd_neg_two_mul_nat_sub_one]

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

Goal state before:
pp: case inl
⊢ riemannZeta (2 * ↑0) = (-1) ^ (0 + 1) * 2 ^ (2 * ↑0 - 1) * ↑π ^ (2 * 0) * ↑(bernoulli (2 * 0)) / ↑(2 * 0)!

Tactic:
simp [riemannZeta_zero]

Goal state after:
case inl
⊢ -1 / 2 = -2⁻¹
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: ⊢ riemannZeta 4 = ↑π ^ 4 / 90

Tactic:
by
  convert! congr_arg ((↑) : ℝ → ℂ) hasSum_zeta_four.tsum_eq
  · rw [← Nat.cast_one, show (4 : ℂ) = (4 : ℕ) by simp,
      zeta_nat_eq_tsum_of_gt_one (by simp : 1 < 4)]
    simp only [push_cast]
  · norm_cast

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
⊢ (∑ x, Φ (-x) * expZeta (toAddCircle (-x)) s) / (2 * I) - (∑ x, Φ x * expZeta (toAddCircle (-x)) s) / (2 * I) =
    -I⁻¹ * LFunction (𝓕 Φ) s

Tactic:
simp only [hΦ _, neg_mul, sum_neg_distrib, LFunction_dft Φ (.inl hΦ.map_zero)]
    ring

Goal state after:
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
n : ℕ
⊢ term (fun n ↦ ↑(residueClass a n)) (↑y) n = {n | ↑n = a}.indicator (term (fun n ↦ ↑(Λ n)) ↑y) n

Tactic:
by_cases hn : (n : ZMod q) = a

Goal state after:
case pos
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun n ↦ ↑(Λ n)) ↑y
n : ℕ
hn : ↑n = a
⊢ term (fun n ↦ ↑(residueClass a n)) (↑y) n = {n | ↑n = a}.indicator (term (fun n ↦ ↑(Λ n)) ↑y) n

case neg
q : ℕ
a : ZMod q
y : ℝ
hy : 1 < y
this : LSeriesSummable (fun n ↦ ↑(Λ n)) ↑y
n : ℕ
hn : ¬↑n = a
⊢ 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
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ LFunctionResidueClassAux a s = (fun s ↦ L (fun n ↦ ↑(residueClass a n)) s - (↑q.totient)⁻¹ / (s - 1)) s

Tactic:
simp only [LSeries_residueClass_eq ha hs, LFunctionResidueClassAux]

Goal state after:
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
s : ℂ
hs : 1 < s.re
⊢ (↑q.totient)⁻¹ *
      (-deriv (LFunctionTrivChar₁ q) s / LFunctionTrivChar₁ q s -
        ∑ χ ∈ {1}ᶜ, χ a⁻¹ * deriv (LFunction χ) s / LFunction χ s) =
    -(↑q.totient)⁻¹ * ∑ χ, χ a⁻¹ * (deriv (LFunction χ) s / LFunction χ s) - (↑q.totient)⁻¹ / (s - 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
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
hc : ∀ (k : ℕ), Tendsto (fun x ↦ F x k) atTop (nhds 0)
⊢ Tendsto (fun x ↦ ∑' (m : ℕ), F x m) atTop (nhds 0)

Tactic:
rw [show (0 : ℂ) = tsum (fun _ : ℕ ↦ 0) from tsum_zero.symm]

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
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
hc : ∀ (k : ℕ), Tendsto (fun x ↦ F x k) atTop (nhds 0)
⊢ Tendsto (fun x ↦ ∑' (m : ℕ), F x m) atTop (nhds (∑' (x : ℕ), 0))
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: ⊢ 2 ≠ 1

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: ⊢ 4 ≠ 1

Tactic:
decide

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: this : 1 / 4 = (algebraMap ℚ ℝ) (1 / 4)
⊢ 2 * 1 + 1 = 3

Tactic:
decide

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
x✝ : ℕ
hx : x✝ ∈ Ico 1 (p / 2).succ
⊢ 1 < 2

Tactic:
decide

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
⊢ Multiset.map (fun x ↦ (a * ↑x).valMinAbs.natAbs) (Ico 1 (p / 2).succ).val =
    Multiset.map (fun a ↦ a) (Ico 1 (p / 2).succ).val

Tactic:
have hmem : ∀ (x : ℕ) (_ : x ∈ Ico 1 (p / 2).succ),
      (a * x : ZMod p).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ := by
    intro x hx
    simp [hap, CharP.cast_eq_zero_iff (ZMod p) p, hpe hx, one_le_iff_ne_zero, natAbs_valMinAbs_le _]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
hmem : ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
⊢ Multiset.map (fun x ↦ (a * ↑x).valMinAbs.natAbs) (Ico 1 (p / 2).succ).val =
    Multiset.map (fun a ↦ a) (Ico 1 (p / 2).succ).val
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ 1 < 2

Tactic:
decide

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

Goal state before:
pp: f : ℕ → ℝ
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
hf : ∀ (n : ℕ), 0 ≤ f n
x✝ : ℕ
⊢ ∑ k ∈ Icc 1 x✝, f k = ∑ k ∈ Icc 1 x✝, ‖↑(f k)‖

Tactic:
by simp [abs_of_nonneg (hf _)]

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

Goal state before:
pp: p q : ℕ
hp : Fact (Nat.Prime p)
hq0 : ↑q ≠ 0
hswap :
  #({x ∈ Ico 1 (q / 2).succ ×ˢ Ico 1 (p / 2).succ | x.2 * q ≤ x.1 * p}) =
    #({x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.1 * q ≤ x.2 * p})
x : ℕ × ℕ
hx : x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ
hpq : x.2 * p ≤ x.1 * q
hqp : x.1 * q ≤ x.2 * p
⊢ 1 < 2

Tactic:
decide

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

Goal state before:
pp: a : ℤ
b : ℕ
h : a.gcd ↑b = 1
⊢ J(a | b) ^ 2 = 1

Tactic:
rcases eq_one_or_neg_one h with h₁ | h₁ <;> rw [h₁]

Goal state after:
case inl
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h₁ : J(a | b) = 1
⊢ 1 ^ 2 = 1

case inr
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h₁ : J(a | b) = -1
⊢ (-1) ^ 2 = 1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : J(a | p) = 1
⊢ ¬1 = -1

Tactic:
decide

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

Goal state before:
pp: b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
this : (↑2).gcd ↑b = 1
⊢ 4 ≠ 0

Tactic:
decide

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

Goal state before:
pp: b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
this : (↑2).gcd ↑b = 1
⊢ 4 = ↑2 ^ 2

Tactic:
decide

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

Goal state before:
pp: b : ℕ
hb : Odd b
⊢ 4 % 4 = 0

Tactic:
decide

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

Goal state before:
pp: b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha2 : 2 * a % 2 = 0
⊢ 2 ≠ 0

Tactic:
decide

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

Goal state before:
pp: case e'_2.e'_6
a✝ b : ℕ
ha : Odd a✝
hb : Odd b
a : ℕ
⊢ 1 = J(↑1 | a)

Tactic:
symm

Goal state after:
case e'_2.e'_6
a✝ b : ℕ
ha : Odd a✝
hb : Odd b
a : ℕ
⊢ J(↑1 | a) = 1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
⊢ Even 4

Tactic:
decide

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

Goal state before:
pp: 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 * (2 ^ (e + 1) * a') = 8 * (2 ^ e * a')

Tactic:
Nat.pow_succ

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 * (2 ^ e * 2 * a') = 8 * (2 ^ e * a')
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
hb : Odd b
ha : a = -↑a.natAbs
⊢ Even 4

Tactic:
decide

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

Goal state before:
pp: a b : ℕ
flip : Bool
ha0 : a > 0
ha4 : a % 4 = 0
⊢ 0 < 4

Tactic:
decide

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

Goal state before:
pp: a b : ℕ
flip : Bool
ha0 : a > 0
ha4 : ¬a % 4 = 0
ha2 : a % 2 = 0
⊢ 0 < 2

Tactic:
decide

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

Goal state before:
pp: a b : ℕ
flip : Bool
ha0 : a > 0
ha4 : a % 4 = 0
⊢ 1 < 4

Tactic:
decide

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

Goal state before:
pp: a b : ℕ
flip : Bool
ha0 : a > 0
ha4 : ¬a % 4 = 0
ha2 : a % 2 = 0
⊢ 1 < 2

Tactic:
decide

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

Goal state before:
pp: a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : a % 4 = 0
⊢ 1 < 4

Tactic:
decide

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

Goal state before:
pp: a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : a % 2 = 0
⊢ 1 < 2

Tactic:
decide

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

Goal state before:
pp: a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
hba : b % a = 0
h : b = 0
⊢ ¬0 > 1

Tactic:
decide

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

Goal state before:
pp: a : ℤ
ha2 : ¬a % 2 = 0
b : ℕ
IH : ∀ m < 2 * b, J(a | m) = fastJacobiSym a m
hb0 : ¬2 * b = 0
hb2 : 2 * b % 2 = 0
⊢ 2 ≠ 0

Tactic:
decide

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

Goal state before:
pp: a : ℤ
ha2 : ¬a % 2 = 0
b : ℕ
IH : ∀ m < 2 * b, J(a | m) = fastJacobiSym a m
hb0 : ¬2 * b = 0
hb2 : 2 * b % 2 = 0
⊢ 0 < 2

Tactic:
decide

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

Goal state before:
pp: case pos
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : a % ↑b = 0
⊢ J(a | b) = 0

pp: case neg
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ J(a | b) = fastJacobiSymAux (a % ↑b).natAbs b false ⋯

Tactic:
· rw [mod_left, hab, zero_left (lt_of_le_of_ne (Nat.pos_of_ne_zero hb0) (Ne.symm hb1))]

Goal state after:
case neg
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ J(a | b) = fastJacobiSymAux (a % ↑b).natAbs b false ⋯
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₁ : ∀ {C ε : ℝ}, Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[>] 1) fun s ↦ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖
⊢ limsup (fun x ↦ ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖) (𝓝[>] 1) ≤ 0

Tactic:
refine le_of_forall_pos_le_add fun ε hε ↦ ?_
    rw [zero_add]
    obtain ⟨C, hC₁, hC₂⟩ := LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₃ hlim hfS hε
    refine le_of_le_of_eq (limsup_le_limsup hC₂ ?_ h₁.isBoundedUnder_le) h₁.limsup_eq
    exact isCoboundedUnder_le_of_eventually_le _ (univ_mem' fun _ ↦ norm_nonneg _)

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz : z ∈ p.aroots ℂ
⊢ ‖z‖ ≤ 1

Tactic:
by
  calc
  ‖z‖ ≤ max 1 ‖z‖ := le_max_right 1 ‖z‖
  _   ≤ ((p.map (castRingHom ℂ)).roots.map (fun a ↦ max 1 ‖a‖)).prod :=
        mem_le_prod_of_one_le (fun a ↦ le_max_left 1 ‖a‖) hz
  _   ≤ 1 := by 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: case refine_1
p' : ℕ
⊢ 1 < p' + 2

Tactic:
exact le_add_left _ _

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
k : ℤ
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
h : ω ^ 2 ^ (p' + 1) = ↑k * ↑(2 ^ (p' + 2) - 1) * ω ^ 2 ^ p' - 1
⊢ 0 < 2

Tactic:
decide

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
⊢ 4 ∣ mersenne (p' + 2) + 1

Tactic:
simp [pow_add]

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
this : X.ω ^ (2 ^ p' * 2 ^ 2 / 4) + X.ωb ^ (2 ^ p' * 2 ^ 2 / 4) = 0
⊢ (X.ω ^ 2 ^ p' + X.ωb ^ 2 ^ p').1 = 0

Tactic:
show 2 ^ 2 = 4 by norm_num,

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
this : X.ω ^ (2 ^ p' * 4 / 4) + X.ωb ^ (2 ^ p' * 4 / 4) = 0
⊢ (X.ω ^ 2 ^ p' + X.ωb ^ 2 ^ p').1 = 0
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n✝ : Type u_1
inst✝¹ : Fintype n✝
inst✝ : DecidableEq n✝
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
g : GL (Fin 2) ℝ
hg : g ∈ Γ
n : ℕ
hn : 0 < n
left✝ : n ≤ (mapGL ℝ).range.relIndex Γ
hgn : g ^ n ∈ (mapGL ℝ).range ⊓ Γ
this : |↑(GeneralLinearGroup.det g ^ n)| = 1
⊢ |↑(GeneralLinearGroup.det g)| = 1

Tactic:
simpa [← abs_pow, abs_pow_eq_one _ (Nat.ne_zero_of_lt hn)]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods < 𝒢.periods
u : R
hu_mem : u ∈ 𝒢.periods
hu_notMem : u ∉ 𝒢.strictPeriods
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2

Tactic:
AddSubgroup.relIndex_eq_two_iff_exists_notMem_and

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods < 𝒢.periods
u : R
hu_mem : u ∈ 𝒢.periods
hu_notMem : u ∉ 𝒢.strictPeriods
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨
    ∃ a ∈ 𝒢.periods, a ∉ 𝒢.strictPeriods ∧ ∀ b ∈ 𝒢.periods, b + a ∈ 𝒢.strictPeriods ∨ b ∈ 𝒢.strictPeriods
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_1
inst✝² : SMul α ℂ
inst✝¹ : IsScalarTower α ℂ ℂ
inst✝ : Γ.HasDetOne
c : α
f : ModularForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ IsBoundedAtImInfty ((c • f.toSlashInvariantForm).toFun ∣[k] g)

Tactic:
simp_rw [IsBoundedAtImInfty, Filter.BoundedAtFilter, SlashInvariantForm.toFun_eq_coe,
        FunLike.coe_smul, toSlashInvariantForm_coe, ← smul_one_smul ℂ c ⇑f, smul_slash]
      exact (f.bdd_at_cusps' hc g hg).const_smul_left (σ g (c • (1 : ℂ)))

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: case funProp.discharger
k : ℤ
f f' : ℍ → ℂ
hf : Continuous f
hf' : Continuous f'
⊢ ∀ (a : ℂ), a ≠ 0 ∨ 0 ≤ k

Tactic:
simp [im_ne_zero _]

Goal state after:
case funProp.discharger
k : ℤ
f f' : ℍ → ℂ
hf : Continuous f
hf' : Continuous f'
⊢ ∀ (a : ℂ), ¬a = 0 ∨ 0 ≤ k
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: case funProp.discharger
k : ℤ
f f' : ℍ → ℂ
hf : Continuous f
hf' : Continuous f'
⊢ ∀ (a : ℍ), ↑a.im ≠ 0 ∨ 0 ≤ k

Tactic:
simp [im_ne_zero _]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ (Fin 2 → ℝ) ≃ₗ[ℝ] Fin 2 → ℝ

Tactic:
refine
        LinearMap.GeneralLinearGroup.generalLinearEquiv ℝ (Fin 2 → ℝ)
          (GeneralLinearGroup.toLin (planeConformalMatrix (cd 0 : ℝ) (-(cd 1 : ℝ)) ?_))
      norm_cast
      rw [neg_sq]
      exact hcd.sq_add_sq_ne_zero

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: case right
F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
⊢ (fun x ↦ ‖f' x‖ * (‖f x‖ * x.im ^ k)) =O[atImInfty] fun τ ↦ Real.exp (-a * τ.im)

Tactic:
conv_rhs => enter [τ]; rw [← one_mul (Real.exp _)]

Goal state after:
case right
F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
⊢ (fun x ↦ ‖f' x‖ * (‖f x‖ * x.im ^ k)) =O[atImInfty] fun τ ↦ 1 * Real.exp (-a * τ.im)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hc : ↑g 1 0 = 0
⊢ ∃ n, ∀ (z : ℍ), g • z = T ^ n • z

Tactic:
have had := g.det_coe
  replace had : g 0 0 * g 1 1 = 1 := by rw [det_fin_two, hc] at had; lia
  rcases Int.eq_one_or_neg_one_of_mul_eq_one' had with (⟨ha, hd⟩ | ⟨ha, hd⟩)
  · use g 0 1
    suffices g = T ^ g 0 1 by intro z; conv_lhs => rw [this]
    ext i j; fin_cases i <;> fin_cases j <;>
      simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]
  · use -(g 0 1)
    suffices g = -T ^ (-(g 0 1)) by intro z; conv_lhs => rw [this, SL_neg_smul]
    ext i j; fin_cases i <;> fin_cases j <;>
      simp [ha, hc, hd, coe_T_zpow, show (1 : Fin (0 + 2)) = (1 : Fin 2) from rfl]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: k : ℤ
i : Fin 2 → ℤ
A : SL(2, ℤ)
z : ℍ
⊢ eisSummand k i (A • z) =
    denom (SpecialLinearGroup.toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) A)) ↑z ^ k * eisSummand k (i ᵥ* ↑A) z

Tactic:
by
  simp only [eisSummand, vecMul, vec2_dotProduct, denom, UpperHalfPlane.specialLinearGroup_apply]
  have h (a b c d u v : ℂ) (hc : c * z + d ≠ 0) : (u * ((a * z + b) / (c * z + d)) + v) ^ (-k) =
      (c * z + d) ^ k * ((u * a + v * c) * z + (u * b + v * d)) ^ (-k) := by
    replace hc : z * c + d ≠ 0 := by convert! hc using 1; ring
    field_simp
    simp [div_zpow]
    ring_nf
  simpa using h (hc := denom_ne_zero A z) ..

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty

Goal state before:
pp: k : ℤ
hk : 3 ≤ k
z : ℍ
⊢ Summable fun x ↦ ‖eisSummand k x z‖

Tactic:
by
  have hk' : (2 : ℝ) < k := by norm_cast
  apply ((summable_one_div_norm_rpow hk').mul_left <| r z ^ (-k : ℝ)).of_nonneg_of_le
    (fun _ ↦ norm_nonneg _)
  intro b
  simp only [eisSummand, norm_zpow]
  exact_mod_cast summand_bound z (show 0 ≤ (k : ℝ) by positivity) b

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h✝ : 0 < ‖↑τ.im ^ ↑k‖
t : ℝ
h : τ.im = t
ht : 0 < t
⊢ max t (1 / t) ^ ↑k / ‖↑t ^ ↑k‖ = max 1 (1 / t ^ ↑k) ^ 2

Tactic:
lift t to NNReal using ht.le

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h✝ : 0 < ‖↑τ.im ^ ↑k‖
t : NNReal
h : τ.im = ↑t
ht : 0 < ↑t
⊢ max (↑t) (1 / ↑t) ^ ↑k / ‖↑↑t ^ ↑k‖ = max 1 (1 / ↑t ^ ↑k) ^ 2
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
i j : Fin 2
⊢ ↑g i j = ↑(T ^ b) i j

Tactic:
coe_T_zpow

Goal state after:
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
i j : Fin 2
⊢ ↑g i j = !![1, b; 0, 1] i j