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

Goal state before:
pp: case e'_6
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)
⊢ ↑(bernoulliFun k y) = B ↑y

Tactic:
· rw [ContinuousMap.coe_mk, Function.comp_apply, ofReal_inj, periodizedBernoulli,
      AddCircle.liftIco_coe_apply (show y ∈ Ico 0 (0 + 1) by rwa [zero_add])]

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

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

Goal state before:
pp: 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
⊢ Summable fun n ↦ (if Nat.Prime n then 0 else residueClass a n) / ↑n

Tactic:
refine Summable.of_nonneg_of_le h₀ hleF₀ ?_

Goal state after:
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
⊢ Summable F₀
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✝ : ℕ
⊢ 1 / ↑x✝ ^ (2 * k + 1) = ↑(1 / ↑x✝ ^ (2 * k + 1))

Tactic:
ofReal_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✝ : ℕ
⊢ 1 / ↑x✝ ^ (2 * k + 1) = ↑1 / ↑(↑x✝ ^ (2 * k + 1))
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
h : ¬(χ ^ 2 = 1 ∧ s = 1)
| s

Tactic:
rw [← re_add_im s, hs, ofReal_one, mul_comm]

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
s : ℂ
hs : s.re = 1
hχs : χ ≠ 1 ∨ s ≠ 1
h : ¬(χ ^ 2 = 1 ∧ s = 1)
| 1 + I * ↑s.im
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:
ofReal_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.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:
ofReal_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.SumCoeff

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

Tactic:
sum_insert (by aesop),

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

Goal state before:
pp: s T ε : ℝ
S : ℝ → ℂ
hs : 1 < s
hS₁ : LocallyIntegrableOn (fun t ↦ S t) (Set.Ici 1) volume
hS₂ : ∀ t ≥ T, ‖S t‖ ≤ ε * t
h : LocallyIntegrableOn (fun t ↦ ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
t : ℝ
ht : T ≤ t
ht' : 0 < t
⊢ ‖‖S t‖ * t ^ (-s - 1)‖ ≤ ε * ‖t ^ (-s)‖

Tactic:
simpa [abs_of_nonneg, Real.rpow_nonneg, ht'.le, Real.rpow_sub ht', mul_assoc, ht'.ne',
      mul_div_cancel₀] using mul_le_mul_of_nonneg_right (hS₂ t ht) (norm_nonneg <| t ^ (-s - 1))

Goal state after:
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
⊢ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖ ≤ (s - 1) * s * C + s * ε

Tactic:
have h₃ : (s - 1) * ∫ (t : ℝ) in Set.Ioi 1, (t : ℂ) ^ (-s : ℂ) = 1 := by
    rw [integral_Ioi_cpow_of_lt (by rwa [neg_re, neg_lt_neg_iff]) zero_lt_one, ofReal_one,
      one_cpow, show -(s : ℂ) + 1 = -(s - 1) by ring, neg_div_neg_eq, mul_div_cancel₀]
    exact (sub_ne_zero.trans ofReal_ne_one).mpr hs.ne'

Goal state after:
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
⊢ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖ ≤ (s - 1) * s * C + s * ε
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

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

Tactic:
obtain ⟨b, rfl⟩ := Nat.dvd_of_mod_eq_zero hb2

Goal state after:
case neg
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
⊢ J(a | 2 * b) = J(a | 2 * b / 2)
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case hft
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
⊢ IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ioi T) volume

Tactic:
exact h₁.mono_set <| Set.Ioi_subset_Ici_self.trans <| Set.Ici_subset_Ici.mpr hT₁

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case base
n : ℕ
⊢ mersenne 2 % 4 = 3

Tactic:
| base =>

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case base
k : ℕ
⊢ mersenne (2 * 1 + 1) % 3 = 1

Tactic:
| base =>

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case base
n : ℕ
⊢ mersenne 3 % 8 = 7

Tactic:
| base =>

Goal state after:
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₁ : ∀ {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‖
this : Tendsto (fun s ↦ (↑s - 1) * LSeries f ↑s - ↑s * l) (𝓝[>] 1) (𝓝 0)
⊢ Tendsto (fun s ↦ (↑s - 1) * LSeries f ↑s) (𝓝[>] 1) (𝓝 l)

Tactic:
rw [show 𝓝 l = 𝓝 (0 + 1 * l) by congr; ring]
    have h₃ : Tendsto (fun s : ℝ ↦ s * l) (𝓝[>] 1) (𝓝 (1 * l)) :=
      tendsto_nhdsWithin_of_tendsto_nhds (ContinuousAt.tendsto (by fun_prop))
    exact (this.add h₃).congr fun _ ↦ by ring

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hpdeg : p.degree ≠ 0
hpdegC : (map (castRingHom ℂ) p).degree ≠ 0
z : ℂ
h✝ : eval z (map (castRingHom ℂ) p) = 0
hX : z = 0
⊢ X ∣ p

Tactic:
simp_all [X_dvd_iff, coeff_zero_eq_aeval_zero]

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
this : (ZMod.castHom ⋯ (X q)) 2 * ω ^ ((q + 1) / 2) = -(ZMod.castHom ⋯ (X q)) 2
coe : 2 = (ZMod.castHom ⋯ (X q)) 2
⊢ ω ^ ((q + 1) / 2) = -1

Tactic:
← coe,

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
coe : 2 = (ZMod.castHom ⋯ (X q)) 2
⊢ ω ^ ((q + 1) / 2) = -1
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: case inr.mp
G✝ : Type u_1
inst✝⁶ : CommGroup G✝
inst✝⁵ : TopologicalSpace G✝
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
g : G
ha✝ : 1 ≤ g
ha : 1 < g
n : ℤ
⊢ ⟨(fun x ↦ g ^ x) n, ⋯⟩ ∈ Subtype.val ⁻¹' Set.Ioo (g ^ (-1)) (g ^ 1) → ⟨(fun x ↦ g ^ x) n, ⋯⟩ ∈ {1}

Tactic:
simp only [Set.mem_preimage, Set.mem_Ioo, Set.mem_singleton_iff, and_imp]
    intro hn hn'
    rw [zpow_lt_zpow_iff_right ha] at hn hn'
    simp only [Subtype.ext_iff, show n = 0 by lia, zpow_zero, coe_one]

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

Goal state before:
pp: N : ℕ
⊢ Gamma1 N ≤ Gamma0 N

Tactic:
intro x HA

Goal state after:
N : ℕ
x : SL(2, ℤ)
HA : x ∈ Gamma1 N
⊢ x ∈ Gamma0 N
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: β : Type u_1
G : Type u_2
α : Type u_3
inst✝² : Group G
inst✝¹ : AddGroup α
inst✝ : SlashAction β G α
k : β
g : G
a : α
⊢ a ∣[k] g = 0 ↔ a = 0

Tactic:
refine ⟨fun h ↦ ?_, by simp +contextual⟩
  apply_fun (· ∣[k] g⁻¹) at h
  simpa [← SlashAction.slash_mul] using h

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

Goal state before:
pp: g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
N : ℕ
hN : N ≠ 0
h : ∀ x ∈ Γ(N), g * (mapGL ℚ) x * g⁻¹ ∈ Subgroup.map (mapGL ℚ) Γ(M)
y : GL (Fin 2) ℝ
hy : y ∈ toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) Γ(N)
⊢ y ∈ Subgroup.map (mapGL ℝ) Γ(M)

Tactic:
Subgroup.mem_pointwise_smul_iff_inv_smul_mem,

Goal state after:
g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
N : ℕ
hN : N ≠ 0
h : ∀ x ∈ Γ(N), g * (mapGL ℚ) x * g⁻¹ ∈ Subgroup.map (mapGL ℚ) Γ(M)
y : GL (Fin 2) ℝ
hy : (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹ • y ∈ Subgroup.map (mapGL ℝ) Γ(N)
⊢ y ∈ Subgroup.map (mapGL ℝ) Γ(M)
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
hc : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
x : GL (Fin 2) ℝ
⊢ x ∈ 𝒢 ↔ x ∈ ConjAct.toConjAct g • 𝒢

Tactic:
Subgroup.mem_pointwise_smul_iff_inv_smul_mem,

Goal state after:
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
hc : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
x : GL (Fin 2) ℝ
⊢ x ∈ 𝒢 ↔ (ConjAct.toConjAct g)⁻¹ • x ∈ 𝒢
Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝¹ : FunLike F ℍ ℂ
inst✝ : SlashInvariantFormClass F Γ k
f : F
g j : GL (Fin 2) ℝ
hj : j ∈ toConjAct g⁻¹ • Γ
⊢ (⇑f ∣[k] g) ∣[k] j = ⇑f ∣[k] g

Tactic:
by
    rw [map_inv, Γ.mem_inv_pointwise_smul_iff, toConjAct_smul] at hj
    simpa [← SlashAction.slash_mul] using congr_arg (· ∣[k] g) (slash_action_eqn f _ hj)

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
z : ℍ
hf : f (-1 • z) = denom (-1) ↑z ^ k * f z
⊢ f z = 0 z

Tactic:
neg_smul,

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
z : ℍ
hf : f (1 • z) = denom (-1) ↑z ^ k * f z
⊢ f z = 0 z
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
⊢ ⟨n • k, GradedMonoid.GMonoid.gnpow n f⟩ = ⟨↑n * k, f.pow n⟩

Tactic:
induction n with
  | zero =>
    refine (GradedMonoid.GMonoid.gnpow_zero' ⟨k, f⟩).trans ?_
    exact gradedMonoid_eq_of_cast (zero_mul k).symm (ModularForm.ext fun _ ↦ rfl)
  | succ n ih =>
    refine (GradedMonoid.GMonoid.gnpow_succ' n ⟨k, f⟩).trans ?_
    refine (congrArg (fun x : GradedMonoid (ModularForm Γ) ↦ x * ⟨k, f⟩) ih).trans ?_
    exact gradedMonoid_eq_of_cast (show ((n : ℤ) * k + k = (n + 1) * k) by ring)
      (ModularForm.ext fun _ ↦ rfl)

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

Goal state before:
pp: case hasSum
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
y : ℂ
hy : ‖y‖ < 1
⊢ HasSum (fun n ↦ (FormalMultilinearSeries.ofScalars ℂ c n) fun x ↦ y) (update (cuspFunction h f) 0 (c 0) (0 + y))

Tactic:
rcases eq_or_ne y 0 with rfl | hy'

Goal state after:
case hasSum.inl
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
hy : ‖0‖ < 1
⊢ HasSum (fun n ↦ (FormalMultilinearSeries.ofScalars ℂ c n) fun x ↦ 0) (update (cuspFunction h f) 0 (c 0) (0 + 0))

case hasSum.inr
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
y : ℂ
hy : ‖y‖ < 1
hy' : y ≠ 0
⊢ HasSum (fun n ↦ (FormalMultilinearSeries.ofScalars ℂ c n) fun x ↦ y) (update (cuspFunction h f) 0 (c 0) (0 + y))
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
this : Nonempty { g // ↑g 1 = cd }
g : { g // ↑g 1 = cd }
hg : ∀ (a : { g // ↑g 1 = cd }), |(↑g • z).re| ≤ |(↑a • z).re|
g1 : SL(2, ℤ)
⊢ ↑↑g 1 = ↑g1 1 → |(↑g • z).re| ≤ |(g1 • z).re|

Tactic:
hg1

Goal state after:
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
this : Nonempty { g // ↑g 1 = cd }
g : { g // ↑g 1 = cd }
hg : ∀ (a : { g // ↑g 1 = cd }), |(↑g • z).re| ≤ |(↑a • z).re|
g1 : SL(2, ℤ)
hg1 : ↑↑g 1 = ↑g1 1
⊢ |(↑g • z).re| ≤ |(g1 • z).re|
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
h : ℝ
f : F
inst✝ : CuspFormClass F Γ k
hh : 0 < h
hΓ : h ∈ Γ.strictPeriods
⊢ (PowerSeries.coeff 0) (qExpansion h ⇑f) = 0

Tactic:
simp [qExpansion_coeff, cuspFunction_apply_zero f hh hΓ]

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

Goal state before:
pp: 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✝ : CuspFormClass F' Γ k
⊢ ∃ C, ∀ (τ : ℍ), ‖petersson k (⇑f) (⇑f') τ‖ ≤ C

Tactic:
by
  simpa [petersson_norm_symm] using petersson_bounded_left k Γ f' f

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

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
γ : SL(2, ℤ)
⊢ D (F ∣[k] γ) =
    D F ∣[k + 2] γ - fun z ↦
      ↑k * (2 * ↑π * I)⁻¹ *
          (↑(↑γ 1 0) /
            denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z) *
        (F ∣[k] γ) z

Tactic:
have hdet : (γ : GL (Fin 2) ℝ).val.det = 1 := by
    rw [← Matrix.GeneralLinearGroup.val_det_apply]; simp

Goal state after:
k : ℤ
F : ℍ → ℂ
hF : MDiff F
γ : SL(2, ℤ)
hdet : (↑(Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ))).det = 1
⊢ D (F ∣[k] γ) =
    D F ∣[k + 2] γ - fun z ↦
      ↑k * (2 * ↑π * I)⁻¹ *
          (↑(↑γ 1 0) /
            denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z) *
        (F ∣[k] γ) z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k m : ℕ
p : ℝ
S : Set ℂ
hs : IsOpen S
x : ℂ
hx : x ∈ S
⊢ iteratedDeriv k (fun s ↦ cexp (2 * ↑π * I * ↑m * s / ↑p)) x =
    (fun s ↦ (2 * ↑π * I * ↑m / ↑p) ^ k * cexp (2 * ↑π * I * ↑m * s / ↑p)) x

Tactic:
have : (fun s ↦ cexp (2 * π * I * m * s / p)) = fun s ↦ cexp (((2 * π * I * m) / p) * s) := by
    ext z
    ring_nf

Goal state after:
k m : ℕ
p : ℝ
S : Set ℂ
hs : IsOpen S
x : ℂ
hx : x ∈ S
this : (fun s ↦ cexp (2 * ↑π * I * ↑m * s / ↑p)) = fun s ↦ cexp (2 * ↑π * I * ↑m / ↑p * s)
⊢ iteratedDeriv k (fun s ↦ cexp (2 * ↑π * I * ↑m * s / ↑p)) x =
    (fun s ↦ (2 * ↑π * I * ↑m / ↑p) ^ k * cexp (2 * ↑π * I * ↑m * s / ↑p)) x
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case mp
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
⊢ g ∈ {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)}

Tactic:
have neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹ := by
      have : T • ρ ≠ ρ := by
        rw [ne_eq, UpperHalfPlane.ext_iff, modular_T_smul, coe_vadd]
        norm_num
      have : T⁻¹ • ρ ≠ ρ := by rwa [ne_eq, inv_smul_eq_iff, eq_comm]
      grind [SL_neg_smul]

Goal state after:
case mp
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹
⊢ g ∈ {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)}
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: case hf
z : ℍ
this :
  ∀ (N : ℕ+),
    ∑ n ∈ Ico (-↑↑N) ↑↑N, ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1)) =
      -(2 / ↑↑N) +
        ∑' (m : ℕ+), (1 / (↑↑m * ↑z - ↑↑N) + 1 / (-↑↑m * ↑z + -↑↑N) - 1 / (↑↑m * ↑z + ↑↑N) - 1 / (-↑↑m * ↑z + ↑↑N))
⊢ Tendsto (fun x ↦ -(2 / ↑↑x)) atTop (𝓝 0)

Tactic:
simpa [← PNat.tendsto_comp_val_iff] using!
      (tendsto_inv_atTop_nhds_zero_nat (𝕜 := ℂ)).const_mul (-2)

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ (fun τ ↦ ‖↑τ‖) '' 𝒟 ⊆ Set.Ici 1

Tactic:
rw [Set.image_subset_iff]

Goal state after:
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' Set.Ici 1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ UpperHalfPlane.re '' 𝒟 ⊆ Set.Icc (-(1 / 2)) (1 / 2)

Tactic:
rw [Set.image_subset_iff]

Goal state after:
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ 𝒟 ⊆ UpperHalfPlane.re ⁻¹' Set.Icc (-(1 / 2)) (1 / 2)
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
k : ℤ
hk : k < 0
f : ModularForm 𝒢 k
⊢ f = 0

Tactic:
suffices ModularForm.norm 𝒮ℒ f = 0 by simpa [ModularForm.norm_eq_zero_iff]

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
k : ℤ
hk : k < 0
f : ModularForm 𝒢 k
⊢ ModularForm.norm (Matrix.SpecialLinearGroup.mapGL ℝ).range f = 0