mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.LSeries.ZMod

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

Tactic:
← (Equiv.neg _).sum_comp _ _ (by simp),

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

Goal state before:
pp: case succ
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
i : ∫ (x : ℝ) in 0..(↑m)⁻¹, f (k + 1) x = 0
⊢ ∀ (x : ℝ), f (k + 1) x = 0

Tactic:
simp only [fc, intervalIntegral.integral_const, sub_zero, smul_eq_mul, mul_eq_zero, inv_eq_zero,
      Nat.cast_eq_zero, m0, false_or] at i

Goal state after:
case succ
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
i : c = 0
⊢ ∀ (x : ℝ), f (k + 1) x = 0
Module: Mathlib.NumberTheory.KummerDedekind

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

Tactic:
Multiset.map_singleton,

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
⊢ LFunction Φ s = ↑N ^ (-s) * ∑ j, Φ j * hurwitzZetaEven (toAddCircle j) s

Tactic:
by
  simp only [LFunction, hurwitzZeta, mul_add (Φ _), sum_add_distrib]
  congr 1
  simp only [add_eq_left, ← neg_eq_self, ← sum_neg_distrib]
  refine Fintype.sum_equiv (.neg _) _ _ fun i ↦ ?_
  simp only [Equiv.neg_apply, hΦ i, map_neg, hurwitzZetaOdd_neg, mul_neg]

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

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

Tactic:
← hurwitzZeta_zero,

Goal state after:
case inr
k : ℕ
hk : k ≠ 0
⊢ hurwitzZeta 0 (-↑k) = -↑(bernoulli' (k + 1)) / (↑k + 1)
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:
by
  simpa [LSeriesHasSum, term_sub] using! HasSum.sub hf hg

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
n : ℤ
⊢ 1 / ↑n ^ k * (fourier n) ↑y = (2 * ↑π * I) ^ k / ((2 * ↑π * I) ^ k * ↑n ^ k) * (fourier n) ↑y

pp: case e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
n : ℤ
⊢ ↑k ! ≠ 0

Tactic:
← div_div,

Goal state after:
case e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
n : ℤ
⊢ 1 / ↑n ^ k * (fourier n) ↑y = (2 * ↑π * I) ^ k / (2 * ↑π * I) ^ k / ↑n ^ k * (fourier n) ↑y

case e'_5.h
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
y : ℝ
hy : y ∈ Ico 0 1
B : C(𝕌, ℂ) := { toFun := ofReal ∘ periodizedBernoulli k, continuous_toFun := ⋯ }
step1 : ∀ (n : ℤ), fourierCoeff (⇑B) n = -↑k ! / (2 * ↑π * I * ↑n) ^ k
step2 : HasSum (fun i ↦ (-↑k ! / (2 * ↑π * I * ↑i) ^ k) • (fourier i) ↑y) (B ↑y)
n : ℤ
⊢ ↑k ! ≠ 0
Module: Mathlib.NumberTheory.LSeries.ZMod

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

Tactic:
by rw [inv_I, neg_neg]

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

Goal state before:
pp: a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
⊢ 0 ≤ 3 * (a ^ n / ↑n) + 4 * (a ^ n * (z ^ n).re / ↑n) + a ^ n * ((z ^ 2) ^ n).re / ↑n

Tactic:
rcases n.eq_zero_or_pos with rfl | hn

Goal state after:
case inl
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
⊢ 0 ≤ 3 * (a ^ 0 / ↑0) + 4 * (a ^ 0 * (z ^ 0).re / ↑0) + a ^ 0 * ((z ^ 2) ^ 0).re / ↑0

case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * (a ^ n / ↑n) + 4 * (a ^ n * (z ^ n).re / ↑n) + a ^ n * ((z ^ 2) ^ n).re / ↑n
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
⊢ ContinuousOn (LFunctionResidueClassAux a) {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Tactic:
rw [show LFunctionResidueClassAux a = fun s ↦ _ from rfl]

Goal state after:
q : ℕ
a : ZMod q
inst✝ : NeZero q
⊢ ContinuousOn (fun s ↦ LFunctionResidueClassAux a s) {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
⊢ LFunction χ s ≠ 0

Tactic:
by
  by_cases h : χ ^ 2 = 1 ∧ s = 1
  · exact h.2 ▸ LFunction_apply_one_ne_zero_of_quadratic h.1 <| hχs.neg_resolve_right h.2
  · have hs' : s = 1 + I * s.im := by
      conv_lhs => rw [← re_add_im s, hs, ofReal_one, mul_comm]
    rw [not_and_or, ← ne_eq, ← ne_eq, hs', add_ne_left] at h
    replace h : χ ^ 2 ≠ 1 ∨ s.im ≠ 0 :=
      h.imp_right (fun H ↦ by exact_mod_cast right_ne_zero_of_mul H)
    exact hs'.symm ▸ χ.LFunction_ne_zero_of_not_quadratic_or_ne_one h

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

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

Tactic:
← div_div,

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

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

Tactic:
← div_div,

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

Goal state before:
pp: case refine_1
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
x : ℝ
hx : 1 < x
n : ℕ
⊢ residueClass a n / ↑n ^ x ≤ residueClass a n / ↑n

Tactic:
rcases n.eq_zero_or_pos with rfl | hn

Goal state after:
case refine_1.inl
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
x : ℝ
hx : 1 < x
⊢ residueClass a 0 / ↑0 ^ x ≤ residueClass a 0 / ↑0

case refine_1.inr
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
x : ℝ
hx : 1 < x
n : ℕ
hn : n > 0
⊢ residueClass a n / ↑n ^ x ≤ residueClass a n / ↑n
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
h₄ : ∀ (n : ℕ), ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k
hO : (fun n ↦ ∑ k ∈ Icc 0 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ -(s + 1).re + r ≤ (-s - 1).re + r

Tactic:
rw [← neg_re, neg_add']

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ (∏ x ∈ Ico 1 (p / 2).succ, if (↑a * ↑x).val ≤ p / 2 then 1 else -1) *
      ∏ x ∈ Ico 1 (p / 2).succ, ↑(↑a * ↑x).valMinAbs.natAbs =
    (-1) ^ #({x ∈ Ico 1 (p / 2).succ | ¬(↑a * ↑x).val ≤ p / 2}) * ∏ x ∈ Ico 1 (p / 2).succ, ↑(↑a * ↑x).valMinAbs.natAbs

Tactic:
Finset.prod_ite

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ((∏ x ∈ Ico 1 (p / 2).succ with (↑a * ↑x).val ≤ p / 2, 1) *
        ∏ x ∈ Ico 1 (p / 2).succ with ¬(↑a * ↑x).val ≤ p / 2, -1) *
      ∏ x ∈ Ico 1 (p / 2).succ, ↑(↑a * ↑x).valMinAbs.natAbs =
    (-1) ^ #({x ∈ Ico 1 (p / 2).succ | ¬(↑a * ↑x).val ≤ p / 2}) * ∏ x ∈ Ico 1 (p / 2).succ, ↑(↑a * ↑x).valMinAbs.natAbs
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case refine_1
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
h₂ : (fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t ↦ t ^ 1
⊢ (fun t ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) =O[atTop] fun t ↦ t ^ (-s)

Tactic:
refine IsBigO.mul_atTop_rpow_of_isBigO_rpow 1 (-s - 1) _ h₂ ?_ (by linarith)

Goal state after:
case refine_1
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
s : ℝ
hs : 1 < s
h₁ : LocallyIntegrableOn (fun t ↦ (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-↑s - 1)) (Set.Ici 1) volume
h₂ : (fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k) =O[atTop] fun t ↦ t ^ 1
⊢ (fun t ↦ ↑t ^ (-↑s - 1)) =O[atTop] fun t ↦ t ^ (-s - 1)
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : Subsingleton (ValueGroupWithZero R)ˣ
y : ValueGroupWithZero R
hy : 0 < y
⊢ 1 ≤ y

Tactic:
have : 1 = Units.mk0 y hy.ne' := Subsingleton.elim _ _

Goal state after:
case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this✝ : IsRankLeOne R
h : Subsingleton (ValueGroupWithZero R)ˣ
y : ValueGroupWithZero R
hy : 0 < y
this : 1 = Units.mk0 y ⋯
⊢ 1 ≤ y
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
hpo : Odd p
q : ℕ
pq : Nat.Prime q
hq : q ≠ 2
hqo : Odd q
⊢ legendreSym q ↑p = qrSign q p * J(↑q | p)

Tactic:
← @legendreSym.to_jacobiSym p ⟨pp⟩,

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
q : ℕ
pq : Nat.Prime q
hq : q ≠ 2
hqo : Odd q
⊢ legendreSym q ↑p = qrSign q p * legendreSym p ↑q
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
⊢ ∃ x, 0 < ‖↑x‖ ∧ ‖↑x‖ < 1

Tactic:
obtain ⟨x, hx, hx'⟩ := NormedField.exists_norm_lt_one K
  refine ⟨⟨x, hx'.le⟩, ?_⟩
  simpa [hx', Subtype.ext_iff] using hx

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
⊢ MulArchimedean ↥(MonoidHom.mrange v)

Tactic:
by
  rw [← Units.mulArchimedean_iff]
  obtain ⟨_⟩ := locallyFiniteOrder_units_mrange_of_isCompact_integer hc
  exact MulArchimedean.of_locallyFiniteOrder

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

Goal state before:
pp: H K : Subgroup SL(2, ℤ)
h : H ≤ K
h2 : IsCongruenceSubgroup H
⊢ IsCongruenceSubgroup K

Tactic:
obtain ⟨N, hN⟩ := h2
  exact ⟨N, hN.1, hN.2.trans h⟩

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

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
g x : SL(2, ℤ)
⊢ g * x * g⁻¹ ∈ Γ ↔ x ∈ (toConjAct g)⁻¹ • Γ

Tactic:
Subgroup.mem_inv_pointwise_smul_iff,

Goal state after:
Γ : Subgroup SL(2, ℤ)
g x : SL(2, ℤ)
⊢ g * x * g⁻¹ ∈ Γ ↔ toConjAct g • x ∈ Γ
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.det = A₁.det * A₂.det * ↑y.det
⊢ z.det = 1

Tactic:
← Matrix.det_mul,

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₁ * A₂).det * ↑y.det
⊢ z.det = 1
Module: Mathlib.NumberTheory.ModularForms.SlashActions

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

Tactic:
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]

Goal state after:
case empty
ι : Type u_1
k : ι → ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
⊢ 1 ∣[0] g = |(↑g).det|⁻¹ • 1
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mpr
g : SL(2, ℤ)
⊢ (mapGL ℝ) g • ∞ ∈ Set.range (OnePoint.map Rat.cast)

Tactic:
refine ⟨mapGL ℚ g • ∞, ?_⟩

Goal state after:
case mpr
g : SL(2, ℤ)
⊢ OnePoint.map Rat.cast ((mapGL ℚ) g • ∞) = (mapGL ℝ) g • ∞
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mp
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
g : SL(2, ℤ)
hx : (mapGL ℝ) g = upperRightHom x
hg : ↑(↑g 0 1) = 0
⊢ ↑N ∣ ↑g 0 1

Tactic:
← ZMod.intCast_zmod_eq_zero_iff_dvd

Goal state after:
case mp
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
g : SL(2, ℤ)
hx : (mapGL ℝ) g = upperRightHom x
hg : ↑(↑g 0 1) = 0
⊢ ↑(↑g 0 1) = 0
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: ι : Type
s : Finset ι
k : ι → ℤ
m : ℤ
hm : m = ∑ i ∈ s, k i
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
F : (i : ι) → ModularForm Γ (k i)
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
γ : GL (Fin 2) ℝ
hγ : γ • OnePoint.infty = c✝
⊢ IsBoundedAtImInfty ((SlashInvariantForm.prod m hm fun i ↦ { toFun := ⇑(F i), slash_action_eq' := ⋯ }).toFun ∣[m] γ)

Tactic:
by
    simp only [SlashInvariantForm.toFun_eq_coe, coe_prod, SlashInvariantForm.coe_mk, hm,
      prod_slash_sum_weights, IsBoundedAtImInfty]
    refine BoundedAtFilter.smul _ (BoundedAtFilter.prod (s := s) ?_)
    intro i hi
    simpa using! (F i).bdd_at_cusps' hc γ hγ

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

Goal state before:
pp: N : ℕ
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
z : ℍ
⊢ ‖∑' (x : ↑(gammaSet N 1 a)), eisSummand k (↑x) z‖ ≤ ∑' (x : Fin 2 → ℤ), ‖eisSummand k x z‖

Tactic:
apply le_trans (norm_tsum_le_tsum_norm ((summable_norm_eisSummand hk z).subtype _))
    (Summable.tsum_subtype_le (fun (x : Fin 2 → ℤ) ↦ ‖(eisSummand k x z)‖) _ (fun _ ↦ norm_nonneg _)
      (summable_norm_eisSummand hk z))

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

Goal state before:
pp: h : ℝ
⊢ cuspFunction h 0 = 0

Tactic:
simpa [cuspFunction, Periodic.cuspFunction]
    using! (tendsto_const_nhds.mono_left nhdsWithin_le_nhds).limUnder_eq

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
r : 𝕜
hr : ‖r‖ < 1
k : ℕ
this : ∀ (m : ℕ) [NeZero m], ∑' (n : ℕ), (r ^ m) ^ n = (1 - r ^ m)⁻¹
⊢ ∑' (n : ℕ+), ↑↑n ^ k * r ^ ↑n / (1 - r ^ ↑n) = ∑' (n : ℕ+), ↑((σ k) ↑n) * r ^ ↑n

Tactic:
simp only [div_eq_mul_inv, ← this, ← tsum_mul_left, mul_assoc, ← _root_.pow_succ',
    ← fun (n : ℕ) ↦ tsum_pnat_eq_tsum_succ (f := fun m ↦ n ^ k * (r ^ n) ^ m)]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
r : 𝕜
hr : ‖r‖ < 1
k : ℕ
this : ∀ (m : ℕ) [NeZero m], ∑' (n : ℕ), (r ^ m) ^ n = (1 - r ^ m)⁻¹
⊢ ∑' (n : ℕ+) (n_1 : ℕ+), ↑↑n ^ k * (r ^ ↑n) ^ ↑n_1 = ∑' (n : ℕ+), ↑((σ k) ↑n) * r ^ ↑n
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs

Goal state before:
pp: ⊢ D2 1 = 0

Tactic:
by
  ext z
  simp [D2]

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

Goal state before:
pp: this :
  (Summable fun n ↦ (1 / 2) ^ (n + 1)) →
    (∀ (k : ℕ), Tendsto (fun x ↦ -x ^ (k + 1)) (𝓝 0) (𝓝 0)) →
      (∀ᶠ (n : ℂ) in 𝓝 0, ∀ (k : ℕ), ‖n‖ ^ (k + 1) ≤ (1 / 2) ^ (k + 1)) →
        Tendsto (fun n ↦ ∏' (k : ℕ), (1 + -n ^ (k + 1))) (𝓝 0) (𝓝 1)
k : ℕ
⊢ Tendsto (fun x ↦ -x ^ (k + 1)) (𝓝 0) (𝓝 0)

Tactic:
by simpa using ((continuous_pow (M := ℂ) (k + 1)).tendsto 0).neg

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℂ
⊢ x ∈ UpperHalfPlane.coe '' 𝒟 ↔ x ∈ {z | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}

Tactic:
refine ⟨?_, fun ⟨hxim, hxnorm, hxre⟩ ↦ ⟨⟨x, hxim⟩, ⟨one_le_normSq_iff.mpr hxnorm, hxre⟩, rfl⟩⟩

Goal state after:
x : ℂ
⊢ x ∈ UpperHalfPlane.coe '' 𝒟 → x ∈ {z | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case refine_1
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
⊢ ↑p ∣ ∑ i ∈ range p, x ^ i * y ^ (p - ↑1 - i)

Tactic:
exact dvd_geom_sum₂_self hxy

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

Goal state before:
pp: case e'_5
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
n : ℕ
p : ℂ
⊢ p / ↑n ^ s = ↑π ^ (-s) * Gamma s * p / ↑(2 * ↑n / h Γ) ^ s * (2 / (2 * (2 * ↑π) ^ (-s) * Gamma s) * ↑(h Γ) ^ (-s))

Tactic:
← div_div,

Goal state after:
case e'_5
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
n : ℕ
p : ℂ
⊢ p / ↑n ^ s = ↑π ^ (-s) * Gamma s * p / ↑(2 * ↑n / h Γ) ^ s * (2 / (2 * (2 * ↑π) ^ (-s)) / Gamma s * ↑(h Γ) ^ (-s))
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: case e'_5
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
n : ℕ
p : ℂ
⊢ p / ↑n ^ s = ↑π ^ (-s) * Gamma s * p / ↑(2 * ↑n / h Γ) ^ s * (2 / (2 * (2 * ↑π) ^ (-s)) / Gamma s * ↑(h Γ) ^ (-s))

Tactic:
← div_div,

Goal state after:
case e'_5
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
n : ℕ
p : ℂ
⊢ p / ↑n ^ s = ↑π ^ (-s) * Gamma s * p / ↑(2 * ↑n / h Γ) ^ s * (2 / 2 / (2 * ↑π) ^ (-s) / Gamma s * ↑(h Γ) ^ (-s))