Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case h.inr.inl.«0»
ihn :
  ∀ m < 3 + 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 (3 + 1)
hk : 3 ≤ 3 + 1 ∧ 3 + 1 < 12
⊢ 1 + 0 = ↑(if 3 + 1 ≡ 2 [MOD 12] then (3 + 1) / 12 else (3 + 1) / 12 + 1)

pp: case h.inr.inl.«1»
ihn :
  ∀ m < 3 + 1 + 1 + 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 (3 + 1 + 1 + 1)
hk : 3 ≤ 3 + 1 + 1 + 1 ∧ 3 + 1 + 1 + 1 < 12
⊢ 1 + 0 = ↑(if 3 + 1 + 1 + 1 ≡ 2 [MOD 12] then (3 + 1 + 1 + 1) / 12 else (3 + 1 + 1 + 1) / 12 + 1)

pp: case h.inr.inl.«2»
ihn :
  ∀ m < 3 + 1 + 1 + 1 + 1 + 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 (3 + 1 + 1 + 1 + 1 + 1)
hk : 3 ≤ 3 + 1 + 1 + 1 + 1 + 1 ∧ 3 + 1 + 1 + 1 + 1 + 1 < 12
⊢ 1 + 0 =
    ↑(if 3 + 1 + 1 + 1 + 1 + 1 ≡ 2 [MOD 12] then (3 + 1 + 1 + 1 + 1 + 1) / 12 else (3 + 1 + 1 + 1 + 1 + 1) / 12 + 1)

pp: case h.inr.inl.«3»
ihn :
  ∀ m < 3 + 1 + 1 + 1 + 1 + 1 + 1 + 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 (3 + 1 + 1 + 1 + 1 + 1 + 1 + 1)
hk : 3 ≤ 3 + 1 + 1 + 1 + 1 + 1 + 1 + 1 ∧ 3 + 1 + 1 + 1 + 1 + 1 + 1 + 1 < 12
⊢ 1 + 0 =
    ↑(if 3 + 1 + 1 + 1 + 1 + 1 + 1 + 1 ≡ 2 [MOD 12] then (3 + 1 + 1 + 1 + 1 + 1 + 1 + 1) / 12
      else (3 + 1 + 1 + 1 + 1 + 1 + 1 + 1) / 12 + 1)

Tactic:
<;>

Goal state after:
case h.inr.inl.«0»
ihn :
  ∀ m < 3 + 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 (3 + 1)
hk : 3 ≤ 3 + 1 ∧ 3 + 1 < 12
⊢ 1 + 0 = ↑(if 3 + 1 ≡ 2 [MOD 12] then (3 + 1) / 12 else (3 + 1) / 12 + 1)

case h.inr.inl.«1»
ihn :
  ∀ m < 3 + 1 + 1 + 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 (3 + 1 + 1 + 1)
hk : 3 ≤ 3 + 1 + 1 + 1 ∧ 3 + 1 + 1 + 1 < 12
⊢ 1 + 0 = ↑(if 3 + 1 + 1 + 1 ≡ 2 [MOD 12] then (3 + 1 + 1 + 1) / 12 else (3 + 1 + 1 + 1) / 12 + 1)

case h.inr.inl.«2»
ihn :
  ∀ m < 3 + 1 + 1 + 1 + 1 + 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 (3 + 1 + 1 + 1 + 1 + 1)
hk : 3 ≤ 3 + 1 + 1 + 1 + 1 + 1 ∧ 3 + 1 + 1 + 1 + 1 + 1 < 12
⊢ 1 + 0 =
    ↑(if 3 + 1 + 1 + 1 + 1 + 1 ≡ 2 [MOD 12] then (3 + 1 + 1 + 1 + 1 + 1) / 12 else (3 + 1 + 1 + 1 + 1 + 1) / 12 + 1)

case h.inr.inl.«3»
ihn :
  ∀ m < 3 + 1 + 1 + 1 + 1 + 1 + 1 + 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 (3 + 1 + 1 + 1 + 1 + 1 + 1 + 1)
hk : 3 ≤ 3 + 1 + 1 + 1 + 1 + 1 + 1 + 1 ∧ 3 + 1 + 1 + 1 + 1 + 1 + 1 + 1 < 12
⊢ 1 + 0 =
    ↑(if 3 + 1 + 1 + 1 + 1 + 1 + 1 + 1 ≡ 2 [MOD 12] then (3 + 1 + 1 + 1 + 1 + 1 + 1 + 1) / 12
      else (3 + 1 + 1 + 1 + 1 + 1 + 1 + 1) / 12 + 1)