Theorem: Tag.advance_time (Runtime/Time.lean)

State before:
tag : Tag
time : Time.From tag.time
⊢ (advance tag time).time = time.val
Tactic:
simp [advance]
State after:
tag : Tag
time : Time.From tag.time
⊢ (if tag.time < time.val then { time := time.val, microstep := 0 } else increment tag).time = time.val

State before:
tag : Tag
time : Time.From tag.time
⊢ (if tag.time < time.val then { time := time.val, microstep := 0 } else increment tag).time = time.val
Tactic:
split <;> simp
State after:
case inr
tag : Tag
time : Time.From tag.time
h✝ : ¬tag.time < time.val
⊢ (increment tag).time = time.val

State before:
tag : Tag
time : Time.From tag.time
h : ¬tag.time < time.val
⊢ (increment tag).time = time.val
Tactic:
case _ h => simp_arith [LT.lt] at h; exact Time.le_antisymm time.property h
State after:
no goals

State before:
tag : Tag
time : Time.From tag.time
h : ¬tag.time < time.val
⊢ (increment tag).time = time.val
Tactic:
simp_arith [LT.lt] at h
State after:
tag : Tag
time : Time.From tag.time
h : time.val.ns ≤ tag.time.ns
⊢ (increment tag).time = time.val

State before:
tag : Tag
time : Time.From tag.time
h : time.val.ns ≤ tag.time.ns
⊢ (increment tag).time = time.val
Tactic:
exact Time.le_antisymm time.property h
State after:
no goals