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

Goal state before:
pp: z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ ∑'[symmetricIcc ℤ] (m : ℤ), e2Summand m z =
    ∑' (b : ℤ),
      (∑' (n : ℤ), G2Term z ![b, n] + ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑b * ↑z + ↑n) - 1 / (↑b * ↑z + ↑n + 1)))

pp: case hf
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ Summable fun m ↦ ∑' (n : ℤ), G2Term z ![m, n]

pp: case hg
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ Summable fun m ↦ ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1))

Tactic:
·

Goal state after:
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ ∑'[symmetricIcc ℤ] (m : ℤ), e2Summand m z =
    ∑' (b : ℤ),
      (∑' (n : ℤ), G2Term z ![b, n] + ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑b * ↑z + ↑n) - 1 / (↑b * ↑z + ↑n + 1)))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ ∑'[symmetricIcc ℤ] (m : ℤ), e2Summand m z =
    ∑'[symmetricIcc ℤ] (b : ℤ),
      (∑' (n : ℤ), G2Term z ![b, n] + ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑b * ↑z + ↑n) - 1 / (↑b * ↑z + ↑n + 1)))

pp: z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ Summable fun b ↦
    ∑' (n : ℤ), G2Term z ![b, n] + ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑b * ↑z + ↑n) - 1 / (↑b * ↑z + ↑n + 1))

Tactic:
·

Goal state after:
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ ∑'[symmetricIcc ℤ] (m : ℤ), e2Summand m z =
    ∑'[symmetricIcc ℤ] (b : ℤ),
      (∑' (n : ℤ), G2Term z ![b, n] + ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑b * ↑z + ↑n) - 1 / (↑b * ↑z + ↑n + 1)))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ Summable fun b ↦
    ∑' (n : ℤ), G2Term z ![b, n] + ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑b * ↑z + ↑n) - 1 / (↑b * ↑z + ↑n + 1))

Tactic:
·

Goal state after:
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ Summable fun b ↦
    ∑' (n : ℤ), G2Term z ![b, n] + ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑b * ↑z + ↑n) - 1 / (↑b * ↑z + ↑n + 1))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case hf
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ Summable fun m ↦ ∑' (n : ℤ), G2Term z ![m, n]

pp: case hg
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ Summable fun m ↦ ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1))

Tactic:
·

Goal state after:
case hf
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ Summable fun m ↦ ∑' (n : ℤ), G2Term z ![m, n]
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case hg
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ Summable fun m ↦ ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1))

Tactic:
·

Goal state after:
case hg
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ Summable fun m ↦ ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: 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]

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

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

pp: z : ℍ
⊢ Summable fun n ↦ ∑' (m : ℤ), G2Term z ![m, n]

Tactic:
·

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]
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

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

pp: case hf
z : ℍ
N : ℤ
⊢ Summable fun m ↦ 1 / (↑m * ↑z + ↑N) ^ 2

pp: case hg
z : ℍ
N : ℤ
⊢ Summable fun m ↦ 1 / (↑m * ↑z + ↑N) - 1 / (↑m * ↑z + ↑N + 1)

Tactic:
·

Goal state after:
z : ℍ
N : ℤ
⊢ ∑' (b : ℤ), (1 / (↑b * ↑z + ↑N) ^ 2 - (1 / (↑b * ↑z + ↑N) - 1 / (↑b * ↑z + ↑N + 1))) = ∑' (m : ℤ), G2Term z ![m, N]
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case hf
z : ℍ
N : ℤ
⊢ Summable fun m ↦ 1 / (↑m * ↑z + ↑N) ^ 2

pp: case hg
z : ℍ
N : ℤ
⊢ Summable fun m ↦ 1 / (↑m * ↑z + ↑N) - 1 / (↑m * ↑z + ↑N + 1)

Tactic:
·

Goal state after:
case hf
z : ℍ
N : ℤ
⊢ Summable fun m ↦ 1 / (↑m * ↑z + ↑N) ^ 2
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case hg
z : ℍ
N : ℤ
⊢ Summable fun m ↦ 1 / (↑m * ↑z + ↑N) - 1 / (↑m * ↑z + ↑N + 1)

Tactic:
·

Goal state after:
case hg
z : ℍ
N : ℤ
⊢ Summable fun m ↦ 1 / (↑m * ↑z + ↑N) - 1 / (↑m * ↑z + ↑N + 1)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

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

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

pp: z : ℍ
⊢ Summable fun n ↦ ∑' (m : ℤ), G2Term z ![m, n]

Tactic:
·

Goal state after:
case hf
z : ℍ
⊢ Summable (fun n ↦ ∑' (m : ℤ), 1 / (↑m * ↑z + ↑n) ^ 2) (symmetricIco ℤ)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case hre
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 + (-2 * z.re + 1) ≤ 1
this : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
⊢ z.re = (1 +ᵥ ρ).re

pp: case hnorm
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 + (-2 * z.re + 1) ≤ 1
this : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
⊢ ‖↑z‖ = ‖↑(1 +ᵥ ρ)‖

Tactic:
·

Goal state after:
case hre
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 + (-2 * z.re + 1) ≤ 1
this : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
⊢ z.re = (1 +ᵥ ρ).re
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

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

pp: z : ℍ
⊢ Summable fun n ↦ ∑' (m : ℤ), G2Term z ![m, n]

Tactic:
·

Goal state after:
case hg
z : ℍ
⊢ Summable (fun n ↦ ∑' (m : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1))) (symmetricIco ℤ)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
⊢ Summable fun n ↦ ∑' (m : ℤ), G2Term z ![m, n]

Tactic:
·

Goal state after:
z : ℍ
⊢ Summable fun n ↦ ∑' (m : ℤ), G2Term z ![m, n]
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case hnorm
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 + (-2 * z.re + 1) ≤ 1
this : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
⊢ ‖↑z‖ = ‖↑(1 +ᵥ ρ)‖

Tactic:
·

Goal state after:
case hnorm
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 + (-2 * z.re + 1) ≤ 1
this : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
⊢ ‖↑z‖ = ‖↑(1 +ᵥ ρ)‖
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case h
z : ℍ
⊢ Summable (Function.uncurry fun m n ↦ G2Term z ![m, n])

pp: case h₁
z : ℍ
⊢ ∀ (b : ℤ), Summable fun n ↦ G2Term z ![b, n]

pp: case h₂
z : ℍ
⊢ ∀ (c : ℤ), Summable fun b ↦ G2Term z ![b, c]

Tactic:
·

Goal state after:
case h
z : ℍ
⊢ Summable (Function.uncurry fun m n ↦ G2Term z ![m, n])
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case h₁
z : ℍ
⊢ ∀ (b : ℤ), Summable fun n ↦ G2Term z ![b, n]

pp: case h₂
z : ℍ
⊢ ∀ (c : ℤ), Summable fun b ↦ G2Term z ![b, c]

Tactic:
·

Goal state after:
case h₁
z : ℍ
⊢ ∀ (b : ℤ), Summable fun n ↦ G2Term z ![b, n]
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case h₂
z : ℍ
⊢ ∀ (c : ℤ), Summable fun b ↦ G2Term z ![b, c]

Tactic:
·

Goal state after:
case h₂
z : ℍ
⊢ ∀ (c : ℤ), Summable fun b ↦ G2Term z ![b, c]
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case mem.inl
γ g : SL(2, ℤ)
h1 : g = S
⊢ G2 ∣[2] g = G2 - D2 g

pp: case mem.inr
γ g : SL(2, ℤ)
h2 : g = T
⊢ G2 ∣[2] g = G2 - D2 g

Tactic:
·

Goal state after:
case mem.inl
γ g : SL(2, ℤ)
h1 : g = S
⊢ G2 ∣[2] g = G2 - D2 g
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case mem.inr
γ g : SL(2, ℤ)
h2 : g = T
⊢ G2 ∣[2] g = G2 - D2 g

Tactic:
·

Goal state after:
case mem.inr
γ g : SL(2, ℤ)
h2 : g = T
⊢ G2 ∣[2] g = G2 - D2 g
Module: Mathlib.NumberTheory.ModularForms.Derivative

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

Tactic:
rw [show (c • F) ∘ ofComplex = c • (F ∘ ofComplex) from rfl,
    deriv_const_smul c hFz, smul_eq_mul]

Goal state after:
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)
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: F : ℍ → ℂ
k : ℂ
hF : MDiff F
⊢ MDiff (serreDerivative k F)

Tactic:
by
  refine (normalizedDerivOfComplex_mdifferentiable hF).sub ?_
  convert!
    (MDifferentiable.mul mdifferentiable_const (E2_mdifferentiable.mul hF) :
      MDiff (fun z ↦ (k * 12⁻¹) * (EisensteinSeries.E2 z * F z)))
  simp [Pi.mul_apply, mul_assoc, mul_left_comm, mul_comm]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
this : ∀ {g : SL(2, ℤ)} {z : ℍ}, z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → (g • z).im = z.im
hden : ¬z.im ≤ (g • z).im
⊢ (g • z).im = z.im

pp: g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
⊢ (g • z).im = z.im

Tactic:
·

Goal state after:
case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
this : ∀ {g : SL(2, ℤ)} {z : ℍ}, z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → (g • z).im = z.im
hden : ¬z.im ≤ (g • z).im
⊢ (g • z).im = z.im
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))
⊢ (2 * ↑π * I)⁻¹ * deriv (F ∣[k] g ∘ ↑ofComplex) ↑z =
    (↑(↑g).det)⁻¹ *
        ((σ g) ((2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑(g • z)) *
            ↑|↑(Matrix.GeneralLinearGroup.det g)| ^ (k + 2 - 1) *
          denom g ↑z ^ (-(k + 2))) -
      ↑k * (2 * ↑π * I)⁻¹ * (↑(↑g 1 0) / denom g ↑z) *
        ((σ g) (F (g • z)) * ↑|↑(Matrix.GeneralLinearGroup.det g)| ^ (k - 1) * denom g ↑z ^ (-k))

Tactic:
((((h_F.comp (z : ℂ) h_smul).mul h_denom).const_mul _).congr_of_eventuallyEq hcomp).deriv

Goal state after:
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))
⊢ (2 * ↑π * I)⁻¹ *
      (↑(↑g).det ^ (k - 1) *
        (deriv (F ∘ ↑ofComplex) ↑(g • ↑ofComplex ↑z) * (↑(↑g).det / denom g ↑z ^ 2) * denom g ↑z ^ (-k) +
          ((F ∘ ↑ofComplex) ∘ fun w ↦ ↑(g • ↑ofComplex w)) ↑z * (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)))) =
    (↑(↑g).det)⁻¹ *
        ((σ g) ((2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑(g • z)) *
            ↑|↑(Matrix.GeneralLinearGroup.det g)| ^ (k + 2 - 1) *
          denom g ↑z ^ (-(k + 2))) -
      ↑k * (2 * ↑π * I)⁻¹ * (↑(↑g 1 0) / denom g ↑z) *
        ((σ g) (F (g • z)) * ↑|↑(Matrix.GeneralLinearGroup.det g)| ^ (k - 1) * denom g ↑z ^ (-k))
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ} {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → 0 ≤ ↑g 1 0 → (g • z).im = z.im
hc : ¬0 ≤ ↑g 1 0
⊢ (g • z).im = z.im

pp: g✝¹ : SL(2, ℤ)
z✝¹ : ℍ
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
hc : 0 ≤ ↑g 1 0
⊢ (g • z).im = z.im

Tactic:
·

Goal state after:
case inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ} {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → 0 ≤ ↑g 1 0 → (g • z).im = z.im
hc : ¬0 ≤ ↑g 1 0
⊢ (g • z).im = z.im
Module: Mathlib.NumberTheory.Modular

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

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

Tactic:
·

Goal state after:
case inl
g✝¹ : SL(2, ℤ)
z✝¹ : ℍ
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 0
⊢ (g • z).im = z.im
Module: Mathlib.NumberTheory.Modular

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

Tactic:
·

Goal state after:
case inr
g✝¹ : SL(2, ℤ)
z✝¹ : ℍ
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
⊢ (g • z).im = z.im
Module: Mathlib.NumberTheory.Modular

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

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

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

Tactic:
·

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

Goal state before:
pp: z : ℍ
⊢ deriv (fun x ↦ -x⁻¹) ↑z * logDeriv η (-(↑z)⁻¹) = (↑z ^ 2)⁻¹ * logDeriv η (-(↑z)⁻¹)

pp: case hf
z : ℍ
⊢ DifferentiableAt ℂ η (-(↑z)⁻¹)

pp: case hg
z : ℍ
⊢ DifferentiableAt ℂ (fun x ↦ -x⁻¹) ↑z

Tactic:
·

Goal state after:
z : ℍ
⊢ deriv (fun x ↦ -x⁻¹) ↑z * logDeriv η (-(↑z)⁻¹) = (↑z ^ 2)⁻¹ * logDeriv η (-(↑z)⁻¹)
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: case hf
z : ℍ
⊢ DifferentiableAt ℂ η (-(↑z)⁻¹)

pp: case hg
z : ℍ
⊢ DifferentiableAt ℂ (fun x ↦ -x⁻¹) ↑z

Tactic:
·

Goal state after:
case hf
z : ℍ
⊢ DifferentiableAt ℂ η (-(↑z)⁻¹)
Module: Mathlib.NumberTheory.Modular

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

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

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

Tactic:
·

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

Goal state before:
pp: case hg
z : ℍ
⊢ DifferentiableAt ℂ (fun x ↦ -x⁻¹) ↑z

Tactic:
·

Goal state after:
case hg
z : ℍ
⊢ DifferentiableAt ℂ (fun x ↦ -x⁻¹) ↑z
Module: Mathlib.NumberTheory.Modular

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

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

Tactic:
·

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

Goal state before:
pp: z : ℍ
hE2 :
  E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * (↑z ^ 2)⁻¹ =
    E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑(↑ModularGroup.S 1 0) / ↑z)
⊢ (E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑1 / ↑z)) * (↑π * I / 12) = 1 / ↑z / 2 + ↑π * I / 12 * E2 z

pp: z : ℍ
hE2 :
  E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * (↑z ^ 2)⁻¹ =
    E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑(↑ModularGroup.S 1 0) / ↑z)
⊢ 1 / ↑z / 2 + ↑π * I / 12 * E2 z = ↑z ^ (-1 / 2) / 2 * (↑z ^ 2⁻¹)⁻¹ + ↑π * I / 12 * E2 z

Tactic:
·

Goal state after:
z : ℍ
hE2 :
  E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * (↑z ^ 2)⁻¹ =
    E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑(↑ModularGroup.S 1 0) / ↑z)
⊢ (E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑1 / ↑z)) * (↑π * I / 12) = 1 / ↑z / 2 + ↑π * I / 12 * E2 z
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: z : ℍ
hE2 :
  E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * (↑z ^ 2)⁻¹ =
    E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑(↑ModularGroup.S 1 0) / ↑z)
⊢ 1 / ↑z / 2 + ↑π * I / 12 * E2 z = ↑z ^ (-1 / 2) / 2 * (↑z ^ 2⁻¹)⁻¹ + ↑π * I / 12 * E2 z

Tactic:
·

Goal state after:
z : ℍ
hE2 :
  E2 { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * (↑z ^ 2)⁻¹ =
    E2 z - 6 / ↑π ^ 2 * 2⁻¹ * (2 * ↑π * I * ↑(↑ModularGroup.S 1 0) / ↑z)
⊢ 1 / ↑z / 2 + ↑π * I / 12 * E2 z = ↑z ^ (-1 / 2) / 2 * (↑z ^ 2⁻¹)⁻¹ + ↑π * I / 12 * E2 z
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: ⊢ Set.EqOn (logDeriv (η ∘ fun z ↦ -1 / z)) (logDeriv (sqrt * η)) upperHalfPlaneSet

pp: case hf
⊢ DifferentiableOn ℂ (η ∘ fun z ↦ -1 / z) upperHalfPlaneSet

pp: case hg
⊢ DifferentiableOn ℂ (sqrt * η) upperHalfPlaneSet

pp: case hs2
⊢ IsOpen upperHalfPlaneSet

pp: case hsc
⊢ IsPreconnected upperHalfPlaneSet

pp: case hgn
⊢ ∀ x ∈ upperHalfPlaneSet, (sqrt * η) x ≠ 0

pp: case hfn
⊢ ∀ x ∈ upperHalfPlaneSet, (η ∘ fun z ↦ -1 / z) x ≠ 0

Tactic:
·

Goal state after:
⊢ Set.EqOn (logDeriv (η ∘ fun z ↦ -1 / z)) (logDeriv (sqrt * η)) upperHalfPlaneSet
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: case hf
⊢ DifferentiableOn ℂ (η ∘ fun z ↦ -1 / z) upperHalfPlaneSet

pp: case hg
⊢ DifferentiableOn ℂ (sqrt * η) upperHalfPlaneSet

pp: case hs2
⊢ IsOpen upperHalfPlaneSet

pp: case hsc
⊢ IsPreconnected upperHalfPlaneSet

pp: case hgn
⊢ ∀ x ∈ upperHalfPlaneSet, (sqrt * η) x ≠ 0

pp: case hfn
⊢ ∀ x ∈ upperHalfPlaneSet, (η ∘ fun z ↦ -1 / z) x ≠ 0

Tactic:
·

Goal state after:
case hf
⊢ DifferentiableOn ℂ (η ∘ fun z ↦ -1 / z) upperHalfPlaneSet
Module: Mathlib.NumberTheory.Modular

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

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

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

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