mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs

Goal state before:
pp: A B : SL(2, ℤ)
z : ℍ
h0 :
  (↑A * ↑B) 0 0 = ↑A 0 0 * ↑B 0 0 + ↑A 0 1 * ↑B 1 0 ∧
    (↑A * ↑B) 0 1 = ↑A 0 0 * ↑B 0 1 + ↑A 0 1 * ↑B 1 1 ∧
      (↑A * ↑B) 1 0 = ↑A 1 0 * ↑B 0 0 + ↑A 1 1 * ↑B 1 0 ∧ (↑A * ↑B) 1 1 = ↑A 1 0 * ↑B 0 1 + ↑A 1 1 * ↑B 1 1
⊢ (↑(↑A 1 0) * ↑(↑B 0 0) + ↑(↑A 1 1) * ↑(↑B 1 0)) * (↑(↑B 1 0) * ↑z + ↑(↑B 1 1)) =
    ↑(↑A 1 0) * (↑(↑B 0 0) * ↑(↑B 1 1) - ↑(↑B 0 1) * ↑(↑B 1 0)) +
      ↑(↑B 1 0) *
        ((↑(↑A 1 0) * ↑(↑B 0 0) + ↑(↑A 1 1) * ↑(↑B 1 0)) * ↑z + (↑(↑A 1 0) * ↑(↑B 0 1) + ↑(↑A 1 1) * ↑(↑B 1 1)))

Tactic:
ring

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

Goal state before:
pp: A B : SL(2, ℤ)
z : ℍ
hd : ↑((↑A * ↑B) 1 0) * denom (toGL (φ B)) ↑z - ↑(↑B 1 0) * denom (toGL (φ A) * toGL (φ B)) ↑z = ↑(↑A 1 0)
this : denom (toGL (φ A)) (num (toGL (φ B)) ↑z / denom (toGL (φ B)) ↑z) = denom (toGL (φ A)) ↑(B • z)
⊢ ↑((↑A * ↑B) 1 0) =
    ↑((↑A * ↑B) 1 0) - denom (toGL (φ A)) ↑(toGL (φ B) • z) * ↑(↑B 1 0) +
      denom (toGL (φ A)) ↑(toGL (φ B) • z) * ↑(↑B 1 0)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq (↑z + 1) ≤ 1
⊢ (z.re + 1) * (z.re + 1) + z.im * z.im = z.re * z.re + z.im * z.im + (2 * z.re + 1)

Tactic:
ring

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

Goal state before:
pp: r : ℂ
g : ℂ → ℂ
hg : Differentiable ℂ g
y : ℂ
⊢ (fun z ↦ -r * cexp z / (1 - r * cexp z)) (g y) * deriv g y = -r * deriv g y * cexp (g y) / (1 - r * cexp (g y))

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case pos
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : b = 0
hn : n = -1
⊢ 2 + -1 = 1

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ t = t + 0

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this : ↑g 0 1 = -↑g 0 0 - 1
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq (↑z - 1) ≤ 1
⊢ (z.re - 1) * (z.re - 1) + z.im * z.im = z.re * z.re + z.im * z.im + (-(2 * z.re) + 1)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
N M : ℤ
⊢ (↑M * ↑z + ↑N + 1)⁻¹ * ((↑M * ↑z + ↑N) ^ 2)⁻¹ + δ ![M, N] + ((↑M * ↑z + ↑N)⁻¹ - (↑M * ↑z + ↑N + 1)⁻¹) -
      ((↑M * ↑z + ↑N)⁻¹ - (↑M * ↑z + ↑N + 1)⁻¹) =
    (↑M * ↑z + ↑N + 1)⁻¹ * ((↑M * ↑z + ↑N) ^ 2)⁻¹ + δ ![M, N]

Tactic:
ring

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

Goal state before:
pp: c : ℂ
F : ℍ → ℂ
hF : MDiff F
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
⊢ (2 * ↑π * I)⁻¹ * (c * deriv (F ∘ ↑ofComplex) ↑z) = c * ((2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑z)

Tactic:
ring

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

Goal state before:
pp: F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
hGz : DifferentiableAt ℂ (G ∘ ↑ofComplex) ↑z
⊢ -(I * ((↑π)⁻¹ * 2⁻¹) * (deriv (F ∘ ↑ofComplex) ↑z * G z + F z * deriv (G ∘ ↑ofComplex) ↑z)) =
    -(I * ((↑π)⁻¹ * 2⁻¹) * deriv (F ∘ ↑ofComplex) ↑z * G z) + -(F z * (I * ((↑π)⁻¹ * 2⁻¹) * deriv (G ∘ ↑ofComplex) ↑z))

Tactic:
ring

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

Goal state before:
pp: F : ℍ → ℂ
n : ℕ
hF : MDiff F
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
⊢ I * ((↑π)⁻¹ * 2⁻¹) * (↑n * F z ^ (n - 1) * deriv (F ∘ ↑ofComplex) ↑z) =
    ↑n * F z ^ (n - 1) * (I * ((↑π)⁻¹ * 2⁻¹) * deriv (F ∘ ↑ofComplex) ↑z)

Tactic:
ring

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

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
hdet : ↑(Matrix.GeneralLinearGroup.det g) = (↑g).det
hdetℂ : ↑(↑g).det ≠ 0
hσ : ∀ (x : ℂ), (σ g) x = x
z : ℍ
hz : denom g ↑z ≠ 0
h_smul : HasDerivAt (fun w ↦ ↑(g • ↑ofComplex w)) (↑(↑g).det / denom g ↑z ^ 2) ↑z
h_F : HasDerivAt (F ∘ ↑ofComplex) (deriv (F ∘ ↑ofComplex) ↑(g • ↑ofComplex ↑z)) ↑(g • ↑ofComplex ↑z)
h_denom : HasDerivAt (fun w ↦ denom g w ^ (-k)) (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)) ↑z
hcomp :
  F ∣[k] g ∘ ↑ofComplex =ᶠ[𝓝 ↑z] fun w ↦ ↑(↑g).det ^ (k - 1) * ((F ∘ ↑ofComplex) ↑(g • ↑ofComplex w) * denom g w ^ (-k))
⊢ k + 2 - 1 = k - 1 + 2

Tactic:
ring

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

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
hdet : ↑(Matrix.GeneralLinearGroup.det g) = (↑g).det
hdetℂ : ↑(↑g).det ≠ 0
hσ : ∀ (x : ℂ), (σ g) x = x
z : ℍ
hz : denom g ↑z ≠ 0
h_smul : HasDerivAt (fun w ↦ ↑(g • ↑ofComplex w)) (↑(↑g).det / denom g ↑z ^ 2) ↑z
h_F : HasDerivAt (F ∘ ↑ofComplex) (deriv (F ∘ ↑ofComplex) ↑(g • ↑ofComplex ↑z)) ↑(g • ↑ofComplex ↑z)
h_denom : HasDerivAt (fun w ↦ denom g w ^ (-k)) (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)) ↑z
hcomp :
  F ∣[k] g ∘ ↑ofComplex =ᶠ[𝓝 ↑z] fun w ↦ ↑(↑g).det ^ (k - 1) * ((F ∘ ↑ofComplex) ↑(g • ↑ofComplex w) * denom g w ^ (-k))
⊢ -(k + 2) = -k + -2

Tactic:
ring

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

Goal state before:
pp: z : ℂ
hz : z ≠ 0
⊢ log z * 12 = ↑12 * log z

Tactic:
ring

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

Goal state before:
pp: case e_a
z : ℍ
⊢ (∏' (n : ℕ), (1 - eta_q n ↑z)) ^ 24 = ∏' (n : ℕ), (1 - eta_q n ↑z) ^ 24

Tactic:
exact ((multipliableLocallyUniformlyOn_eta.multipliable z.2).tprod_pow _).symm

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

Goal state before:
pp: k l : ℕ
p : ℝ
f : ℕ → ℂ
hf : f =O[atTop] fun n ↦ ↑n ^ l
z : ℕ
⊢ (2 * ↑π * I * ↑z / ↑p) ^ k = (2 * ↑π * I / ↑p) ^ k * ↑z ^ k

Tactic:
ring

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

Goal state before:
pp: case e'_8
k l : ℕ
p : ℝ
f : ℕ → ℂ
hf : f =O[atTop] fun n ↦ ↑n ^ l
h0 : (fun n ↦ (2 * ↑π * I * ↑n / ↑p) ^ k) =O[atTop] fun n ↦ ↑n ^ k
x✝ : ℕ
⊢ ↑x✝ ^ (l + k) = ↑x✝ ^ l * ↑x✝ ^ k

Tactic:
ring

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

Goal state before:
pp: ⊢ 0 = 0 * 1

Tactic:
ring

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

Goal state before:
pp: k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (k - 12)
⊢ 12 + (k - 12) = k

Tactic:
ring

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

Goal state before:
pp: case e_f
k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  iteratedDerivWithin k (fun z ↦ ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z =
    -(2 * ↑π * I) * ∑' (n : ℕ), iteratedDerivWithin k (fun s ↦ cexp (2 * ↑π * I * s) ^ n) ℍₒ ↑z
y : ℕ
⊢ -(2 * ↑π * I * (2 * ↑π * I) ^ k) * (↑y ^ k * cexp (2 * ↑π * I * ↑z) ^ y) =
    -(2 * ↑π * I) * ((2 * ↑π * I * ↑y) ^ k * cexp (2 * ↑π * I * ↑z) ^ y)

Tactic:
ring

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

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
this :
  (-1) ^ k * ↑k ! * ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) =
    -(2 * ↑π * I) ^ (k + 1) * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n
n : ℕ
⊢ (-2 * ↑π * I) ^ (k + 1) = (-(2 * ↑π * I)) ^ (k + 1)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ 1 / (↑m * ↑z + ↑a) - 1 / (↑m * ↑z + ↑b) = (↑b - ↑a) * (1 / ((↑m * ↑z + ↑a) * (↑m * ↑z + ↑b)))

Tactic:
rw [← one_div_mul_sub_mul_one_div_eq_one_div_add_one_div]

Goal state after:
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ 1 / (↑m * ↑z + ↑a) * (↑m * ↑z + ↑b - (↑m * ↑z + ↑a)) * (1 / (↑m * ↑z + ↑b)) =
    (↑b - ↑a) * (1 / ((↑m * ↑z + ↑a) * (↑m * ↑z + ↑b)))

case ha
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ ↑m * ↑z + ↑a ≠ 0

case hb
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ ↑m * ↑z + ↑b ≠ 0
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case h.inr.inl
k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
hk : 3 ≤ k ∧ k < 12
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1)

Tactic:
rw [rank_eq_one_add_rank_cuspForm hk.1 hk2, CuspForm.discriminantEquiv.rank_eq,
      levelOne_neg_weight_rank_zero (by lia)]

Goal state after:
case h.inr.inl
k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
hk : 3 ≤ k ∧ k < 12
⊢ 1 + 0 = ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
⊢ T • ρ ≠ ρ

Tactic:
rw [ne_eq, UpperHalfPlane.ext_iff, modular_T_smul, coe_vadd]

Goal state after:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
⊢ ¬↑1 + ↑ρ = ↑ρ
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: case hf
z : ℍ
d : ℕ+
this : Summable fun n ↦ (-↑↑d / ↑z - ↑(n + 1))⁻¹ + (-↑↑d / ↑z + ↑(n + 1))⁻¹
⊢ Summable fun m ↦ (-↑↑d / ↑z - ↑↑m)⁻¹ + (-↑↑d / ↑z + ↑↑m)⁻¹

Tactic:
rw [summable_nat_add_iff (f := fun n ↦ (-d / (z : ℂ) - n)⁻¹ + (-d / (z : ℂ) + n)⁻¹)] at this

Goal state after:
case hf
z : ℍ
d : ℕ+
this : Summable fun n ↦ (-↑↑d / ↑z - ↑n)⁻¹ + (-↑↑d / ↑z + ↑n)⁻¹
⊢ Summable fun m ↦ (-↑↑d / ↑z - ↑↑m)⁻¹ + (-↑↑d / ↑z + ↑↑m)⁻¹
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
⊢ ‖cexp (↑π * I * ↑n ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ n.natAbs

Tactic:
have h : y < 1 := exp_lt_one_iff.mpr (mul_neg_of_neg_of_pos (neg_lt_zero.mpr pi_pos) hτ)

Goal state after:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ ‖cexp (↑π * I * ↑n ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ n.natAbs
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ ↑π * I * ↑n ^ 2 * τ = ↑π * ↑n ^ 2 * (τ * I)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ π * ↑n ^ 2 * -τ.im = -π * τ.im * ↑n ^ 2

Tactic:
ring

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ ∑' (b : ℕ) (c : ↑(gammaSet 1 b 0)), eisSummand (↑k) (↑⟨b, c⟩.snd) z =
    riemannZeta ↑k * ∑' (x : ↑(gammaSet 1 1 0)), eisSummand (↑k) (↑x) z

pp: case hsumm
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ Summable fun c ↦ eisSummand (↑k) (↑c.snd) z

Tactic:
zeta_nat_eq_tsum_of_gt_one hk1,

Goal state after:
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ ∑' (b : ℕ) (c : ↑(gammaSet 1 b 0)), eisSummand (↑k) (↑⟨b, c⟩.snd) z =
    (∑' (n : ℕ), 1 / ↑n ^ k) * ∑' (x : ↑(gammaSet 1 1 0)), eisSummand (↑k) (↑x) z

case hsumm
k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
⊢ Summable fun c ↦ eisSummand (↑k) (↑c.snd) z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
H0 :
  (fun n ↦ 2 / ↑z * ∑' (m : ℕ+), (1 / (-↑↑n / ↑z - ↑↑m) + 1 / (-↑↑n / ↑z + ↑↑m))) = fun n ↦
    -2 * ↑π * I / ↑z - 2 / ↑z * (2 * ↑π * I) * ∑' (m : ℕ+), cexp (2 * ↑π * I * (-↑↑n / ↑z)) ^ ↑m + 2 / ↑↑n
⊢ -2 * ↑π * I / ↑z = -2 * ↑π * I / ↑z - 2 / ↑z * (2 * ↑π * I) * 0 + 2 * 0

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: 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))
⊢ -2 * ↑π * I / ↑z = 0 + -2 * ↑π * I / ↑z

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
ha : 0 < a
this : 1 < ‖↑x‖ ^ 2 + ↑a ^ 2 + 2 * ↑a * x.im
⊢ x.re * x.re + (x.im + ↑a) * (x.im + ↑a) = x.re * x.re + x.im * x.im + ↑a ^ 2 + 2 * ↑a * x.im

Tactic:
ring

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(2 * ↑k / ↑(bernoulli k))
c : ℕ → ℂ := fun m ↦ if m = 0 then 1 else β * ↑((σ (k - 1)) m)
τ : ℍ
hS : Summable fun n ↦ ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
this : (E hk) τ = 1 - 2 * ↑k / ↑(bernoulli k) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑τ) ^ ↑n
⊢ 1 - 2 * ↑k / ↑(bernoulli k) * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑τ) ^ ↑n - 1 =
    β * ∑' (n : ℕ+), ↑((σ (k - 1)) ↑n) * cexp (2 * ↑π * I * ↑τ) ^ ↑n

Tactic:
ring

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

Goal state before:
pp: ⊢ qExpansion 1 ⇑E₄ ^ 3 - qExpansion 1 ⇑E₆ ^ 2 =
    qExpansion 1 ⇑E₄ * qExpansion 1 ⇑E₄ * qExpansion 1 ⇑E₄ - qExpansion 1 ⇑E₆ * qExpansion 1 ⇑E₆

Tactic:
ring

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

Goal state before:
pp: Γ : 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 : ↑k + 1 < s.re
⊢ (weakFEPair hk f).k < s.re

Tactic:
by grind [weakFEPair]

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 : ℂ
this : (2 * ↑n / ↑(h Γ)) ^ s = 2 ^ s * ↑n ^ s / ↑(h Γ) ^ s
⊢ p / ↑n ^ s = (↑π ^ s)⁻¹ * Gamma s * p / (2 ^ s * ↑n ^ s / ↑(h Γ) ^ s) * (2 ^ s * ↑π ^ s / Gamma s * (↑(h Γ) ^ s)⁻¹)

Tactic:
have := Gamma_ne_zero_of_re_pos hs

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 : ℂ
this✝ : (2 * ↑n / ↑(h Γ)) ^ s = 2 ^ s * ↑n ^ s / ↑(h Γ) ^ s
this : Gamma s ≠ 0
⊢ p / ↑n ^ s = (↑π ^ s)⁻¹ * Gamma s * p / (2 ^ s * ↑n ^ s / ↑(h Γ) ^ s) * (2 ^ s * ↑π ^ s / Gamma s * (↑(h Γ) ^ s)⁻¹)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
x y : R
d : ℕ
hd : x ^ 2 ^ d - y ^ 2 ^ d = (∏ i ∈ range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
⊢ x ^ 2 ^ (d + 1) - y ^ 2 ^ (d + 1) = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: m : ℤ
⊢ (2 * m + 1) ^ 2 - 1 = 4 * (m * (m + 1))

Tactic:
ring

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
S : Set ι
hS : cofinite ≤ 𝓟 S
p : ι → Prop
⊢ IsOpen[topologicalSpace R A (𝓟 S)] {f | ∀ (i : ι), p i → ↑f i ∈ A i}

Tactic:
rw [le_principal_iff] at hS
  convert!
    isOpen_set_pi (hS.inter_of_left {i | p i}) (fun i _ ↦ hAopen i) |>.preimage continuous_coe
  ext f
  refine ⟨fun H i hi ↦ H i hi.2, fun H i hiT ↦ ?_⟩
  by_cases hiS : i ∈ S
  · exact f.2 hiS
  · exact H i ⟨hiS, hiT⟩

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ (1 - y ^ 2 % 4) % 4 = 0

pp: x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ Odd x

Tactic:
Int.sq_mod_four_eq_one_of_odd hy

Goal state after:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ (1 - 1) % 4 = 0

x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ Odd x
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁵ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst✝⁴ : (i : ι) → TopologicalSpace (R i)
hBopen : Fact (∀ (i : ι), IsOpen[inst✝⁴ i] ↑(B i))
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : (i : ι) → SMul G (R i)
inst✝¹ : ∀ (i : ι), SMulMemClass (S i) G (R i)
inst✝ : ∀ (i : ι), ContinuousSMul G (R i)
⊢ Continuous[instTopologicalSpaceProd, topologicalSpace R (fun i ↦ ↑(B i)) cofinite] fun p ↦ p.1 • p.2

Tactic:
by
    rw [continuous_dom_prod_left hBopen.out]
    exact fun S hS ↦ (continuous_inclusion hS).comp continuous_smul

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h : x = 0
⊢ u • 0 = 0

Tactic:
smul_zero

Goal state after:
K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h : x = 0
⊢ 0 = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Measurable ↑(mixedEmbedding.polarCoord K).symm

Tactic:
rw [polarCoord_symm_eq]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Measurable (⇑(mixedSpaceToRealMixedSpace K).symm ∘ ↑(polarCoordReal K).symm)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
hy : mixedEmbedding.norm y ≠ 0
w : { w // w ≠ w₀ }
⊢ ↑(↑w).mult *
      (Real.log ((normAtPlace ↑w) x) + Real.log ((normAtPlace ↑w) y) -
        (Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹ +
          Real.log (mixedEmbedding.norm y) * (↑(finrank ℚ K))⁻¹)) =
    ↑(↑w).mult * (Real.log ((normAtPlace ↑w) x) - Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹) +
      ↑(↑w).mult * (Real.log ((normAtPlace ↑w) y) - Real.log (mixedEmbedding.norm y) * (↑(finrank ℚ K))⁻¹)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : ¬LinearIndependent ℝ fun i ↦ (logEmbedding K) (Additive.ofMul (u i))
⊢ ¬LinearIndependent ℝ fun i ↦ of (fun i ↦ (logEmbedding K) (Additive.ofMul (u ((equivFinRank K).symm i)))) i

Tactic:
← linearIndependent_equiv (equivFinRank K).symm

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : ¬LinearIndependent ℝ ((fun i ↦ (logEmbedding K) (Additive.ofMul (u i))) ∘ ⇑(equivFinRank K).symm)
⊢ ¬LinearIndependent ℝ fun i ↦ of (fun i ↦ (logEmbedding K) (Additive.ofMul (u ((equivFinRank K).symm i)))) i
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: case refine_2
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : 𝓞 K
x✝ : ∃ y, (algebraMap (𝓞 ↥K⁺) K) y = ↑x
y : 𝓞 ↥K⁺
hy : (algebraMap (𝓞 ↥K⁺) K) y = ↑x
⊢ ↑x ∈ K⁺

Tactic:
rw [← hy, IsScalarTower.algebraMap_apply (𝓞 K⁺) K⁺]
    exact SetLike.coe_mem _

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
x✝ y✝ : (𝓞 K)ˣ
⊢ (algebraMap (𝓞 K) K) ↑x✝ * (algebraMap (𝓞 K) K) ↑y✝ *
      (((algebraMap (𝓞 K) K) ↑((unitsComplexConj K) y✝))⁻¹ * ((algebraMap (𝓞 K) K) ↑((unitsComplexConj K) x✝))⁻¹) =
    (algebraMap (𝓞 K) K) ↑x✝ * ((algebraMap (𝓞 K) K) ↑((unitsComplexConj K) x✝))⁻¹ *
      ((algebraMap (𝓞 K) K) ↑y✝ * ((algebraMap (𝓞 K) K) ↑((unitsComplexConj K) y✝))⁻¹)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ (powMonoidHom 2).range.index = 2

Tactic:
rw [IsCyclic.index_powMonoidHom_range, Nat.gcd_eq_right_iff_dvd]

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ 2 ∣ Nat.card ↥(torsion K)
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
this : (∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤) ↔ (unitsMulComplexConjInv K).range.index = 1
⊢ indexRealUnits K = 2 ↔ (unitsMulComplexConjInv K).range.index = 1

Tactic:
have h_eq := indexRealUnits_mul_eq K

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
this : (∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤) ↔ (unitsMulComplexConjInv K).range.index = 1
h_eq : indexRealUnits K * (unitsMulComplexConjInv K).range.index = 2
⊢ indexRealUnits K = 2 ↔ (unitsMulComplexConjInv K).range.index = 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
J : ↥(Ideal (𝓞 K))⁰
⊢ (x ∈ fundamentalCone K ∧ ∃ y, (mixedEmbedding K) ↑y = x) ↔ x ∈ fundamentalCone K ∧ ∃ a ∈ ↑J, (mixedEmbedding K) ↑a = x

Tactic:
Subtype.exists,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
J : ↥(Ideal (𝓞 K))⁰
⊢ (x ∈ fundamentalCone K ∧ ∃ a, ∃ (_ : a ∈ ↑↑↑J), (mixedEmbedding K) a = x) ↔
    x ∈ fundamentalCone K ∧ ∃ a ∈ ↑J, (mixedEmbedding K) ↑a = x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝² x✝¹ : realSpace K
x✝ : { w // w ≠ w₀ }
⊢ x✝² ↑x✝ + x✝¹ ↑x✝ - ↑(↑x✝).mult * (∑ x, x✝² x + ∑ x, x✝¹ x) * (↑(finrank ℚ K))⁻¹ =
    x✝² ↑x✝ - (↑(↑x✝).mult * ∑ x, x✝² x) * (↑(finrank ℚ K))⁻¹ +
      (x✝¹ ↑x✝ - (↑(↑x✝).mult * ∑ x, x✝¹ x) * (↑(finrank ℚ K))⁻¹)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝² : ℝ
x✝¹ : realSpace K
x✝ : { w // w ≠ w₀ }
⊢ x✝² * x✝¹ ↑x✝ - ↑(↑x✝).mult * (x✝² * ∑ i, x✝¹ i) * (↑(finrank ℚ K))⁻¹ =
    x✝² * (x✝¹ ↑x✝ - (↑(↑x✝).mult * ∑ i, x✝¹ i) * (↑(finrank ℚ K))⁻¹)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ZLattice.covolume (unitLattice K) volume = ZLattice.covolume (span ℤ (Set.range ⇑(basisOfIsMaxRank ⋯))) volume

Tactic:
← (basisUnitLattice K).ofZLatticeBasis_span ℝ,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ZLattice.covolume (span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)))) volume =
    ZLattice.covolume (span ℤ (Set.range ⇑(basisOfIsMaxRank ⋯))) volume
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ mixedEmbedding.norm
      (mixedSpaceOfRealSpace (↑expMap ((completeBasis K).equivFun.symm fun i ↦ if i = w₀ then 0 else x i))) =
    1

Tactic:
by rw [← expMapBasis_apply,
    norm_expMapBasis, if_pos rfl, Real.exp_zero, one_pow]

Goal state after: