awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
c6 : ℂ
hc6 : c6 • E₆ = (f.mul f).mul f
hqc4 : c4 • qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 2
hqc6 : c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 3
⊢ qExpansion 1 (⇑f : (a : ℍ) → ℂ) = 0

Tactic:
eq_zero_of_pow_eq_smul (E_qExpansion_coeff_zero _ ⟨2, rfl⟩)
    (E_qExpansion_coeff_zero _ ⟨3, rfl⟩) E₄_qExpansion_coeff_one E₆_qExpansion_coeff_one hqc4 hqc6

Premises used: ModularForm.E₆_qExpansion_coeff_one, ModularForm.E₄_qExpansion_coeff_one, Exists.intro, _private.0.ModularForm.eq_zero_of_pow_eq_smul, EisensteinSeries.E_qExpansion_coeff_zero, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
c6 : ℂ
hc6 : c6 • E₆ = (f.mul f).mul f
hqc4 : c4 • qExpansion 1 (⇑E₄ : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 2
hqc6 : c6 • qExpansion 1 (⇑E₆ : (a : ℍ) → ℂ) = HPow.hPow (β := ℕ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) 3
⊢ qExpansion 1 (⇑f : (a : ℍ) → ℂ) = 0

Tactic:
exact eq_zero_of_pow_eq_smul (E_qExpansion_coeff_zero _ ⟨2, rfl⟩)
    (E_qExpansion_coeff_zero _ ⟨3, rfl⟩) E₄_qExpansion_coeff_one E₆_qExpansion_coeff_one hqc4 hqc6

Premises used: ModularForm.E₆_qExpansion_coeff_one, ModularForm.E₄_qExpansion_coeff_one, Exists.intro, _private.0.ModularForm.eq_zero_of_pow_eq_smul, EisensteinSeries.E_qExpansion_coeff_zero, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 2) = 0

Tactic:
simpa [rank_zero_iff_forall_zero, ModularForm.qExpansion_eq_zero_iff]
    using weight_two_qExpansion_eq_zero

Premises used: rank_zero_iff_forall_zero, _private.0.ModularForm.weight_two_qExpansion_eq_zero, ModularForm.qExpansion_eq_zero_iff
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
⊢ k < 3 ∨ 3 ≤ k ∧ k < 12 ∨ 12 ≤ k

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
⊢ k < 3 ∨ 3 ≤ k ∧ k < 12 ∨ 12 ≤ k

Tactic:
have : k < 3 ∨ (3 ≤ k ∧ k < 12) ∨ 12 ≤ k := by grind
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
this : k < 3 ∨ 3 ≤ k ∧ k < 12 ∨ 12 ≤ k
h :
  ∀ (hk : k < 3),
    Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
      (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})
h₁ :
  ∀ (hk : 3 ≤ k ∧ k < 12),
    Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
      (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})
h₂ :
  ∀ (hk : 12 ≤ k),
    Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
      (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
    (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})

Tactic:
rcases this with hk | hk | hk
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
hk : k < 3
h :
  ∀
    (ihn :
      ∀ m < 0,
        ∀ (hk2 : Even m),
          Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
            (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0}))
    (hk2 : Even (α := ℕ) 0) (hk : LT.lt (α := ℕ) 0 3),
    Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑0 : ℤ)) =
      (↑(if 0 ≡ 2 [MOD 12] then 0 / 12 else 0 / 12 + 1) : Cardinal.{0})
h₁ :
  ∀
    (ihn :
      ∀ m < 1,
        ∀ (hk2 : Even m),
          Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
            (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0}))
    (hk2 : Even (α := ℕ) 1) (hk : LT.lt (α := ℕ) 1 3),
    Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑1 : ℤ)) =
      (↑(if 1 ≡ 2 [MOD 12] then 1 / 12 else 1 / 12 + 1) : Cardinal.{0})
h₂ :
  ∀
    (ihn :
      ∀ m < 2,
        ∀ (hk2 : Even m),
          Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
            (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0}))
    (hk2 : Even (α := ℕ) 2) (hk : LT.lt (α := ℕ) 2 3),
    Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑2 : ℤ)) =
      (↑(if 2 ≡ 2 [MOD 12] then 2 / 12 else 2 / 12 + 1) : Cardinal.{0})
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
    (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})

Tactic:
interval_cases k
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
ihn :
  ∀ m < 0,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even (α := ℕ) 0
hk : LT.lt (α := ℕ) 0 3
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑0 : ℤ)) =
    (↑(if 0 ≡ 2 [MOD 12] then 0 / 12 else 0 / 12 + 1) : Cardinal.{0})

Tactic:
simpa using levelOne_weight_zero_rank_one

Premises used: ModularForm.levelOne_weight_zero_rank_one
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
ihn :
  ∀ m < 1,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even (α := ℕ) 1
hk : LT.lt (α := ℕ) 1 3
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑1 : ℤ)) =
    (↑(if 1 ≡ 2 [MOD 12] then 1 / 12 else 1 / 12 + 1) : Cardinal.{0})

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
ihn :
  ∀ m < 2,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even (α := ℕ) 2
hk : LT.lt (α := ℕ) 2 3
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑2 : ℤ)) =
    (↑(if 2 ≡ 2 [MOD 12] then 2 / 12 else 2 / 12 + 1) : Cardinal.{0})

Tactic:
simpa [Nat.ModEq] using levelOne_weight_two_rank_zero

Premises used: Nat.ModEq, ModularForm.levelOne_weight_two_rank_zero
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
hk : 3 ≤ k ∧ k < 12
⊢ HSub.hSub (α := ℤ) (↑k : ℤ) 12 < 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
hk : 3 ≤ k ∧ k < 12
h : HAdd.hAdd (α := Cardinal.{0}) 1 0 = (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
    (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})

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

Premises used: ModularForm.levelOne_neg_weight_rank_zero, And.left, ModularForm.rank_eq_one_add_rank_cuspForm, LinearEquiv.rank_eq, CuspForm.discriminantEquiv
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
hk : 3 ≤ k ∧ k < 12
⊢ Membership.mem (γ := Finset ℕ) (Finset.filter Even (Finset.Icc 3 11)) k

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
hk : 3 ≤ k ∧ k < 12
⊢ Membership.mem (γ := Finset ℕ) (Finset.filter Even (Finset.Icc 3 11)) k

Tactic:
have : k ∈ (Finset.Icc 3 11).filter Even := by grind
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
ihn :
  ∀ m < HAdd.hAdd (α := ℕ) 3 1,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even (HAdd.hAdd (α := ℕ) 3 1)
hk : 3 ≤ HAdd.hAdd (α := ℕ) 3 1 ∧ HAdd.hAdd (α := ℕ) 3 1 < 12
⊢ HAdd.hAdd (α := Cardinal.{0}) 1 0 =
    (↑(if HAdd.hAdd (α := ℕ) 3 1 ≡ 2 [MOD 12] then HAdd.hAdd (α := ℕ) 3 1 / 12 else HAdd.hAdd (α := ℕ) 3 1 / 12 + 1) :
      Cardinal.{0})

Tactic:
simp [Nat.ModEq]

Premises used: Nat.ModEq
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
ihn :
  ∀ m < HAdd.hAdd (α := ℕ) 3 1 + 1 + 1,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even (HAdd.hAdd (α := ℕ) 3 1 + 1 + 1)
hk : 3 ≤ HAdd.hAdd (α := ℕ) 3 1 + 1 + 1 ∧ HAdd.hAdd (α := ℕ) 3 1 + 1 + 1 < 12
⊢ HAdd.hAdd (α := Cardinal.{0}) 1 0 =
    (↑(if HAdd.hAdd (α := ℕ) 3 1 + 1 + 1 ≡ 2 [MOD 12] then (HAdd.hAdd (α := ℕ) 3 1 + 1 + 1) / 12
        else (HAdd.hAdd (α := ℕ) 3 1 + 1 + 1) / 12 + 1) :
      Cardinal.{0})

Tactic:
simp [Nat.ModEq]

Premises used: Nat.ModEq
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
ihn :
  ∀ m < HAdd.hAdd (α := ℕ) 3 1 + 1 + 1 + 1 + 1,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even (HAdd.hAdd (α := ℕ) 3 1 + 1 + 1 + 1 + 1)
hk : 3 ≤ HAdd.hAdd (α := ℕ) 3 1 + 1 + 1 + 1 + 1 ∧ HAdd.hAdd (α := ℕ) 3 1 + 1 + 1 + 1 + 1 < 12
⊢ HAdd.hAdd (α := Cardinal.{0}) 1 0 =
    (↑(if HAdd.hAdd (α := ℕ) 3 1 + 1 + 1 + 1 + 1 ≡ 2 [MOD 12] then (HAdd.hAdd (α := ℕ) 3 1 + 1 + 1 + 1 + 1) / 12
        else (HAdd.hAdd (α := ℕ) 3 1 + 1 + 1 + 1 + 1) / 12 + 1) :
      Cardinal.{0})

Tactic:
simp [Nat.ModEq]

Premises used: Nat.ModEq
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
ihn :
  ∀ m < HAdd.hAdd (α := ℕ) 3 1 + 1 + 1 + 1 + 1 + 1 + 1,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even (HAdd.hAdd (α := ℕ) 3 1 + 1 + 1 + 1 + 1 + 1 + 1)
hk : 3 ≤ HAdd.hAdd (α := ℕ) 3 1 + 1 + 1 + 1 + 1 + 1 + 1 ∧ HAdd.hAdd (α := ℕ) 3 1 + 1 + 1 + 1 + 1 + 1 + 1 < 12
⊢ HAdd.hAdd (α := Cardinal.{0}) 1 0 =
    (↑(if HAdd.hAdd (α := ℕ) 3 1 + 1 + 1 + 1 + 1 + 1 + 1 ≡ 2 [MOD 12] then
          (HAdd.hAdd (α := ℕ) 3 1 + 1 + 1 + 1 + 1 + 1 + 1) / 12
        else (HAdd.hAdd (α := ℕ) 3 1 + 1 + 1 + 1 + 1 + 1 + 1) / 12 + 1) :
      Cardinal.{0})

Tactic:
simp [Nat.ModEq]

Premises used: Nat.ModEq
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
hk : 12 ≤ k
⊢ 3 ≤ k

Tactic:
lia
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
hk : 12 ≤ k
⊢ HSub.hSub (α := ℤ) (↑k : ℤ) 12 = (↑(k - 12) : ℤ)

Tactic:
lia
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
hk : 12 ≤ k
⊢ k - 12 < k

Tactic:
lia
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
hk : 12 ≤ k
⊢ Even (k - 12)

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
hk : 12 ≤ k
h :
  HAdd.hAdd (α := Cardinal.{0}) 1 (↑(if k - 12 ≡ 2 [MOD 12] then (k - 12) / 12 else (k - 12) / 12 + 1) : Cardinal.{0}) =
    (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
    (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})

Tactic:
rw [rank_eq_one_add_rank_cuspForm (by lia) hk2, CuspForm.discriminantEquiv.rank_eq,
      show ((k : ℤ) - 12 : ℤ) = ((k - 12 : ℕ) : ℤ) by lia,
      ihn (k - 12) (by lia) (by grind)]

Premises used: HSub.hSub, ModularForm.rank_eq_one_add_rank_cuspForm, LinearEquiv.rank_eq, CuspForm.discriminantEquiv, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
hk : 12 ≤ k
⊢ k / 12 = (k - 12) / 12 + 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
hk : 12 ≤ k
⊢ (k - 12) % 12 = k % 12

Tactic:
lia
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
hk : 12 ≤ k
h :
  HAdd.hAdd (α := Cardinal.{0}) 1
      (↑(if k % 12 = HMod.hMod (α := ℕ) 2 12 then (k - 12) / 12 else (k - 12) / 12 + 1) : Cardinal.{0}) =
    (↑(if k % 12 = HMod.hMod (α := ℕ) 2 12 then (k - 12) / 12 + 1 else (k - 12) / 12 + 1 + 1) : Cardinal.{0})
⊢ HAdd.hAdd (α := Cardinal.{0}) 1 (↑(if k - 12 ≡ 2 [MOD 12] then (k - 12) / 12 else (k - 12) / 12 + 1) : Cardinal.{0}) =
    (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})

Tactic:
simp only [Nat.ModEq, show k / 12 = (k - 12) / 12 + 1 by lia,
      show (k - 12) % 12 = k % 12 by lia]

Premises used: Nat.ModEq
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
hk : 12 ≤ k
pos :
  k % 12 = HMod.hMod (α := ℕ) 2 12 →
    HAdd.hAdd (α := Cardinal.{0}) 1 (↑((k - 12) / 12) : Cardinal.{0}) = (↑((k - 12) / 12 + 1) : Cardinal.{0})
neg :
  ¬k % 12 = HMod.hMod (α := ℕ) 2 12 →
    HAdd.hAdd (α := Cardinal.{0}) 1 (↑((k - 12) / 12 + 1) : Cardinal.{0}) = (↑((k - 12) / 12 + 1 + 1) : Cardinal.{0})
⊢ HAdd.hAdd (α := Cardinal.{0}) 1
      (↑(if k % 12 = HMod.hMod (α := ℕ) 2 12 then (k - 12) / 12 else (k - 12) / 12 + 1) : Cardinal.{0}) =
    (↑(if k % 12 = HMod.hMod (α := ℕ) 2 12 then (k - 12) / 12 + 1 else (k - 12) / 12 + 1 + 1) : Cardinal.{0})

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
hk : 12 ≤ k
h : k % 12 = HMod.hMod (α := ℕ) 2 12
⊢ HAdd.hAdd (α := Cardinal.{0}) 1 (↑((k - 12) / 12) : Cardinal.{0}) = (↑((k - 12) / 12 + 1) : Cardinal.{0})

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
ihn :
  ∀ m < k,
    ∀ (hk2 : Even m),
      Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
        (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0})
hk2 : Even k
hk : 12 ≤ k
h : ¬k % 12 = HMod.hMod (α := ℕ) 2 12
⊢ HAdd.hAdd (α := Cardinal.{0}) 1 (↑((k - 12) / 12 + 1) : Cardinal.{0}) = (↑((k - 12) / 12 + 1 + 1) : Cardinal.{0})

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
hk2 : Even k
h :
  ∀ (k : ℕ)
    (ihn :
      ∀ m < k,
        ∀ (hk2 : Even m),
          Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)) =
            (↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1) : Cardinal.{0}))
    (hk2 : Even k),
    Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
      (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) =
    (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})

Tactic:
induction k using Nat.strong_induction_on with | h k ihn =>
  have : k < 3 ∨ (3 ≤ k ∧ k < 12) ∨ 12 ≤ k := by grind
  rcases this with hk | hk | hk
  · -- `k < 3`: direct case-by-case check
    interval_cases k
    · simpa using levelOne_weight_zero_rank_one
    · grind
    · simpa [Nat.ModEq] using levelOne_weight_two_rank_zero
  · -- `3 ≤ k < 12`: rank decomposition + the weight `k - 12` space is zero
    rw [rank_eq_one_add_rank_cuspForm hk.1 hk2, CuspForm.discriminantEquiv.rank_eq,
      levelOne_neg_weight_rank_zero (by lia)]
    have : k ∈ (Finset.Icc 3 11).filter Even := by grind
    fin_cases this <;> simp [Nat.ModEq]
  · -- `12 ≤ k`: rank decomposition + induction hypothesis at weight `k - 12`
    rw [rank_eq_one_add_rank_cuspForm (by lia) hk2, CuspForm.discriminantEquiv.rank_eq,
      show ((k : ℤ) - 12 : ℤ) = ((k - 12 : ℕ) : ℤ) by lia,
      ihn (k - 12) (by lia) (by grind)]
    simp only [Nat.ModEq, show k / 12 = (k - 12) / 12 + 1 by lia,
      show (k - 12) % 12 = k % 12 by lia]
    split_ifs <;> grind

Premises used: ModularForm.levelOne_neg_weight_rank_zero, ModularForm.levelOne_weight_zero_rank_one, Nat.ModEq, ModularForm.rank_eq_one_add_rank_cuspForm, LinearEquiv.rank_eq, CuspForm.discriminantEquiv, ModularForm.levelOne_weight_two_rank_zero
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
rw :
  Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) < Cardinal.aleph0
⊢ FiniteDimensional ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k)

Tactic:
rw [FiniteDimensional, ← Module.rank_lt_aleph0_iff]

Premises used: Module.rank_lt_aleph0_iff, FiniteDimensional
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
inl :
  ∀ (hk_neg : k < 0),
    Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) <
      Cardinal.aleph0
inr :
  ∀ (hk_nonneg : 0 ≤ k),
    Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) <
      Cardinal.aleph0
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) < Cardinal.aleph0

Tactic:
rcases lt_or_ge k 0 with hk_neg | hk_nonneg

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
hk_neg : k < 0
inl : 0 < Cardinal.aleph0
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) < Cardinal.aleph0

Tactic:
rw [levelOne_neg_weight_rank_zero hk_neg]

Premises used: ModularForm.levelOne_neg_weight_rank_zero
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
hk_neg : k < 0
⊢ 0 < Cardinal.aleph0

Tactic:
Cardinal.aleph0_pos

Premises used: Cardinal.aleph0_pos
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
hk_neg : k < 0
⊢ 0 < Cardinal.aleph0

Tactic:
exact Cardinal.aleph0_pos

Premises used: Cardinal.aleph0_pos
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
hk_nonneg : 0 ≤ k
inr :
  ∀ (hk_even : Even k),
    Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) <
      Cardinal.aleph0
inr₁ :
  ∀ (hk_odd : Odd k),
    Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) <
      Cardinal.aleph0
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) < Cardinal.aleph0

Tactic:
rcases Int.even_or_odd k with hk_even | hk_odd

Premises used: Int.even_or_odd
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
hk_nonneg : 0 ≤ k
hk_even : Even k
⊢ 0 ≤ k

Tactic:
hk_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
hk_nonneg : 0 ≤ k
hk_even : Even k
inr :
  ∀ (k : ℕ) (hk_even : Even (α := ℤ) (↑k : ℤ)),
    Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) <
      Cardinal.aleph0
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) < Cardinal.aleph0

Tactic:
lift k to ℕ using hk_nonneg