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

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

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

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

Tactic:
·

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

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

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

Tactic:
·

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

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

Tactic:
·

Goal state after:
case h.inl.«2»
k : ℕ
ihn :
  ∀ m < 2,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even 2
hk : 2 < 3
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑2) =
    ↑(if 2 ≡ 2 [MOD 12] then 2 / 12 else 2 / 12 + 1)
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) * (↑m * ↑z + ↑b - (↑m * ↑z + ↑a)) * (1 / (↑m * ↑z + ↑b)) =
    (↑b - ↑a) * (1 / ((↑m * ↑z + ↑a) * (↑m * ↑z + ↑b)))

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

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

Tactic:
·

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

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

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

Tactic:
·

Goal state after:
case ha
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ ↑m * ↑z + ↑a ≠ 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)

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

Goal state before:
pp: case hb
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ ↑m * ↑z + ↑b ≠ 0

Tactic:
·

Goal state after:
case hb
z : ℍ
a b m : ℤ
hm : m ≠ 0 ∨ a ≠ 0 ∧ b ≠ 0
⊢ ↑m * ↑z + ↑b ≠ 0
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 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: case inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
⊢ (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 inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 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: 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
⊢ ↑k - 12 < 0

Tactic:
by lia

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
⊢ (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✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
⊢ (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.Modular

Goal state before:
pp: case inr.inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
hd : ↑g 1 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: case inr.inr.inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
⊢ (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: case inr.inr.inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
⊢ (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.inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
hd : ↑g 1 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 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.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)
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: 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
⊢ 3 ≤ k

Tactic:
by lia

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

Goal state before:
pp: 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
⊢ k - 12 < k

Tactic:
by lia

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inr.inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
⊢ (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: case inr.inr.inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
⊢ (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.inr.inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
⊢ (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.EisensteinSeries.QExpansion

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

pp: k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ Summable fun n ↦ ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
·

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ (-2 * ↑π * I) ^ (k + 1) / ↑k ! *
      (↑0 ^ k * cexp (2 * ↑π * I * ↑z) ^ 0 + ∑' (n : ℕ+), ↑↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ ↑n) =
    (-2 * ↑π * I) ^ (k + 1) / ↑k ! * ∑' (n : ℕ+), ↑↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ ↑n
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ Summable fun n ↦ ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
·

Goal state after:
k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ Summable fun n ↦ ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inr.inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
⊢ (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.inr.inr
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
⊢ (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 inl
k : ℤ
hk_neg : k < 0
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0

pp: case inr
k : ℤ
hk_nonneg : 0 ≤ k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0

Tactic:
·

Goal state after:
case inl
k : ℤ
hk_neg : k < 0
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case inr.inl
k : ℤ
hk_nonneg : 0 ≤ k
hk_even : Even k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0

pp: case inr.inr
k : ℤ
hk_nonneg : 0 ≤ k
hk_odd : Odd k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0

Tactic:
·

Goal state after:
case inr.inl
k : ℤ
hk_nonneg : 0 ≤ k
hk_even : Even k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case inr.inr
k : ℤ
hk_nonneg : 0 ≤ k
hk_odd : Odd k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0

Tactic:
·

Goal state after:
case inr.inr
k : ℤ
hk_nonneg : 0 ≤ k
hk_odd : Odd k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case h.inl
k : ℕ
ih :
  ∀ m < k, ∀ {f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m}, ↑(m / 12) < (qExpansion 1 ⇑f).order → f = 0
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
h : ↑(k / 12) < (qExpansion 1 ⇑f).order
h0 : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
hk12 : k < 12
⊢ CuspForm.discriminantEquiv (f.toCuspForm h0) = 0

pp: case h.inr
k : ℕ
ih :
  ∀ m < k, ∀ {f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m}, ↑(m / 12) < (qExpansion 1 ⇑f).order → f = 0
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
h : ↑(k / 12) < (qExpansion 1 ⇑f).order
h0 : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
hk12 : 12 ≤ k
⊢ CuspForm.discriminantEquiv (f.toCuspForm h0) = 0

Tactic:
·

Goal state after:
case h.inl
k : ℕ
ih :
  ∀ m < k, ∀ {f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m}, ↑(m / 12) < (qExpansion 1 ⇑f).order → f = 0
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
h : ↑(k / 12) < (qExpansion 1 ⇑f).order
h0 : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
hk12 : k < 12
⊢ CuspForm.discriminantEquiv (f.toCuspForm h0) = 0
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℕ
ih :
  ∀ m < k, ∀ {f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m}, ↑(m / 12) < (qExpansion 1 ⇑f).order → f = 0
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
h : ↑(k / 12) < (qExpansion 1 ⇑f).order
h0 : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
hk12 : k < 12
⊢ ↑k - 12 < 0

Tactic:
by lia

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

Goal state before:
pp: case h.inr
k : ℕ
ih :
  ∀ m < k, ∀ {f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m}, ↑(m / 12) < (qExpansion 1 ⇑f).order → f = 0
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
h : ↑(k / 12) < (qExpansion 1 ⇑f).order
h0 : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
hk12 : 12 ≤ k
⊢ CuspForm.discriminantEquiv (f.toCuspForm h0) = 0

Tactic:
·

Goal state after:
case h.inr
k : ℕ
ih :
  ∀ m < k, ∀ {f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m}, ↑(m / 12) < (qExpansion 1 ⇑f).order → f = 0
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
h : ↑(k / 12) < (qExpansion 1 ⇑f).order
h0 : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
hk12 : 12 ≤ k
⊢ CuspForm.discriminantEquiv (f.toCuspForm h0) = 0
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℕ
ih :
  ∀ m < k, ∀ {f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m}, ↑(m / 12) < (qExpansion 1 ⇑f).order → f = 0
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
h : ↑(k / 12) < (qExpansion 1 ⇑f).order
h0 : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
hk12 : 12 ≤ k
⊢ ↑k - 12 = ↑(k - 12)

Tactic:
by lia

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case mp
g : SL(2, ℤ)
⊢ g • I = I → g ∈ {1, -1, S, -S}

pp: case mpr
g : SL(2, ℤ)
⊢ g ∈ {1, -1, S, -S} → g • I = I

Tactic:
·

Goal state after:
case mp
g : SL(2, ℤ)
⊢ g • I = I → g ∈ {1, -1, S, -S}
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℕ
ih :
  ∀ m < k, ∀ {f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m}, ↑(m / 12) < (qExpansion 1 ⇑f).order → f = 0
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
h : ↑(k / 12) < (qExpansion 1 ⇑f).order
h0 : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
hk12 : 12 ≤ k
⊢ k - 12 < k

Tactic:
by lia

Goal state after: