awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
hk_even : Even (α := ℤ) (↑k : ℤ)
inr : (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0}) < Cardinal.aleph0
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑k : ℤ)) <
    Cardinal.aleph0

Tactic:
rw [dimension_level_one k (mod_cast hk_even)]

Premises used: cast, ModularForm.dimension_level_one, Int.even_coe_nat._simp_1
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
hk_even : Even (α := ℤ) (↑k : ℤ)
pos : k ≡ 2 [MOD 12] → (↑(k / 12) : Cardinal.{0}) < Cardinal.aleph0
neg : ¬k ≡ 2 [MOD 12] → (↑(k / 12 + 1) : Cardinal.{0}) < Cardinal.aleph0
⊢ (↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1) : Cardinal.{0}) < Cardinal.aleph0

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
hk_even : Even (α := ℤ) (↑k : ℤ)
h : k ≡ 2 [MOD 12]
⊢ (↑(k / 12) : Cardinal.{0}) < Cardinal.aleph0

Tactic:
exact_mod_cast Cardinal.natCast_lt_aleph0

Premises used: Cardinal.natCast_lt_aleph0
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℕ
hk_even : Even (α := ℤ) (↑k : ℤ)
h : ¬k ≡ 2 [MOD 12]
⊢ (↑(k / 12 + 1) : Cardinal.{0}) < Cardinal.aleph0

Tactic:
exact_mod_cast Cardinal.natCast_lt_aleph0

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

Tactic:
rw [levelOne_odd_weight_rank_zero hk_odd]

Premises used: ModularForm.levelOne_odd_weight_rank_zero
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
Goal:
k : ℤ
hk_nonneg : 0 ≤ k
hk_odd : Odd k
⊢ 0 < Cardinal.aleph0

Tactic:
Cardinal.aleph0_pos

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

Tactic:
exact Cardinal.aleph0_pos

Premises used: Cardinal.aleph0_pos
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
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
⊢ 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)
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
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 : ℂ)
this :
  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))
⊢ f = 0

Tactic:
simpa [CuspForm.discriminantEquiv.map_eq_zero_iff, DFunLike.ext_iff]

Premises used: DFunLike.ext_iff, LinearEquiv.map_eq_zero_iff, CuspForm.discriminantEquiv
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
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 : ℂ)
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))
⊢ f = 0

Tactic:
suffices CuspForm.discriminantEquiv (toCuspForm f h0) = 0 by
    simpa [CuspForm.discriminantEquiv.map_eq_zero_iff, DFunLike.ext_iff]
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
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 : ℂ)
h₁ :
  ∀ (hk12 : k < 12),
    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))
h₂ :
  ∀ (hk12 : 12 ≤ k),
    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))
⊢ 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:
rcases lt_or_ge k 12 with hk12 | hk12

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
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 : ℂ)
hk12 : k < 12
⊢ HSub.hSub (α := ℤ) (↑k : ℤ) 12 < 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
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 : ℂ)
hk12 : k < 12
⊢ 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:
apply rank_zero_iff_forall_zero.mp (levelOne_neg_weight_rank_zero (by lia))

Premises used: rank_zero_iff_forall_zero, ModularForm.levelOne_neg_weight_rank_zero, Iff.mp
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
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 : ℂ)
hk12 : 12 ≤ k
⊢ HSub.hSub (α := ℤ) (↑k : ℤ) 12 = (↑(k - 12) : ℤ)

Tactic:
lia
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
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 : ℂ)
hk12 : 12 ≤ k
h₁ :
  Eq (α := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑(k - 12) : ℤ))
    (mcast ⋯
      ((CuspForm.discriminantEquiv :
          (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (↑k : ℤ)) →
            ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ((↑k : ℤ) - 12))
        (f.toCuspForm h0))
      ⋯)
    0
⊢ 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:
rw [← mcast_eq_zero_iff (b := ↑(k - 12)) (by lia) rfl]

Premises used: ModularForm.mcast_eq_zero_iff, rfl
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
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 : ℂ)
hk12 : 12 ≤ k
⊢ k - 12 < k

Tactic:
lia
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
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 : ℂ)
hk12 : 12 ≤ k
h₁ :
  (↑((k - 12) / 12) : ℕ∞) <
    (qExpansion 1
        (⇑(mcast ⋯
              ((CuspForm.discriminantEquiv :
                  (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (↑k : ℤ)) →
                    ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ((↑k : ℤ) - 12))
                (f.toCuspForm h0))
              ⋯) :
          (a : ℍ) → ℂ)).order
⊢ Eq (α := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (↑(k - 12) : ℤ))
    (mcast ⋯
      ((CuspForm.discriminantEquiv :
          (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (↑k : ℤ)) →
            ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ((↑k : ℤ) - 12))
        (f.toCuspForm h0))
      ⋯)
    0

Tactic:
refine ih (k - 12) (by lia) ?_

Premises used: HSub.hSub, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
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 : ℂ)
hk12 : 12 ≤ k
⊢ k / 12 = (k - 12) / 12 + 1

Tactic:
lia
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
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 : ℂ)
hk12 : 12 ≤ k
⊢ k / 12 = (k - 12) / 12 + 1

Tactic:
have hsucc : k / 12 = (k - 12) / 12 + 1 := by lia
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
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 : ℂ)
hk12 : 12 ≤ k
hsucc : k / 12 = (k - 12) / 12 + 1
⊢ HAdd.hAdd (α := ℕ∞) (↑((k - 12) / 12) : ℕ∞) 1 <
    (qExpansion 1
          (⇑((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)) :
            (a : ℍ) → ℂ)).order +
      1

Tactic:
rw [qExpansion_eq_qExpansion_discriminant_mul f h0, PowerSeries.order_mul,
      discriminant_qExpansion_order, add_comm, hsucc, Nat.cast_add, Nat.cast_one] at h

Premises used: ModularForm.qExpansion_eq_qExpansion_discriminant_mul, ModularForm.discriminant_qExpansion_order, add_comm, Nat.cast_add, PowerSeries.order_mul, Nat.cast_one
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
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 : ℂ)
hk12 : 12 ≤ k
hsucc : k / 12 = (k - 12) / 12 + 1
h₁ :
  HAdd.hAdd (α := ℕ∞) (↑((k - 12) / 12) : ℕ∞) 1 <
    (qExpansion 1
          (⇑((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)) :
            (a : ℍ) → ℂ)).order +
      1
⊢ 12 ≤ k

Tactic:
rw [qExpansion_eq_qExpansion_discriminant_mul f h0, PowerSeries.order_mul,
      discriminant_qExpansion_order, add_comm, hsucc, Nat.cast_add, Nat.cast_one] at h

Premises used: ModularForm.qExpansion_eq_qExpansion_discriminant_mul, ModularForm.discriminant_qExpansion_order, add_comm, Nat.cast_add, PowerSeries.order_mul, Nat.cast_one
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
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 : ℂ)
hk12 : 12 ≤ k
hsucc : k / 12 = (k - 12) / 12 + 1
h₁ :
  HAdd.hAdd (α := ℕ∞) (↑((k - 12) / 12) : ℕ∞) 1 <
    (qExpansion 1
          (⇑((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)) :
            (a : ℍ) → ℂ)).order +
      1
hk12₁ : 12 ≤ k
⊢ k / 12 = (k - 12) / 12 + 1

Tactic:
rw [qExpansion_eq_qExpansion_discriminant_mul f h0, PowerSeries.order_mul,
      discriminant_qExpansion_order, add_comm, hsucc, Nat.cast_add, Nat.cast_one] at h

Premises used: ModularForm.qExpansion_eq_qExpansion_discriminant_mul, ModularForm.discriminant_qExpansion_order, add_comm, Nat.cast_add, PowerSeries.order_mul, Nat.cast_one
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
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 : ℤ)
h0 : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
h :
  HAdd.hAdd (α := ℕ∞) (↑((k - 12) / 12) : ℕ∞) 1 <
    (qExpansion 1
          (⇑((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)) :
            (a : ℍ) → ℂ)).order +
      1
hk12 : 12 ≤ k
hsucc : k / 12 = (k - 12) / 12 + 1
⊢ (↑((k - 12) / 12) : ℕ∞) <
    (qExpansion 1
        (⇑(mcast ⋯
              ((CuspForm.discriminantEquiv :
                  (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (↑k : ℤ)) →
                    ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ((↑k : ℤ) - 12))
                (f.toCuspForm h0))
              ⋯) :
          (a : ℍ) → ℂ)).order

Tactic:
(ENat.add_lt_add_iff_right (ENat.coe_ne_top 1)).mp h

Premises used: Iff.mp, ENat.coe_ne_top, OfNat.ofNat, ENat.add_lt_add_iff_right
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
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 : ℤ)
h0 : Eq (α := ℂ) ((PowerSeries.coeff 0 : (a : PowerSeries ℂ) → ℂ) (qExpansion 1 (⇑f : (a : ℍ) → ℂ)) : ℂ) (0 : ℂ)
h :
  HAdd.hAdd (α := ℕ∞) (↑((k - 12) / 12) : ℕ∞) 1 <
    (qExpansion 1
          (⇑((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)) :
            (a : ℍ) → ℂ)).order +
      1
hk12 : 12 ≤ k
hsucc : k / 12 = (k - 12) / 12 + 1
⊢ (↑((k - 12) / 12) : ℕ∞) <
    (qExpansion 1
        (⇑(mcast ⋯
              ((CuspForm.discriminantEquiv :
                  (a : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range (↑k : ℤ)) →
                    ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ((↑k : ℤ) - 12))
                (f.toCuspForm h0))
              ⋯) :
          (a : ℍ) → ℂ)).order

Tactic:
exact (ENat.add_lt_add_iff_right (ENat.coe_ne_top 1)).mp h

Premises used: Iff.mp, ENat.coe_ne_top, OfNat.ofNat, ENat.add_lt_add_iff_right