-- Mathlib/.lake/packages/lean4/src/lean/Std/Time/Date/Unit/Month.lean
theorem difference_eq (p : month.val ≤ 11) :
  let next := month.truncateTop p |>.addTop 1 (by decide)
  (cumulativeDays leap next).val = (cumulativeDays leap month).val + (days leap month).val

Proof state:
leap : Bool
month : Ordinal
property✝ : 1 ≤ 1 ∧ 1 ≤ 12
p : ⟨1, property✝⟩.val ≤ 11
⊢ (Std.Time.Month.Ordinal.cumulativeSizes.val[↑1] + 0).val =
    (Std.Time.Month.Ordinal.cumulativeSizes.val[↑0] + 0).val +
      [31, 28, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31][↑(Fin.cast ⋯ 0)].val

Tactic:
rfl

Result:
no goals

Proof state:
leap : Bool
month : Ordinal
property✝ : 1 ≤ 11 ∧ 11 ≤ 12
p : ⟨11, property✝⟩.val ≤ 11
⊢ (Std.Time.Month.Ordinal.cumulativeSizes.val[↑11] + if leap = true then 1 else 0).val =
    (Std.Time.Month.Ordinal.cumulativeSizes.val[↑10] + if leap = true then 1 else 0).val +
      [31, 28, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31][↑(Fin.cast ⋯ 10)].val

Tactic:
try split <;> rfl

Result:
no goals

Proof state:
leap : Bool
month : Ordinal
property✝ : 1 ≤ 11 ∧ 11 ≤ 12
p : ⟨11, property✝⟩.val ≤ 11
⊢ (Std.Time.Month.Ordinal.cumulativeSizes.val[↑11] + if leap = true then 1 else 0).val =
    (Std.Time.Month.Ordinal.cumulativeSizes.val[↑10] + if leap = true then 1 else 0).val +
      [31, 28, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31][↑(Fin.cast ⋯ 10)].val

Tactic:
split <;> rfl

Result:
no goals

Proof state:
leap : Bool
month : Ordinal
p : month.val ≤ 11
⊢ let next := (Bounded.LE.truncateTop month p).addTop 1 ⋯;
  (cumulativeDays leap next).val = (cumulativeDays leap month).val + (days leap month).val

Tactic:
match month with
| ⟨1, _⟩ | ⟨2, _⟩ | ⟨3, _⟩  | ⟨4, _⟩  | ⟨5, _⟩  | ⟨6, _⟩  | ⟨7, _⟩  | ⟨8, _⟩  | ⟨9, _⟩  | ⟨10, _⟩  | ⟨11, _⟩ =>
  simp [cumulativeDays, Bounded.LE.addTop, days, monthSizesNonLeap];
  try split <;> rfl
  try rfl
| ⟨12, _⟩ => contradiction

Result:
no goals

Proof state:
leap : Bool
month : Ordinal
property✝ : 1 ≤ 11 ∧ 11 ≤ 12
p : ⟨11, property✝⟩.val ≤ 11
⊢ let next := (Bounded.LE.truncateTop ⟨11, property✝⟩ p).addTop 1 ⋯;
  (cumulativeDays leap next).val = (cumulativeDays leap ⟨11, property✝⟩).val + (days leap ⟨11, property✝⟩).val

Tactic:
simp [cumulativeDays, Bounded.LE.addTop, days, monthSizesNonLeap]

Result:
leap : Bool
month : Ordinal
property✝ : 1 ≤ 11 ∧ 11 ≤ 12
p : ⟨11, property✝⟩.val ≤ 11
⊢ (Std.Time.Month.Ordinal.cumulativeSizes.val[↑11] + if leap = true then 1 else 0).val =
    (Std.Time.Month.Ordinal.cumulativeSizes.val[↑10] + if leap = true then 1 else 0).val +
      [31, 28, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31][↑(Fin.cast ⋯ 10)].val

Proof state:
leap : Bool
month : Ordinal
p : month.val ≤ 11
⊢ 1 ≥ 0

Tactic:
decide

Result:
no goals

Proof state:
leap : Bool
month : Ordinal
property✝ : 1 ≤ 12 ∧ 12 ≤ 12
p : ⟨12, property✝⟩.val ≤ 11
⊢ let next := (Bounded.LE.truncateTop ⟨12, property✝⟩ p).addTop 1 ⋯;
  (cumulativeDays leap next).val = (cumulativeDays leap ⟨12, property✝⟩).val + (days leap ⟨12, property✝⟩).val

Tactic:
contradiction

Result:
no goals

Proof state:
leap : Bool
month : Ordinal
property✝ : 1 ≤ 1 ∧ 1 ≤ 12
p : ⟨1, property✝⟩.val ≤ 11
⊢ (Std.Time.Month.Ordinal.cumulativeSizes.val[↑1] + 0).val =
    (Std.Time.Month.Ordinal.cumulativeSizes.val[↑0] + 0).val +
      [31, 28, 31, 30, 31, 30, 31, 31, 30, 31, 30, 31][↑(Fin.cast ⋯ 0)].val

Tactic:
try rfl

Result:
no goals