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

Goal state before:
pp: k : ℤ
F : Type u_1
inst✝⁴ : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
f : F
inst✝³ : ModularFormClass F Γ k
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : DiscreteTopology ↥Γ
inst✝ : Fact (IsCusp OnePoint.infty Γ)
hh : 0 < Γ.strictWidthInfty
hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods
τ : ℍ
⊢ -(2 * π / Γ.strictWidthInfty) * τ.im = -2 * π * τ.im / Γ.strictWidthInfty

Tactic:
ring_nf

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • S • z ∈ 𝒟
hg'✝ : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
hg' : g = T ^ ↑g 0 0 * S
hSre : (S • z).re = -z.re
this✝ : |↑(↑g 0 0) + -z.re| ≤ 1 / 2
this : |↑(↑g 0 0)| - |(-z.re)| ≤ 1 / 2
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ

Tactic:
rw [abs_neg, sub_le_iff_le_add] at this

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • S • z ∈ 𝒟
hg'✝ : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
hg' : g = T ^ ↑g 0 0 * S
hSre : (S • z).re = -z.re
this✝ : |↑(↑g 0 0) + -z.re| ≤ 1 / 2
this : |↑(↑g 0 0)| ≤ 1 / 2 + |z.re|
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ
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
⊢ ↑g =
    !![(1 * 0 + ↑g 0 0 * 1) * 1 + (1 * -1 + ↑g 0 0 * 0) * 0, (1 * 0 + ↑g 0 0 * 1) * 1 + (1 * -1 + ↑g 0 0 * 0) * 1;
      (0 * 0 + 1 * 1) * 1 + (0 * -1 + 1 * 0) * 0, (0 * 0 + 1 * 1) * 1 + (0 * -1 + 1 * 0) * 1]

Tactic:
ring_nf

Goal state after:
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
⊢ ↑g = !![↑g 0 0, -1 + ↑g 0 0; 1, 1]
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: n : ℕ
z : ℂ
⊢ cexp ((↑n + 1) * (2 * ↑π * I * z)) = cexp (2 * ↑π * I * (↑n + 1) * z)

Tactic:
ring_nf

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

Goal state before:
pp: z : ℂ
hz : z ∈ ℍₒ
this :
  Summable fun n ↦ ↑n ^ 1 * 𝕢 ↑1 ↑{ coe := z, coe_im_pos := hz } ^ n / (1 - 𝕢 ↑1 ↑{ coe := z, coe_im_pos := hz } ^ n)
⊢ Summable fun i ↦ logDeriv (fun x ↦ 1 - eta_q i x) z

Tactic:
convert! ((summable_nat_add_iff 1).mpr this).mul_left (-2 * π * I) using 1 with n

Goal state after:
case e'_5
z : ℂ
hz : z ∈ ℍₒ
this :
  Summable fun n ↦ ↑n ^ 1 * 𝕢 ↑1 ↑{ coe := z, coe_im_pos := hz } ^ n / (1 - 𝕢 ↑1 ↑{ coe := z, coe_im_pos := hz } ^ n)
⊢ (fun i ↦ logDeriv (fun x ↦ 1 - eta_q i x) z) = fun i ↦
    -2 * ↑π * I *
      (↑(i + 1) ^ 1 * 𝕢 ↑1 ↑{ coe := z, coe_im_pos := hz } ^ (i + 1) /
        (1 - 𝕢 ↑1 ↑{ coe := z, coe_im_pos := hz } ^ (i + 1)))
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
⊢ ↑g =
    !![(1 * 0 + ↑g 0 0 * 1) * 1 + (1 * -1 + ↑g 0 0 * 0) * 0, (1 * 0 + ↑g 0 0 * 1) * -1 + (1 * -1 + ↑g 0 0 * 0) * 1;
      (0 * 0 + 1 * 1) * 1 + (0 * -1 + 1 * 0) * 0, (0 * 0 + 1 * 1) * -1 + (0 * -1 + 1 * 0) * 1]

Tactic:
ring_nf

Goal state after:
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
⊢ ↑g = !![↑g 0 0, -1 - ↑g 0 0; 1, -1]
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case neg
z : ℍ
b n : ℤ
h : ¬(b = 0 ∧ n = 0)
⊢ (↑b * ↑z + ↑n + 1)⁻¹ * ((↑b * ↑z + ↑n) ^ 2)⁻¹ + δ ![b, n] + ((↑b * ↑z + ↑n)⁻¹ - (↑b * ↑z + ↑n + 1)⁻¹) =
    ((↑b * ↑z + ↑n) ^ 2)⁻¹

Tactic:
simp only [not_and] at h

Goal state after:
case neg
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
⊢ (↑b * ↑z + ↑n + 1)⁻¹ * ((↑b * ↑z + ↑n) ^ 2)⁻¹ + δ ![b, n] + ((↑b * ↑z + ↑n)⁻¹ - (↑b * ↑z + ↑n + 1)⁻¹) =
    ((↑b * ↑z + ↑n) ^ 2)⁻¹
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «0».«1»
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
⊢ -↑g 0 0 - 1 = -1 - ↑g 0 0

Tactic:
ring_nf

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

Goal state before:
pp: z : ℍ
⊢ (↑z ^ 2)⁻¹ * G2 (S • z) - -2 * ↑π * I / ↑z = ∑' (n : ℤ) (m : ℤ), G2Term z ![m, n]

Tactic:
rw [← tsum_symmetricIco_tsum_sub_eq z, ← tsum_symmetricIco_tsum_eq_S_act z,
    ← tsum_eq_of_summable_unconditional (L := symmetricIco ℤ), ← Summable.tsum_sub]

Goal state after:
z : ℍ
⊢ ∑'[symmetricIco ℤ] (b : ℤ),
      (∑' (m : ℤ), 1 / (↑m * ↑z + ↑b) ^ 2 - ∑' (m : ℤ), (1 / (↑m * ↑z + ↑b) - 1 / (↑m * ↑z + ↑b + 1))) =
    ∑'[symmetricIco ℤ] (b : ℤ), ∑' (m : ℤ), G2Term z ![m, b]

case hf
z : ℍ
⊢ Summable (fun n ↦ ∑' (m : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2) (symmetricIco ℤ)

case hg
z : ℍ
⊢ Summable (fun n ↦ ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1))) (symmetricIco ℤ)

z : ℍ
⊢ Summable fun n ↦ ∑' (m : ℤ), G2Term z ![m, n]
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case mem.inl
γ g : SL(2, ℤ)
h1 : g = S
z : ℍ
⊢ ↑z ^ (-2) * G2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } =
    (↑z ^ 2)⁻¹ * G2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } - I * (↑π * -2) / ↑z - I * (↑π * 2) / ↑z

Tactic:
ring_nf

Goal state after:
case mem.inl
γ g : SL(2, ℤ)
h1 : g = S
z : ℍ
⊢ ↑z ^ (-2) * G2 { coe := -(↑z)⁻¹, coe_im_pos := ⋯ } = (↑z)⁻¹ ^ 2 * G2 { coe := -(↑z)⁻¹, coe_im_pos := ⋯ }
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: k : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
⊢ D F z + D G z - k * 12⁻¹ * EisensteinSeries.E2 z * (F z + G z) =
    D F z - k * 12⁻¹ * EisensteinSeries.E2 z * F z + (D G z - k * 12⁻¹ * EisensteinSeries.E2 z * G z)

Tactic:
ring_nf

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

Goal state before:
pp: k : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
⊢ D F z - D G z - k * 12⁻¹ * EisensteinSeries.E2 z * (F z - G z) =
    D F z - k * 12⁻¹ * EisensteinSeries.E2 z * F z - (D G z - k * 12⁻¹ * EisensteinSeries.E2 z * G z)

Tactic:
ring_nf

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

Goal state before:
pp: k c : ℂ
F : ℍ → ℂ
hF : MDiff F
z : ℍ
⊢ c * D F z - k * 12⁻¹ * EisensteinSeries.E2 z * (c * F z) = c * (D F z - k * 12⁻¹ * EisensteinSeries.E2 z * F z)

Tactic:
ring_nf

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

Goal state before:
pp: k₁ k₂ : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
⊢ D F z * G z + F z * D G z - (k₁ + k₂) * 12⁻¹ * EisensteinSeries.E2 z * (F z * G z) =
    (D F z - k₁ * 12⁻¹ * EisensteinSeries.E2 z * F z) * G z + F z * (D G z - k₂ * 12⁻¹ * EisensteinSeries.E2 z * G z)

Tactic:
ring_nf

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

Goal state before:
pp: z : ℂ
hz : z ≠ 0
⊢ cexp (↑24 * (log z / 2)) = z ^ 12

Tactic:
ring_nf

Goal state after:
z : ℂ
hz : z ≠ 0
⊢ cexp (log z * 12) = z ^ 12
Module: Mathlib.NumberTheory.ModularForms.Discriminant

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

Tactic:
exp_nat_mul,

Goal state after:
z : ℂ
hz : z ≠ 0
⊢ cexp (log z) ^ 12 = z ^ 12
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: z : ℍ
⊢ cexp (2 * ↑π * I * (1 + ↑z)) * ∏' (n : ℕ), (1 - cexp (2 * ↑π * I * (1 + ↑z)) ^ (n + 1)) ^ 24 =
    cexp (2 * ↑π * I * ↑z + 2 * ↑π * I) * ∏' (n : ℕ), (1 - cexp (2 * ↑π * I * ↑z + 2 * ↑π * I) ^ (n + 1)) ^ 24

Tactic:
ring_nf

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

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

Tactic:
ring_nf

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

Goal state before:
pp: 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)
⊢ (2 * ↑π * I * ↑m / ↑p) ^ k * cexp (2 * ↑π * I * ↑m / ↑p * x) =
    (2 * ↑π * I * ↑m / ↑p) ^ k * cexp (2 * ↑π * I * ↑m * x / ↑p)

Tactic:
ring_nf

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

Goal state before:
pp: z : ℍ
⊢ η (-(↑z)⁻¹) ^ 24 * (↑z ^ 12)⁻¹ = η ↑z ^ 24

Tactic:
have he : η (-(↑z)⁻¹) = (sqrt I)⁻¹ * (sqrt z * η z) := by
    simpa [neg_div] using eta_comp_eq_csqrt_I_inv z.2

Goal state after:
z : ℍ
he : η (-(↑z)⁻¹) = I.sqrt⁻¹ * ((↑z).sqrt * η ↑z)
⊢ η (-(↑z)⁻¹) ^ 24 * (↑z ^ 12)⁻¹ = η ↑z ^ 24
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inr.inl.inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hc✝ : 0 ≤ ↑(S * T) 1 0
hc : ↑(S * T) 1 0 = 1
hd : ↑(S * T) 1 1 = 1
hz : ρ ∈ 𝒟
hg : (S * T) • ρ ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (S * T))) ↑ρ‖ ≤ 1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (S * T))) ↑ρ) = 1

pp: case inr.inr.inl.inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hc✝ : 0 ≤ ↑(T * S * T) 1 0
hc : ↑(T * S * T) 1 0 = 1
hd : ↑(T * S * T) 1 1 = 1
hz : ρ ∈ 𝒟
hg : (T * S * T) • ρ ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T * S * T))) ↑ρ‖ ≤ 1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T * S * T))) ↑ρ) = 1

Tactic:
· rw [show S * T = ⟨!![0, -1; 1, 1], by simp⟩ by decide]
        norm_num [ρ, denom, normSq, ← pow_two, div_pow]

Goal state after:
case inr.inr.inl.inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hc✝ : 0 ≤ ↑(T * S * T) 1 0
hc : ↑(T * S * T) 1 0 = 1
hd : ↑(T * S * T) 1 1 = 1
hz : ρ ∈ 𝒟
hg : (T * S * T) • ρ ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T * S * T))) ↑ρ‖ ≤ 1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T * S * T))) ↑ρ) = 1
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : f =O[atTop] fun n ↦ ↑n ^ l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace ↑K
c : C(↑K, ℂ) := { toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
x : ↑K
⊢ cexp (2 * ↑π * I * (↑x / ↑p)) = cexp (2 * ↑π * I * ↑x / ↑p)

Tactic:
ring_nf

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

Goal state before:
pp: z : ℍ
N : ℕ
⊢ ↑2 * ∑ k ∈ range N, e2Summand (↑(k + 1)) z + 2 • (2 * riemannZeta 2) - 2 * riemannZeta 2 =
    2 * riemannZeta 2 + ∑ m ∈ range N, -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)

Tactic:
ring_nf

Goal state after:
z : ℍ
N : ℕ
⊢ (∑ x ∈ range N, e2Summand (↑(1 + x)) z) * 2 + riemannZeta 2 * 2 =
    riemannZeta 2 * 2 +
      ∑ x ∈ range N,
        -((↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (↑π * I * ↑z * 2) ^ (x * ↑n) * cexp (↑π * I * ↑z * 2) ^ ↑n) * 8)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
⊢ SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k (fun z ↦ cexp (2 * ↑π * I * z) ^ n) ℍₒ) ℍₒ

Tactic:
by
  have h0 : (fun n : ℕ ↦ (1 : ℂ)) =O[atTop] fun n ↦ ((n ^ 1) : ℝ) := by
    simp only [Asymptotics.isBigO_iff, norm_one, norm_pow, Real.norm_natCast, eventually_atTop]
    exact ⟨1, 1, fun b hb ↦ by norm_cast; simp [hb]⟩
  simpa using summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp k 1 (p := 1)
    (by norm_num) h0

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

Goal state before:
pp: case e_a.e_f
z : ℍ
N a : ℕ
H2 :
  ∑' (n : ℤ), ((↑n + ↑z * (↑a + 1)) ^ 2)⁻¹ =
    (I * (↑π * 2)) ^ 2 * ∑' (n : ℕ+), cexp (↑z * (↑a + 1) * (I * (↑π * 2))) ^ ↑n * ↑↑n
b : ℕ+
⊢ 2 * ((I * (↑π * 2)) ^ 2 * (cexp (↑b • (↑z * (↑a + 1) * (I * (↑π * 2)))) * ↑↑b)) =
    -(8 * (↑π ^ 2 * (cexp (↑b • (↑z * (I * ↑π) * 2)) * (cexp ((a * ↑b) • (↑z * (I * ↑π) * 2)) * ↑↑b))))

Tactic:
ring_nf

Goal state after:
case e_a.e_f
z : ℍ
N a : ℕ
H2 :
  ∑' (n : ℤ), ((↑n + ↑z * (↑a + 1)) ^ 2)⁻¹ =
    (I * (↑π * 2)) ^ 2 * ∑' (n : ℕ+), cexp (↑z * (↑a + 1) * (I * (↑π * 2))) ^ ↑n * ↑↑n
b : ℕ+
⊢ I ^ 2 * ↑π ^ 2 * ↑↑b * cexp (I * ↑π * ↑z * ↑a * ↑↑b * 2 + I * ↑π * ↑z * ↑↑b * 2) * 8 =
    -(↑π ^ 2 * ↑↑b * cexp (I * ↑π * ↑z * ↑↑b * 2) * cexp (I * ↑π * ↑z * ↑↑b * ↑a * 2) * 8)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: case e_f
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 : ℕ
⊢ -(↑n ^ k / ↑k !) = (-1) ^ k * ↑n ^ k * (-1) ^ (k + 1) / ↑k !

Tactic:
ring_nf

Goal state after:
case e_f
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 : ℕ
⊢ -(↑n ^ k * (↑k !)⁻¹) = -(↑n ^ k * (↑k !)⁻¹ * (-1) ^ (k * 2))
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzρ : z ≠ ρ
hzρ' : z ≠ 1 +ᵥ ρ
this✝¹ : T • z ≠ z
this✝ : T⁻¹ • z ≠ z
this : ↑z ≠ -↑I
hzI : Complex.I ^ 2 = ↑z ^ 2
⊢ z = I

Tactic:
sq_eq_sq_iff_eq_or_eq_neg,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z = z
hzρ : z ≠ ρ
hzρ' : z ≠ 1 +ᵥ ρ
this✝¹ : T • z ≠ z
this✝ : T⁻¹ • z ≠ z
this : ↑z ≠ -↑I
hzI : Complex.I = ↑z ∨ Complex.I = -↑z
⊢ z = I
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
d : ℕ+
⊢ 2 / ↑↑d +
      ((-↑↑d)⁻¹ - (↑↑d)⁻¹ + ∑' (n : ℕ+), ((↑↑n * ↑z - ↑↑d)⁻¹ - (↑↑n * ↑z + ↑↑d)⁻¹) +
        ∑' (n : ℕ+), ((-(↑↑n * ↑z) - ↑↑d)⁻¹ - (-(↑↑n * ↑z) + ↑↑d)⁻¹)) =
    ∑' (m : ℕ+), ((↑↑m * ↑z - ↑↑d)⁻¹ + (-(↑↑m * ↑z) + -↑↑d)⁻¹ - (↑↑m * ↑z + ↑↑d)⁻¹ - (-(↑↑m * ↑z) + ↑↑d)⁻¹)

Tactic:
ring_nf

Goal state after:
z : ℍ
d : ℕ+
⊢ ∑' (n : ℕ+), ((-↑↑d + ↑↑n * ↑z)⁻¹ - (↑↑d + ↑↑n * ↑z)⁻¹) + ∑' (n : ℕ+), ((-↑↑d - ↑z * ↑↑n)⁻¹ - (↑↑d - ↑z * ↑↑n)⁻¹) =
    ∑' (m : ℕ+), ((-↑↑d + ↑z * ↑↑m)⁻¹ + (-↑↑d - ↑z * ↑↑m)⁻¹ - (↑↑d + ↑z * ↑↑m)⁻¹ - (↑↑d - ↑z * ↑↑m)⁻¹)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℍ
⊢ jacobiTheta ↑(ModularGroup.S • τ) = (-I * ↑τ) ^ (1 / 2) * jacobiTheta ↑τ

Tactic:
have h0 : (τ : ℂ) ≠ 0 := ne_of_apply_ne im (zero_im.symm ▸ ne_of_gt τ.2)

Goal state after:
τ : ℍ
h0 : ↑τ ≠ 0
⊢ jacobiTheta ↑(ModularGroup.S • τ) = (-I * ↑τ) ^ (1 / 2) * jacobiTheta ↑τ
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
H :
  ∀ (b : ℕ+),
    ∑' (n : ℤ), ((↑↑b * ↑z + ↑n) ^ k)⁻¹ =
      (-(2 * ↑π * I)) ^ k / ↑(k - 1)! * ∑' (n : ℕ+), ↑↑n ^ (k - 1) * cexp (2 * ↑π * I * (↑↑b * ↑z)) ^ ↑n
m n : ℕ+
⊢ ↑↑n ^ (k - 1) * cexp (↑↑n * (2 * ↑π * I * (↑↑m * ↑z))) = ↑↑n ^ (k - 1) * cexp (↑↑m * ↑↑n * (2 * ↑π * I * ↑z))

Tactic:
ring_nf

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

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

Tactic:
refine (le_of_eq ?_).trans (?_ : y ^ n ^ 2 ≤ _)

Goal state after:
case refine_1
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ ‖cexp (↑π * I * ↑n ^ 2 * τ)‖ = y ^ n ^ 2

case refine_2
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ y ^ n ^ 2 ≤ rexp (-π * τ.im) ^ n.natAbs
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

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

Tactic:
norm_exp

Goal state after:
case refine_1
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ rexp (↑π * I * ↑n ^ 2 * τ).re = y ^ n ^ 2
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℤ
z : ℍ
n : ℕ
v : ↑(gammaSet 1 n 0)
⊢ eisSummand k (↑v) z = (↑n ^ k)⁻¹ * eisSummand k (divIntMap ↑n ↑v) z

Tactic:
simp_rw [eisSummand]
  nth_rw 1 2 [gammaSet_eq_gcd_mul_divIntMap v.2]
  simp [← mul_inv, ← mul_zpow, mul_add, mul_assoc]

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

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

Tactic:
zpow_natCast

Goal state after:
case refine_1
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
this : (↑π * I * ↑n ^ 2 * τ).re = -π * τ.im * ↑n ^ 2
m : ℕ
hm : n ^ 2 = ↑m
⊢ rexp (-π * τ.im) ^ m = rexp (-π * τ.im) ^ m
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

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

Tactic:
zpow_natCast

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

Goal state before:
pp: y : ℝ
hy : 1 ≤ y
τ : ℂ
hτ : τ.im = y
⊢ 2 / (1 - rexp (-π * y)) * rexp (-π * y) ≤ 2 / (1 - rexp (-(π * 1))) * rexp (-π * y)

Tactic:
neg_mul

Goal state after:
y : ℝ
hy : 1 ≤ y
τ : ℂ
hτ : τ.im = y
⊢ 2 / (1 - rexp (-(π * y))) * rexp (-(π * y)) ≤ 2 / (1 - rexp (-(π * 1))) * rexp (-(π * y))
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
⊢ (E hk) τ - 1 = β * ∑' (n : ℕ), ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)

Tactic:
zpow_natCast

Goal state after:
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
⊢ (E hk) τ - 1 = β * ∑' (n : ℕ), ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
⊢ (fun a ↦ ∏ c, (quotientFunc f c ∣[k] γ) a) =O[atImInfty] fun x ↦ ∏ i, 1

Tactic:
refine .finsetProd (Quotient.forall.mpr fun ⟨r, hr⟩ _ ↦ (translate f _).bdd_at_cusps' ?_ γ rfl)

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
this : Fintype (↥ℋ ⧸ 𝒢.subgroupOf ℋ) := Fintype.ofFinite (↥ℋ ⧸ 𝒢.subgroupOf ℋ)
x✝¹ : ↥ℋ
r : GL (Fin 2) ℝ
hr : r ∈ ℋ
x✝ : ⟦⟨r, hr⟩⟧ ∈ Finset.univ
⊢ IsCusp (γ • OnePoint.infty) (ConjAct.toConjAct (↑⟨r, hr⟩)⁻¹⁻¹ • 𝒢)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
⊢ ∑ i ∈ range p, (Ideal.Quotient.mk (span {s})) ((a ^ (i - 1) * (↑p * b) * ↑i + a ^ i) * a ^ (p - 1 - i)) =
    (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ (x - 1) * (a ^ (p - 1 - x) * (↑p * (b * ↑x)))) +
      (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ (x + (p - 1 - x)))

Tactic:
ring_nf

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
⊢ ∑ x ∈ range p,
      (Ideal.Quotient.mk (span {s})) (a ^ (x - 1) * a ^ (p - 1 - x) * ↑p * b * ↑x + a ^ x * a ^ (p - 1 - x)) =
    (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ (x - 1) * a ^ (p - 1 - x) * ↑p * b * ↑x) +
      (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ x * a ^ (p - 1 - x))
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
this : ∑ x ∈ range p, ↑x = ↑(∑ x ∈ range p, x)
⊢ (Ideal.Quotient.mk (span {s})) ↑p * (Ideal.Quotient.mk (span {s})) b *
      ((Ideal.Quotient.mk (span {s})) (a ^ (p - 2)) *
        ((Ideal.Quotient.mk (span {s})) ↑p * (Ideal.Quotient.mk (span {s})) ↑((p - 1) / 2))) =
    0

Tactic:
ring_nf

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
this : ∑ x ∈ range p, ↑x = ↑(∑ x ∈ range p, x)
⊢ (Ideal.Quotient.mk (span {s})) ↑p ^ 2 * (Ideal.Quotient.mk (span {s})) b *
        (Ideal.Quotient.mk (span {s})) (a ^ (p - 2)) *
      (Ideal.Quotient.mk (span {s})) ↑((p - 1) / 2) =
    0
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ.hn
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ ¬↑p ∣ ↑k

Tactic:
rw [Int.natCast_dvd_natCast]

Goal state after:
case succ.hn
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ ¬p ∣ k
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: w✝ : ℤ
⊢ (2 * w✝ + 1) ^ 2 % 4 = 1

Tactic:
ring_nf

Goal state after:
w✝ : ℤ
⊢ (1 + w✝ * 4 + w✝ ^ 2 * 4) % 4 = 1
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype.card (Fin (rank K)) = Fintype.card (InfinitePlace K) - 1

Tactic:
Fintype.card_fin,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ rank K = Fintype.card (InfinitePlace K) - 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realMixedSpace K
⊢ (FDerivPolarCoordRealSymm K x).det = ∏ w, (x.2 w).1

Tactic:
have : (FDerivPolarCoordRealSymm K x).toLinearMap =
      LinearMap.prodMap (LinearMap.id) (fderivPiPolarCoordSymm x.2).toLinearMap := rfl

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realMixedSpace K
this : ↑(FDerivPolarCoordRealSymm K x) = LinearMap.id.prodMap ↑(fderivPiPolarCoordSymm x.2)
⊢ (FDerivPolarCoordRealSymm K x).det = ∏ w, (x.2 w).1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' : ∀ {x : mixedSpace K}, A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)
⊢ MeasurableSet (⇑mixedSpaceOfRealSpace ⁻¹' normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A)

Tactic:
convert! hm.preimage mixedSpaceOfRealSpace.measurable

Goal state after: