mathlib-initiative/mathlib-tactics huggingface dataset:
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
| Tendsto (fun x ↦ (↑n + 1) ^ ↑x * LSeries f ↑x) atTop (nhds (f (n + 1)))

Tactic:
conv =>

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
| f (n + 1) + 0
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
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_add, pow_one]

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
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p ↦ -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p ↦ -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p ↦ -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i ↦ 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i ↦ 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y)))).re
hsum₂ : Summable fun x_1 ↦ (-log (1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y)))).re
⊢ 0 ≤
    3 * ∑' (a : Nat.Primes), (-log (1 - 1 ↑↑a * ↑↑a ^ (-(1 + ↑x)))).re +
        4 * (∑' (p : Nat.Primes), -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))).re +
      (∑' (p : Nat.Primes), -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))).re

Tactic:
re_tsum H₁,

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
x : ℝ
hx : 0 < x
y : ℝ
h₀ : 1 < (1 + ↑x).re
h₁ : 1 < (1 + ↑x + I * ↑y).re
h₂ : 1 < (1 + ↑x + 2 * I * ↑y).re
H₀ : Summable fun p ↦ -log (1 - 1 ↑↑p * ↑↑p ^ (-(1 + ↑x)))
H₁ : Summable fun p ↦ -log (1 - χ ↑↑p * ↑↑p ^ (-(1 + ↑x + I * ↑y)))
H₂ : Summable fun p ↦ -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))
hsum₀ : Summable fun i ↦ 3 * (-log (1 - 1 ↑↑i * ↑↑i ^ (-(1 + ↑x)))).re
hsum₁ : Summable fun i ↦ 4 * (-log (1 - χ ↑↑i * ↑↑i ^ (-(1 + ↑x + I * ↑y)))).re
hsum₂ : Summable fun x_1 ↦ (-log (1 - (χ ^ 2) ↑↑x_1 * ↑↑x_1 ^ (-(1 + ↑x + 2 * I * ↑y)))).re
⊢ 0 ≤
    3 * ∑' (a : Nat.Primes), (-log (1 - 1 ↑↑a * ↑↑a ^ (-(1 + ↑x)))).re +
        4 * ∑' (a : Nat.Primes), (-log (1 - χ ↑↑a * ↑↑a ^ (-(1 + ↑x + I * ↑y)))).re +
      (∑' (p : Nat.Primes), -log (1 - (χ ^ 2) ↑↑p * ↑↑p ^ (-(1 + ↑x + 2 * I * ↑y)))).re
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
| Summable fun pk ↦ (↑↑pk.1)⁻¹ ^ (↑pk.2 + 3 / 2)

Tactic:
conv =>

Goal state after:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
pk : Nat.Primes × ℕ
| (↑↑pk.1)⁻¹ ^ pk.2 * (↑↑pk.1)⁻¹ ^ (3 / 2)
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)
k : ℕ
H : n + 1 < k
H₀ : 0 ≤ ↑k / (↑n + 1)
H₀' : 0 ≤ (↑n + 1) / ↑k
H₁ : ↑k / (↑n + 1) = ↑(↑k / (↑n + 1))
H₂ : (↑n + 1) / ↑k < 1
| Tendsto (fun x ↦ f k / (↑k / (↑n + 1)) ^ ↑x) atTop (nhds 0)

Tactic:
conv =>

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)
k : ℕ
H : n + 1 < k
H₀ : 0 ≤ ↑k / (↑n + 1)
H₀' : 0 ≤ (↑n + 1) / ↑k
H₁ : ↑k / (↑n + 1) = ↑(↑k / (↑n + 1))
H₂ : (↑n + 1) / ↑k < 1
x : ℝ
| f k * ↑(((↑n + 1) / ↑k) ^ x)
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
| Summable fun x ↦ ∑' (y : ℕ), (↑↑x)⁻¹ ^ y * (↑↑x)⁻¹ ^ (3 / 2)

Tactic:
conv =>

Goal state after:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
p : Nat.Primes
| (1 - (↑↑p)⁻¹)⁻¹ * (↑↑p)⁻¹ ^ (3 / 2)
Module: Mathlib.NumberTheory.ZetaValues

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

Tactic:
rw [pow_add, pow_one]

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

Goal state before:
pp: k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
⊢ HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * Real.sin (2 * π * ↑n * x))
    ((-1) ^ (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))

Tactic:
have :
    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) := by
    convert! hasSum_one_div_nat_pow_mul_fourier (by lia : 2 ≤ 2 * k + 1) hx using 1
    · ext1 n
      rw [pow_add (-1 : ℂ), pow_mul (-1 : ℂ), neg_one_sq, one_pow, one_mul, pow_one, ←
        neg_eq_neg_one_mul, ← sub_eq_add_neg]
    · congr
      rw [pow_add, pow_one]
      conv_rhs =>
        rw [mul_pow]
        congr
        congr
        · skip
        · rw [pow_add, pow_one, pow_mul, I_sq]
      ring

Goal state after:
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))
⊢ HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * Real.sin (2 * π * ↑n * x))
    ((-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.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)
k : ℕ
H : n + 1 < k
H₀ : 0 ≤ ↑k / (↑n + 1)
H₀' : 0 ≤ (↑n + 1) / ↑k
H₁ : ↑k / (↑n + 1) = ↑(↑k / (↑n + 1))
H₂ : (↑n + 1) / ↑k < 1
| Tendsto (fun x ↦ f k * ↑(((↑n + 1) / ↑k) ^ x)) atTop (nhds 0)

Tactic:
conv =>

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)
k : ℕ
H : n + 1 < k
H₀ : 0 ≤ ↑k / (↑n + 1)
H₀' : 0 ≤ (↑n + 1) / ↑k
H₁ : ↑k / (↑n + 1) = ↑(↑k / (↑n + 1))
H₂ : (↑n + 1) / ↑k < 1
| f k * 0
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case e_a
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ L (fun n ↦ ↑(residueClass a n)) ↑x = ↑(L (fun n ↦ ↑(residueClass a n)) ↑x).re

Tactic:
LSeries,

Goal state after:
case e_a
q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ ∑' (n : ℕ), term (fun n ↦ ↑(residueClass a n)) (↑x) n = ↑(∑' (n : ℕ), term (fun n ↦ ↑(residueClass a n)) (↑x) n).re
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)) * I / 2 =
    (cexp (-(2 * ↑π * ↑x✝ * ↑x) * I) - cexp (2 * ↑π * ↑x✝ * ↑x * I)) * I / 2

Tactic:
neg_sub

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)) * I / 2 =
    (cexp (-(2 * ↑π * ↑x✝ * ↑x) * I) - cexp (2 * ↑π * ↑x✝ * ↑x * I)) * I / 2
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ ∑' (a_1 : ℕ), ↑(residueClass a a_1) / ↑a_1 ^ ↑x = L (fun n ↦ ↑(residueClass a n)) ↑x

Tactic:
LSeries,

Goal state after:
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ ∑' (a_1 : ℕ), ↑(residueClass a a_1) / ↑a_1 ^ ↑x = ∑' (n : ℕ), term (fun n ↦ ↑(residueClass a n)) (↑x) n
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
⊢ LSeries f = 0

Tactic:
ext1 s

Goal state after:
f : ℕ → ℂ
h : abscissaOfAbsConv f = ⊤
s : ℂ
⊢ LSeries f s = 0 s
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f : ℕ → ℂ
h : ¬abscissaOfAbsConv f = ⊤
F : ℕ → ℂ := fun n ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha : ¬abscissaOfAbsConv F = ⊤
h' : ∀ (x : ℝ), LSeries F ↑x = LSeries f ↑x
n : ℕ
s : Set ℝ
hs : s ∈ atTop ∧ Set.EqOn (fun x ↦ LSeries f ↑x) 0 s
⊢ ∃ s ∈ atTop, Set.EqOn (fun x ↦ ↑n ^ ↑x * LSeries f ↑x) (fun x ↦ 0) s

Tactic:
exact ⟨s, hs.1, fun x hx ↦ by simp [hs.2 hx]⟩

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

Goal state before:
pp: f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
⊢ f = 0

Tactic:
ext (- | m)

Goal state after:
case zero
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
⊢ f 0 = 0 0

case succ
f : ℕ → ℂ
hf : f 0 = 0
h : ¬abscissaOfAbsConv f = ⊤
H : LSeries f = 0
H' : ∀ (n : ℕ), n ≠ 0 → f n = 0
m : ℕ
⊢ f (m + 1) = 0 (m + 1)
Module: Mathlib.NumberTheory.LegendreSymbol.Complex

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
⊢ (primitiveChar_to_Complex F).IsPrimitive

Tactic:
refine IsPrimitive.compMulHom_of_isPrimitive (PrimitiveAddChar.prim _) ?_

Goal state after:
F : Type u_1
inst✝¹ : Field F
inst✝ : Finite F
⊢ Function.Injective
    ⇑(IsCyclotomicExtension.algEquiv {↑(primitiveChar F ℂ ⋯).n} ℂ (CyclotomicField ↑(primitiveChar F ℂ ⋯).n ℂ)
            ℂ).toMulEquiv.toMonoidHom
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: n q : ℕ
a : ℤ
hq : q ≠ 0
h : IsCoprime a ↑q
this✝ : NeZero q
this : IsUnit ↑a
p : ℕ
hpn : p > n
hpp : Prime p
heq : ↑p = ↑a
⊢ ↑p ≡ a [ZMOD ↑q]

Tactic:
simpa [← ZMod.intCast_eq_intCast_iff] using heq

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

Goal state before:
pp: b : ℕ
z : ℤ
hz : z ∈ List.pmap (fun p pp ↦ legendreSym p 1) b.primeFactorsList ⋯
p : ℕ
hp : p ∈ b.primeFactorsList
he : legendreSym p 1 = z
⊢ z = 1

Tactic:
rw [← he, legendreSym.at_one]

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

Goal state before:
pp: a b : ℕ
ha : Odd a
hb : Odd b
⊢ J(↑a | b) = qrSign b a * J(↑b | a)

Tactic:
quadratic_reciprocity' ha hb

Goal state after:
a b : ℕ
ha : Odd a
hb : Odd b
⊢ qrSign b a * J(↑b | a) = qrSign b a * J(↑b | a)
Module: Mathlib.NumberTheory.LocalField.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this✝ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := isUniformAddGroup_of_addCommGroup
s : Set K
hs : s ∈ nhds 0
hs' : IsCompact s
r' : K
hr' : ¬r' = 0
hr✝ : (valuation K) r' < 1
r : K
hrs : {x | (valuation K) x < (valuation K) r} ⊆ s
hr1 : (valuation K) r < 1
hr : ¬r = 0
⊢ ∃ r', r' ≠ 0 ∧ (valuation K) r' < 1 ∧ {x | (valuation K) x ≤ (valuation K) r'} ⊆ s

Tactic:
refine ⟨r ^ 2, by simpa using hr, by simpa [pow_two], fun x hx ↦ hrs ?_⟩

Goal state after:
case inl
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this✝ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := isUniformAddGroup_of_addCommGroup
s : Set K
hs : s ∈ nhds 0
hs' : IsCompact s
r' : K
hr' : ¬r' = 0
hr✝ : (valuation K) r' < 1
r : K
hrs : {x | (valuation K) x < (valuation K) r} ⊆ s
hr1 : (valuation K) r < 1
hr : ¬r = 0
x : K
hx : x ∈ {x | (valuation K) x ≤ (valuation K) (r ^ 2)}
⊢ x ∈ {x | (valuation K) x < (valuation K) r}
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: case refine_2
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
p : ↑↑(Finset.Icc (fun x ↦ ⌈B₁ x⌉) fun x ↦ ⌊B₂ x⌋)
⊢ (ofFn (n + 1)) ↑p ∈ boxPoly n B₁ B₂

Tactic:
refine ⟨Nat.le_of_lt_succ <| ofFn_natDegree_lt (Nat.le_add_left 1 n) p.val, fun i ↦ ?_⟩
      have prop := Finset.mem_Icc.mp p.property
      rw [ofFn_coeff_eq_val_of_lt _ i.2]
      exact ⟨ceil_le.mp (prop.1 i), le_floor.mp (prop.2 i)⟩

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
q k : ℕ
ih : sModNatAux (4 % q) q k = sModNat q k
⊢ (sModNatAux (4 % q) q k ^ 2 + (q - 2)) % q = sModNat q (k + 1)

Tactic:
ih,

Goal state after:
case succ
q k : ℕ
ih : sModNatAux (4 % q) q k = sModNat q k
⊢ (sModNat q k ^ 2 + (q - 2)) % q = sModNat q (k + 1)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
q✝ i q k : ℕ
ih : ∀ (b : ℕ), sModNatTR.go q k b = sModNatAux b q k
b : ℕ
⊢ sModNatTR.go q k ((b ^ 2 + (q - 2)) % q) = sModNatAux b q (k + 1)

Tactic:
ih,

Goal state after:
case succ
q✝ i q k : ℕ
ih : ∀ (b : ℕ), sModNatTR.go q k b = sModNatAux b q k
b : ℕ
⊢ sModNatAux ((b ^ 2 + (q - 2)) % q) q k = sModNatAux b q (k + 1)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ.succ
q✝ i q b k : ℕ
ih : sModNatAux ((b ^ 2 + (q - 2)) % q) q k = (sModNatAux b q k ^ 2 + (q - 2)) % q
⊢ (sModNatAux ((b ^ 2 + (q - 2)) % q) q k ^ 2 + (q - 2)) % q = (sModNatAux b q (k + 1) ^ 2 + (q - 2)) % q

Tactic:
ih,

Goal state after:
case succ.succ
q✝ i q b k : ℕ
ih : sModNatAux ((b ^ 2 + (q - 2)) % q) q k = (sModNatAux b q k ^ 2 + (q - 2)) % q
⊢ (((sModNatAux b q k ^ 2 + (q - 2)) % q) ^ 2 + (q - 2)) % q = (sModNatAux b q (k + 1) ^ 2 + (q - 2)) % q
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
⊢ A ∈ Gamma0 N

Tactic:
simp [ha.right.right, Gamma0_mem]

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

Goal state before:
pp: g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ↑g
A₂ : Matrix (Fin 2) (Fin 2) ℚ := ↑g⁻¹
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
⊢ ∃ N, N ≠ 0 ∧ ∀ x ∈ Γ(N), g * (mapGL ℚ) x * g⁻¹ ∈ Subgroup.map (mapGL ℚ) Γ(M)

Tactic:
refine ⟨a₁ * a₂ * M, mul_ne_zero (mul_ne_zero A₁.den_ne_zero A₂.den_ne_zero) (NeZero.ne _),
    fun ⟨y, hy⟩ hy' ↦ ?_⟩

Goal state after:
g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ↑g
A₂ : Matrix (Fin 2) (Fin 2) ℚ := ↑g⁻¹
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x✝ : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : ⟨y, hy⟩ ∈ Γ(a₁ * a₂ * M)
⊢ g * (mapGL ℚ) ⟨y, hy⟩ * g⁻¹ ∈ Subgroup.map (mapGL ℚ) Γ(M)
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ↑g
A₂ : Matrix (Fin 2) (Fin 2) ℚ := ↑g⁻¹
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x✝ : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : ⟨y, hy⟩ ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
this : (z.map Int.cast).det = A₁.det * (y.map Int.cast).det * A₂.det
⊢ z.det = 1

Tactic:
← Int.cast_det

Goal state after:
g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ↑g
A₂ : Matrix (Fin 2) (Fin 2) ℚ := ↑g⁻¹
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x✝ : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : ⟨y, hy⟩ ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
this : ↑z.det = A₁.det * ↑y.det * A₂.det
⊢ z.det = 1
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : ↑g ∉ Set.range ⇑(Matrix.scalar (Fin 2))
hdisc : (↑g 0 0 + ↑g 1 1) ^ 2 - 4 * (↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0) = 0
c : K
hc : ↑g 1 0 = 0
hd : ↑g 1 1 = ↑g 0 0
⊢ ↑g 0 1 ≠ 0

Tactic:
refine fun hb ↦ fixpointPolynomial_eq_zero_iff.not.mpr hg ?_

Goal state after:
case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : ↑g ∉ Set.range ⇑(Matrix.scalar (Fin 2))
hdisc : (↑g 0 0 + ↑g 1 1) ^ 2 - 4 * (↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0) = 0
c : K
hc : ↑g 1 0 = 0
hd : ↑g 1 1 = ↑g 0 0
hb : ↑g 0 1 = 0
⊢ g.fixpointPolynomial = 0
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

Goal state before:
pp: c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (mapGL ℝ).range
⊢ c.IsBoundedAt f k ↔ ∃ γ, (mapGL ℝ) γ • ∞ = c ∧ IsBoundedAtImInfty (f ∣[k] γ)

Tactic:
constructor
  · obtain ⟨γ, rfl⟩ := isCusp_SL2Z_iff'.mp hc
    simpa [IsBoundedAt.smul_iff, isBoundedAt_infty_iff] using! fun hfc ↦ ⟨γ, rfl, hfc⟩
  · rintro ⟨γ, rfl, b⟩
    simpa [IsBoundedAt.smul_iff, isBoundedAt_infty_iff] using! b

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

Goal state before:
pp: ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
s : Finset ι
⊢ (∏ i ∈ s, f i) ∣[∑ i ∈ s, k i] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (↑(#s) - 1) • ∏ i ∈ s, f i ∣[k i] g

Tactic:
induction s using Finset.induction_on with
  | empty =>
    simp only [sum_empty, prod_empty, Matrix.GeneralLinearGroup.val_det_apply, card_empty,
      CharP.cast_eq_zero, zero_sub, Int.reduceNeg, zpow_neg, zpow_one]
    ext _
    simp [slash_apply]
  | insert i t hi IH =>
    rcases t.eq_empty_or_nonempty with rfl | ht
    · simp
    simp only [prod_insert hi, card_insert_of_notMem hi, Nat.cast_succ, add_sub_cancel_right,
    show ∑ i ∈ insert i t, k i = (k i) + ∑ i ∈ t, k i by grind, mul_slash, IH, mul_smul_comm,
      ← mul_smul]
    congr 1
    nth_rw 2 [show (#t : ℤ) = 1 + (#t - 1) by grind]
    rw [zpow_add', zpow_one]
    left
    exact abs_ne_zero.mpr (Matrix.GeneralLinearGroup.det_ne_zero g)

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : SlashInvariantFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
f : F
c : ℂ
hf : ⇑f = Function.const ℍ c
⊢ k = 0 ∨ c = 0

Tactic:
have : SlashInvariantFormClass F Γ(1) k := Gamma_one_coe_eq_SL ▸ ‹_›
  have hI := slash_action_eqn_SL'' f (mem_Gamma_one S) I
  have h2I2 := slash_action_eqn_SL'' f (mem_Gamma_one S) ((⟨2, two_pos⟩ : {x : ℝ // 0 < x}) • .I)
  simp_rw [sl_moeb, hf, Function.const, denom_S] at hI h2I2
  suffices (2 : ℂ) ^ k = 1 ↔ k = 0 by
    simpa [mul_zpow, zpow_ne_zero, this] using h2I2.symm.trans hI
  simpa using ofReal_inj.trans <| zpow_eq_one_iff_right₀ (two_pos.le : (0 : ℝ) ≤ 2) (by norm_num1)

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: k : ℤ
hk : k < 0
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) = 0

Tactic:
refine rank_eq_zero_iff.mpr fun f ↦ ⟨_, one_ne_zero, ?_⟩
  simpa [← FunLike.coe_zero_iff] using levelOne_neg_weight_eq_zero hk f

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

Goal state before:
pp: case pos
E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg✝ : g • τ ∈ 𝒟
hg : ↑g 1 0 = 0
this : ↑g 1 1 ≠ 0
⊢ τ.im / Complex.normSq (↑(↑g 1 0) * ↑τ + ↑(↑g 1 1)) ≤ max τ.im (1 / τ.im)

Tactic:
have : (1 : ℝ) ≤ g 1 1 ^ 2 := mod_cast (one_le_sq_iff_one_le_abs _).mpr (Int.one_le_abs this)

Goal state after:
case pos
E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg✝ : g • τ ∈ 𝒟
hg : ↑g 1 0 = 0
this✝ : ↑g 1 1 ≠ 0
this : 1 ≤ ↑(↑g 1 1) ^ 2
⊢ τ.im / Complex.normSq (↑(↑g 1 0) * ↑τ + ↑(↑g 1 1)) ≤ max τ.im (1 / τ.im)
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
| (2 * ↑π * Complex.I)⁻¹ *
      ∫ (θ : ℝ) in 0..h * (2 * π / h),
        deriv (circleMap 0 R) θ • (cuspFunction h f (circleMap 0 R θ) / circleMap 0 R θ ^ (n + 1)) =
    1 / ↑h * ∫ (u : ℝ) in 0..h, 1 / 𝕢 h (↑u + ↑t * ↑I) ^ n * f { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }

Tactic:
conv =>

Goal state after:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
| 0 * (2 * π / h)
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
| ∃ C, ∀ (τ : ℍ), ‖petersson k (⇑f) (⇑f') τ‖ ≤ C * max τ.im (1 / τ.im) ^ k

Tactic:
conv =>

Goal state after:
k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
C : ℝ
τ : ℍ
| ‖‖petersson k (⇑f) (⇑f') τ‖‖