-- Mathlib/.lake/packages/lean4/src/lean/Std/Time/Date/Unit/Month.lean
theorem cumulativeDays_le (leap : Bool) (month : Month.Ordinal) : cumulativeDays leap month ≥ 0 ∧ cumulativeDays leap month ≤ 334 + (if leap then 1 else 0)

Proof state:
leap : Bool
month : Ordinal
property✝ : 1 ≤ 12 ∧ 12 ≤ 12
⊢ (0 ≤ [0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334][↑11] + if leap = true then 1 else 0) ∧
    ([0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334][↑11] + if leap = true then 1 else 0) ≤
      334 + if leap = true then 1 else 0

Tactic:
try split

Result:
case isTrue
leap : Bool
month : Ordinal
property✝ : 1 ≤ 12 ∧ 12 ≤ 12
h✝ : leap = true
⊢ 0 ≤ [0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334][↑11] + 1 ∧
    [0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334][↑11] + 1 ≤ 334 + 1

case isFalse
leap : Bool
month : Ordinal
property✝ : 1 ≤ 12 ∧ 12 ≤ 12
h✝ : ¬leap = true
⊢ 0 ≤ [0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334][↑11] + 0 ∧
    [0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334][↑11] + 0 ≤ 334 + 0

Proof state:
case isFalse
leap : Bool
month : Ordinal
property✝ : 1 ≤ 12 ∧ 12 ≤ 12
h✝ : ¬leap = true
⊢ 0 ≤ [0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334][↑11] + 0 ∧
    [0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334][↑11] + 0 ≤ 334 + 0

Tactic:
decide +revert

Result:
no goals

Proof state:
leap : Bool
month : Ordinal
property✝ : 1 ≤ 12 ∧ 12 ≤ 12
⊢ cumulativeDays leap ⟨12, property✝⟩ ≥ 0 ∧ cumulativeDays leap ⟨12, property✝⟩ ≤ 334 + if leap = true then 1 else 0

Tactic:
simp [cumulativeSizes, Bounded.LE.sub, Bounded.LE.add, Bounded.LE.toFin, cumulativeDays]

Result:
leap : Bool
month : Ordinal
property✝ : 1 ≤ 12 ∧ 12 ≤ 12
⊢ (0 ≤ [0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334][↑11] + if leap = true then 1 else 0) ∧
    ([0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334][↑11] + if leap = true then 1 else 0) ≤
      334 + if leap = true then 1 else 0

Proof state:
leap : Bool
month : Ordinal
property✝ : 1 ≤ 12 ∧ 12 ≤ 12
⊢ (0 ≤ [0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334][↑11] + if leap = true then 1 else 0) ∧
    ([0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334][↑11] + if leap = true then 1 else 0) ≤
      334 + if leap = true then 1 else 0

Tactic:
split

Result:
case isTrue
leap : Bool
month : Ordinal
property✝ : 1 ≤ 12 ∧ 12 ≤ 12
h✝ : leap = true
⊢ 0 ≤ [0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334][↑11] + 1 ∧
    [0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334][↑11] + 1 ≤ 334 + 1

case isFalse
leap : Bool
month : Ordinal
property✝ : 1 ≤ 12 ∧ 12 ≤ 12
h✝ : ¬leap = true
⊢ 0 ≤ [0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334][↑11] + 0 ∧
    [0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334][↑11] + 0 ≤ 334 + 0

Proof state:
case isTrue
leap : Bool
month : Ordinal
property✝ : 1 ≤ 12 ∧ 12 ≤ 12
h✝ : leap = true
⊢ 0 ≤ [0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334][↑11] + 1 ∧
    [0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334][↑11] + 1 ≤ 334 + 1

case isFalse
leap : Bool
month : Ordinal
property✝ : 1 ≤ 12 ∧ 12 ≤ 12
h✝ : ¬leap = true
⊢ 0 ≤ [0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334][↑11] + 0 ∧
    [0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334][↑11] + 0 ≤ 334 + 0

Tactic:
all_goals decide +revert

Result:
no goals

Proof state:
leap : Bool
month : Ordinal
⊢ cumulativeDays leap month ≥ 0 ∧ cumulativeDays leap month ≤ 334 + if leap = true then 1 else 0

Tactic:
match month with
| ⟨1, _⟩ | ⟨2, _⟩ | ⟨3, _⟩  | ⟨4, _⟩  | ⟨5, _⟩  | ⟨6, _⟩  | ⟨7, _⟩  | ⟨8, _⟩  | ⟨9, _⟩  | ⟨10, _⟩  | ⟨11, _⟩ | ⟨12, _⟩ =>
  simp [cumulativeSizes, Bounded.LE.sub, Bounded.LE.add, Bounded.LE.toFin, cumulativeDays]
  try split
  all_goals decide +revert

Result:
no goals