awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
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})
⊢ 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})
have 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})
Tactic: interval_cases k
Cleared hypotheses: ihn, hk2, hk
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
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})
⊢ 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})
have 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})
Tactic: interval_cases k
Cleared hypotheses: ihn, hk2, hk
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
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
⊢ 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})
have h : HAdd.hAdd (α := Cardinal.{0}) 1 0 = (↑(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)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (hypothesis)
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
⊢ HAdd.hAdd (α := Cardinal.{0}) 1 0 = (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})
have this : Membership.mem (γ := Finset ℕ) (Finset.filter Even (Finset.Icc 3 11)) k
Tactic: have : k ∈ (Finset.Icc 3 11).filter Even := by grind
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
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
this : Membership.mem (γ := Finset ℕ) (Finset.filter Even (Finset.Icc 3 11)) k
⊢ HAdd.hAdd (α := Cardinal.{0}) 1 0 = (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})
have h : ∀
  (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: fin_cases this
Cleared hypotheses: k, ihn, hk2, hk, this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
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
this : Membership.mem (γ := Finset ℕ) (Finset.filter Even (Finset.Icc 3 11)) k
h :
  ∀
    (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})
⊢ HAdd.hAdd (α := Cardinal.{0}) 1 0 = (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})
have h₁ : ∀
  (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: fin_cases this
Cleared hypotheses: k, ihn, hk2, hk, this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
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
this : Membership.mem (γ := Finset ℕ) (Finset.filter Even (Finset.Icc 3 11)) k
h :
  ∀
    (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})
h₁ :
  ∀
    (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})
⊢ HAdd.hAdd (α := Cardinal.{0}) 1 0 = (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0})
have h₂ : ∀
  (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: fin_cases this
Cleared hypotheses: k, ihn, hk2, hk, this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
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
⊢ 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})
have 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})
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)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
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
⊢ 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})
have 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})
Tactic: simp only [Nat.ModEq, show k / 12 = (k - 12) / 12 + 1 by lia,
      show (k - 12) % 12 = k % 12 by lia]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
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
⊢ 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})
have pos : k % 12 = HMod.hMod (α := ℕ) 2 12 →
  HAdd.hAdd (α := Cardinal.{0}) 1 (↑((k - 12) / 12) : Cardinal.{0}) = (↑((k - 12) / 12 + 1) : Cardinal.{0})
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
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})
⊢ 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})
have 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})
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℕ
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})
have 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})
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
Cleared hypotheses: k, hk2
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
⊢ FiniteDimensional ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k)
have rw : Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) < Cardinal.aleph0
Tactic: rw [FiniteDimensional, ← Module.rank_lt_aleph0_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) < Cardinal.aleph0
have inl : ∀ (hk_neg : k < 0),
  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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
inl :
  ∀ (hk_neg : k < 0),
    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
have inr : ∀ (hk_nonneg : 0 ≤ k),
  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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
hk_neg : k < 0
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) < Cardinal.aleph0
have inl : 0 < Cardinal.aleph0
Tactic: rw [levelOne_neg_weight_rank_zero hk_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
hk_nonneg : 0 ≤ k
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) < Cardinal.aleph0
have inr : ∀ (hk_even : Even k),
  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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
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
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) < Cardinal.aleph0
have inr₁ : ∀ (hk_odd : Odd k),
  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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
hk_nonneg : 0 ≤ k
hk_even : Even k
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) < Cardinal.aleph0
have inr : ∀ (k : ℕ) (hk_even : Even (α := ℤ) (↑k : ℤ)),
  Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) <
    Cardinal.aleph0
Tactic: lift k to ℕ using hk_nonneg
Cleared hypotheses: k, hk_nonneg, hk_even
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℕ
hk_even : Even (α := ℤ) (↑k : ℤ)
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) <
    Cardinal.aleph0
have inr : (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0}) < Cardinal.aleph0
Tactic: rw [dimension_level_one k (mod_cast hk_even)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℕ
hk_even : Even (α := ℤ) (↑k : ℤ)
⊢ (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0}) < Cardinal.aleph0
have pos : k ≡ 2 [MOD 12] → (↑(k / 12) : Cardinal.{0}) < Cardinal.aleph0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℕ
hk_even : Even (α := ℤ) (↑k : ℤ)
pos : k ≡ 2 [MOD 12] → (↑(k / 12) : Cardinal.{0}) < Cardinal.aleph0
⊢ (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0}) < Cardinal.aleph0
have neg : ¬k ≡ 2 [MOD 12] → (↑(k / 12 + 1) : Cardinal.{0}) < Cardinal.aleph0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
hk_nonneg : 0 ≤ k
hk_odd : Odd k
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) < Cardinal.aleph0
have inr : 0 < Cardinal.aleph0
Tactic: rw [levelOne_odd_weight_rank_zero hk_odd]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (hypothesis)
Goal:
k : ℕ
ih :
  ∀ m < k,
    ∀ {f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)}
      (h : (↑(m / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order), f = 0
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)
h : (↑(k / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order
⊢ f = 0
have h0 : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
Tactic: have h0 : (qExpansion 1 f).coeff 0 = 0 :=
    PowerSeries.coeff_of_lt_order _ ((Nat.cast_nonneg _).trans_lt h)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℕ
ih :
  ∀ m < k,
    ∀ {f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑m : ℤ)}
      (h : (↑(m / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order), f = 0
f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)
h : (↑(k / 12) : ℕ∞) < (qExpansion 1 (⇑f : (a : ℍ) → ℂ)).order
h0 : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
⊢ f = 0
have h₁ : Eq (α :=
  ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (HSub.hSub (α := ℤ) (↑k : ℤ) 12))
  ((CuspForm.discriminantEquiv :
        (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (↑k : ℤ)) →
          ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ((↑k : ℤ) - 12))
      (f.toCuspForm h0) :
    ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (HSub.hSub (α := ℤ) (↑k : ℤ) 12))
  (0 :
    ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (HSub.hSub (α := ℤ) (↑k : ℤ) 12))
Tactic: suffices CuspForm.discriminantEquiv (toCuspForm f h0) = 0 by
    simpa [CuspForm.discriminantEquiv.map_eq_zero_iff, DFunLike.ext_iff]