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

Goal state before:
pp: case hf.hg
⊢ DifferentiableOn ℂ η upperHalfPlaneSet

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

pp: case hf.st
⊢ Set.MapsTo (fun z ↦ -1 / z) upperHalfPlaneSet upperHalfPlaneSet

Tactic:
·

Goal state after:
case hf.hg
⊢ DifferentiableOn ℂ η upperHalfPlaneSet
Module: Mathlib.NumberTheory.ModularForms.Discriminant

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

pp: case hf.st
⊢ Set.MapsTo (fun z ↦ -1 / z) upperHalfPlaneSet upperHalfPlaneSet

Tactic:
·

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

Goal state before:
pp: case hf.st
⊢ Set.MapsTo (fun z ↦ -1 / z) upperHalfPlaneSet upperHalfPlaneSet

Tactic:
·

Goal state after:
case hf.st
⊢ Set.MapsTo (fun z ↦ -1 / z) upperHalfPlaneSet upperHalfPlaneSet
Module: Mathlib.NumberTheory.Modular

Goal state before:
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.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
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
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 hg
⊢ DifferentiableOn ℂ (sqrt * η) upperHalfPlaneSet
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
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 hs2
⊢ IsOpen upperHalfPlaneSet
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
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 hsc
⊢ IsPreconnected upperHalfPlaneSet
Module: Mathlib.NumberTheory.ModularForms.Discriminant

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

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

Tactic:
·

Goal state after:
case hgn
⊢ ∀ x ∈ upperHalfPlaneSet, (sqrt * η) x ≠ 0
Module: Mathlib.NumberTheory.ModularForms.Discriminant

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

Tactic:
·

Goal state after:
case hfn
⊢ ∀ x ∈ upperHalfPlaneSet, (η ∘ fun z ↦ -1 / z) x ≠ 0
Module: Mathlib.NumberTheory.ModularForms.Discriminant

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

Tactic:
exact fun x hx ↦ eta_ne_zero (by grind [im_pnat_div_pos 1 ⟨x, hx⟩])

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

Goal state before:
pp: ⊢ ∃ c, c ≠ 0 ∧ Set.EqOn (η ∘ fun z ↦ -1 / z) (c • (sqrt * η)) upperHalfPlaneSet

Tactic:
by
  rw [← logDeriv_eqOn_iff]
  · exact fun z hz ↦ logDeriv_eta_comp_eq_logDeriv_csqrt_eta ⟨z, hz⟩
  · apply DifferentiableOn.comp (t := upperHalfPlaneSet)
    · exact fun x hx ↦ (differentiableAt_eta_of_mem_upperHalfPlaneSet hx).differentiableWithinAt
    · exact DifferentiableOn.div (by fun_prop) (by fun_prop)
        (fun x hx ↦ ne_zero (⟨x, hx⟩ : ℍ))
    · exact fun y hy ↦ by grind [im_pnat_div_pos 1 (⟨y, hy⟩ : ℍ)]
  · exact fun x hx ↦ ((differentiableAt_sqrt (mem_slitPlane ⟨x, hx⟩)).mul
     (differentiableAt_eta_of_mem_upperHalfPlaneSet hx)).differentiableWithinAt
  · exact isOpen_upperHalfPlaneSet
  · exact Convex.isPreconnected (convex_halfSpace_im_gt 0)
  · exact fun x hx ↦ mul_ne_zero (by simp [sqrt, ne_zero ⟨x, hx⟩]) (eta_ne_zero hx)
  · exact fun x hx ↦ eta_ne_zero (by grind [im_pnat_div_pos 1 ⟨x, hx⟩])

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

Goal state before:
pp: case e_a
z : ℍ
⊢ 𝕢 24 ↑z ^ 24 = 𝕢 1 ↑z

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

Tactic:
·

Goal state after:
case e_a
z : ℍ
⊢ 𝕢 24 ↑z ^ 24 = 𝕢 1 ↑z
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:
·

Goal state after:
case e_a
z : ℍ
⊢ (∏' (n : ℕ), (1 - eta_q n ↑z)) ^ 24 = ∏' (n : ℕ), (1 - eta_q n ↑z) ^ 24
Module: Mathlib.NumberTheory.Modular

Goal state before:
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.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
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:
·

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

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

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.Modular

Goal state before:
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.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
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‖
hr : ‖r‖ < 1
n : ℕ
z : ℂ
hz : z ∈ K
⊢ ‖(f n • iteratedDerivWithin k (fun z ↦ cexp (2 * ↑π * I * z / ↑p) ^ n) ℍₒ) z‖ ≤
    ‖f n‖ * (2 * |π| * ↑n / |p|) ^ k * |r| ^ n

Tactic:
have h0 := pow_le_pow_left₀ (norm_nonneg _) (norm_coe_le_norm (mkOfCompact c) ⟨z, hz⟩) n

Goal state after:
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‖
hr : ‖r‖ < 1
n : ℕ
z : ℂ
hz : z ∈ K
h0 : ‖(mkOfCompact c) ⟨z, hz⟩‖ ^ n ≤ ‖mkOfCompact c‖ ^ n
⊢ ‖(f n • iteratedDerivWithin k (fun z ↦ cexp (2 * ↑π * I * z / ↑p) ^ n) ℍₒ) z‖ ≤
    ‖f n‖ * (2 * |π| * ↑n / |p|) ^ k * |r| ^ n
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inr.inr.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 : 1 +ᵥ ρ ∈ 𝒟
hg : (S * T⁻¹) • (1 +ᵥ ρ) ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (S * T⁻¹))) ↑(1 +ᵥ ρ)‖ ≤ 1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (S * T⁻¹))) ↑(1 +ᵥ ρ)) = 1

pp: case inr.inr.inr.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 : 1 +ᵥ ρ ∈ 𝒟
hg : (T⁻¹ * S * T⁻¹) • (1 +ᵥ ρ) ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T⁻¹ * S * T⁻¹))) ↑(1 +ᵥ ρ)‖ ≤ 1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T⁻¹ * S * T⁻¹))) ↑(1 +ᵥ ρ)) = 1

Tactic:
·

Goal state after:
case inr.inr.inr.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 : 1 +ᵥ ρ ∈ 𝒟
hg : (S * T⁻¹) • (1 +ᵥ ρ) ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (S * T⁻¹))) ↑(1 +ᵥ ρ)‖ ≤ 1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (S * T⁻¹))) ↑(1 +ᵥ ρ)) = 1
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: case pos
q : ℂ
hq : q ∈ Metric.ball 0 1
hq0 : q = 0
⊢ cuspFunction 1 Δ q = (fun q ↦ q * ∏' (i : ℕ), (1 - q ^ (i + 1)) ^ 24) q

pp: case neg
q : ℂ
hq : q ∈ Metric.ball 0 1
hq0 : ¬q = 0
⊢ cuspFunction 1 Δ q = (fun q ↦ q * ∏' (i : ℕ), (1 - q ^ (i + 1)) ^ 24) q

Tactic:
·

Goal state after:
case pos
q : ℂ
hq : q ∈ Metric.ball 0 1
hq0 : q = 0
⊢ cuspFunction 1 Δ q = (fun q ↦ q * ∏' (i : ℕ), (1 - q ^ (i + 1)) ^ 24) q
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: case neg
q : ℂ
hq : q ∈ Metric.ball 0 1
hq0 : ¬q = 0
⊢ cuspFunction 1 Δ q = (fun q ↦ q * ∏' (i : ℕ), (1 - q ^ (i + 1)) ^ 24) q

Tactic:
·

Goal state after:
case neg
q : ℂ
hq : q ∈ Metric.ball 0 1
hq0 : ¬q = 0
⊢ cuspFunction 1 Δ q = (fun q ↦ q * ∏' (i : ℕ), (1 - q ^ (i + 1)) ^ 24) q
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inr.inr.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 : 1 +ᵥ ρ ∈ 𝒟
hg : (T⁻¹ * S * T⁻¹) • (1 +ᵥ ρ) ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T⁻¹ * S * T⁻¹))) ↑(1 +ᵥ ρ)‖ ≤ 1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T⁻¹ * S * T⁻¹))) ↑(1 +ᵥ ρ)) = 1

Tactic:
·

Goal state after:
case inr.inr.inr.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 : 1 +ᵥ ρ ∈ 𝒟
hg : (T⁻¹ * S * T⁻¹) • (1 +ᵥ ρ) ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T⁻¹ * S * T⁻¹))) ↑(1 +ᵥ ρ)‖ ≤ 1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) (T⁻¹ * S * T⁻¹))) ↑(1 +ᵥ ρ)) = 1
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: case hsum
k : ℕ
z : ℍ
⊢ ∀ t ∈ ℍₒ, Summable fun n ↦ cexp (2 * ↑π * I * t) ^ n

pp: case h
k : ℕ
z : ℍ
⊢ ∀ (k_1 : ℕ),
    1 ≤ k_1 →
      k_1 ≤ k → SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k_1 (fun z ↦ cexp (2 * ↑π * I * z) ^ n) ℍₒ) ℍₒ

pp: case hf2
k : ℕ
z : ℍ
⊢ ∀ (n k_1 : ℕ) (r : ℂ),
    k_1 ≤ k → r ∈ ℍₒ → DifferentiableAt ℂ (iteratedDerivWithin k_1 (fun z ↦ cexp (2 * ↑π * I * z) ^ n) ℍₒ) r

Tactic:
·

Goal state after:
case hsum
k : ℕ
z : ℍ
⊢ ∀ t ∈ ℍₒ, Summable fun n ↦ cexp (2 * ↑π * I * t) ^ n
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: case h
k : ℕ
z : ℍ
⊢ ∀ (k_1 : ℕ),
    1 ≤ k_1 →
      k_1 ≤ k → SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k_1 (fun z ↦ cexp (2 * ↑π * I * z) ^ n) ℍₒ) ℍₒ

pp: case hf2
k : ℕ
z : ℍ
⊢ ∀ (n k_1 : ℕ) (r : ℂ),
    k_1 ≤ k → r ∈ ℍₒ → DifferentiableAt ℂ (iteratedDerivWithin k_1 (fun z ↦ cexp (2 * ↑π * I * z) ^ n) ℍₒ) r

Tactic:
·

Goal state after:
case h
k : ℕ
z : ℍ
⊢ ∀ (k_1 : ℕ),
    1 ≤ k_1 →
      k_1 ≤ k → SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k_1 (fun z ↦ cexp (2 * ↑π * I * z) ^ n) ℍₒ) ℍₒ
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: case hf2
k : ℕ
z : ℍ
⊢ ∀ (n k_1 : ℕ) (r : ℂ),
    k_1 ≤ k → r ∈ ℍₒ → DifferentiableAt ℂ (iteratedDerivWithin k_1 (fun z ↦ cexp (2 * ↑π * I * z) ^ n) ℍₒ) r

Tactic:
·

Goal state after:
case hf2
k : ℕ
z : ℍ
⊢ ∀ (n k_1 : ℕ) (r : ℂ),
    k_1 ≤ k → r ∈ ℍₒ → DifferentiableAt ℂ (iteratedDerivWithin k_1 (fun z ↦ cexp (2 * ↑π * I * z) ^ n) ℍₒ) r
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

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

pp: case hf
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ ContDiffWithinAt ℂ (↑k) (fun z ↦ ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z

Tactic:
·

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ -(2 * ↑π * I * iteratedDerivWithin k (fun z ↦ ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z) =
    -(2 * ↑π * I) * ∑' (n : ℕ), iteratedDerivWithin k (fun s ↦ cexp (2 * ↑π * I * s) ^ n) ℍₒ ↑z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: case hf
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ ContDiffWithinAt ℂ (↑k) (fun z ↦ ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z

Tactic:
·

Goal state after:
case hf
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ ContDiffWithinAt ℂ (↑k) (fun z ↦ ∑' (n : ℕ), cexp (2 * ↑π * I * z) ^ n) ℍₒ ↑z
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: i : ℕ
hi : i < 1
⊢ i = 0

Tactic:
by lia

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

Goal state before:
pp: k : ℤ
hk : k < 12
⊢ k - 12 < 0

Tactic:
by lia

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : (g • z).im = z.im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 →
      g • z ∈ 𝒟 →
        (g • z).im = z.im →
          0 ≤ ↑g 1 0 →
            (g = 1 ∨ g = -1) ∨
              (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
                (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
                  (g = S ∨ g = -S) ∧ ‖↑z‖ = 1 ∨
                    (g = T * S ∨ g = -(T * S)) ∧ z = 1 +ᵥ ρ ∨
                      (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                        (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                          (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                            (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ
hc : ¬0 ≤ ↑g 1 0
⊢ (g = 1 ∨ g = -1) ∨
    (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
      (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
        (g = S ∨ g = -S) ∧ ‖↑z‖ = 1 ∨
          (g = T * S ∨ g = -(T * S)) ∧ z = 1 +ᵥ ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                  (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ

pp: g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : (g • z).im = z.im
hc : 0 ≤ ↑g 1 0
⊢ (g = 1 ∨ g = -1) ∨
    (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
      (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
        (g = S ∨ g = -S) ∧ ‖↑z‖ = 1 ∨
          (g = T * S ∨ g = -(T * S)) ∧ z = 1 +ᵥ ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                  (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ

Tactic:
·

Goal state after:
case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : (g • z).im = z.im
this :
  ∀ {g : SL(2, ℤ)} {z : ℍ},
    z ∈ 𝒟 →
      g • z ∈ 𝒟 →
        (g • z).im = z.im →
          0 ≤ ↑g 1 0 →
            (g = 1 ∨ g = -1) ∨
              (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
                (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
                  (g = S ∨ g = -S) ∧ ‖↑z‖ = 1 ∨
                    (g = T * S ∨ g = -(T * S)) ∧ z = 1 +ᵥ ρ ∨
                      (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                        (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                          (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                            (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ
hc : ¬0 ≤ ↑g 1 0
⊢ (g = 1 ∨ g = -1) ∨
    (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
      (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
        (g = S ∨ g = -S) ∧ ‖↑z‖ = 1 ∨
          (g = T * S ∨ g = -(T * S)) ∧ z = 1 +ᵥ ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                  (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case n
k : ℕ
hk : 3 ≤ k
hk2 : Even k
⊢ Submodule.Quotient.mk (E hk) ≠ 0

pp: case h
k : ℕ
hk : 3 ≤ k
hk2 : Even k
⊢ ∀
    (w :
      ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k ⧸
        cuspFormSubmodule (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k),
    ∃ c, c • Submodule.Quotient.mk (E hk) = w

Tactic:
·

Goal state after:
case n
k : ℕ
hk : 3 ≤ k
hk2 : Even k
⊢ Submodule.Quotient.mk (E hk) ≠ 0
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case h
k : ℕ
hk : 3 ≤ k
hk2 : Even k
⊢ ∀
    (w :
      ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k ⧸
        cuspFormSubmodule (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k),
    ∃ c, c • Submodule.Quotient.mk (E hk) = w

Tactic:
·

Goal state after:
case h
k : ℕ
hk : 3 ≤ k
hk2 : Even k
⊢ ∀
    (w :
      ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k ⧸
        cuspFormSubmodule (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k),
    ∃ c, c • Submodule.Quotient.mk (E hk) = w
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: case e'_5
z : ℍ
hS : Summable fun n ↦ ↑((σ 1) (n + 1)) * cexp (2 * ↑π * I * ↑z) ^ (n + 1)
⊢ (fun n ↦ (if n + 1 = 0 then 1 else -24 * ↑((σ 1) (n + 1))) • cexp (2 * ↑π * I * ↑z) ^ (n + 1)) = fun i ↦
    -24 * (↑((σ 1) (i + 1)) * cexp (2 * ↑π * I * ↑z) ^ (i + 1))

pp: case e'_6
z : ℍ
hS : Summable fun n ↦ ↑((σ 1) (n + 1)) * cexp (2 * ↑π * I * ↑z) ^ (n + 1)
⊢ E2 z - ∑ i ∈ range 1, (if i = 0 then 1 else -24 * ↑((σ 1) i)) • cexp (2 * ↑π * I * ↑z) ^ i =
    ∑' (b : ℕ), -24 * (↑((σ 1) (b + 1)) * cexp (2 * ↑π * I * ↑z) ^ (b + 1))

Tactic:
·

Goal state after:
case e'_5
z : ℍ
hS : Summable fun n ↦ ↑((σ 1) (n + 1)) * cexp (2 * ↑π * I * ↑z) ^ (n + 1)
⊢ (fun n ↦ (if n + 1 = 0 then 1 else -24 * ↑((σ 1) (n + 1))) • cexp (2 * ↑π * I * ↑z) ^ (n + 1)) = fun i ↦
    -24 * (↑((σ 1) (i + 1)) * cexp (2 * ↑π * I * ↑z) ^ (i + 1))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: case e'_6
z : ℍ
hS : Summable fun n ↦ ↑((σ 1) (n + 1)) * cexp (2 * ↑π * I * ↑z) ^ (n + 1)
⊢ E2 z - ∑ i ∈ range 1, (if i = 0 then 1 else -24 * ↑((σ 1) i)) • cexp (2 * ↑π * I * ↑z) ^ i =
    ∑' (b : ℕ), -24 * (↑((σ 1) (b + 1)) * cexp (2 * ↑π * I * ↑z) ^ (b + 1))

Tactic:
·

Goal state after:
case e'_6
z : ℍ
hS : Summable fun n ↦ ↑((σ 1) (n + 1)) * cexp (2 * ↑π * I * ↑z) ^ (n + 1)
⊢ E2 z - ∑ i ∈ range 1, (if i = 0 then 1 else -24 * ↑((σ 1) i)) • cexp (2 * ↑π * I * ↑z) ^ i =
    ∑' (b : ℕ), -24 * (↑((σ 1) (b + 1)) * cexp (2 * ↑π * I * ↑z) ^ (b + 1))
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case h.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 : k < 3
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1)

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)

pp: case h.inr.inr
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 : 12 ≤ k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1)

Tactic:
·

Goal state after:
case h.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 : k < 3
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1)