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

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

State before:
tag : Tag
t : Time.From tag.time
⊢ tag < if tag.time < t.val then { time := t.val, microstep := 0 } else increment tag
Tactic:
split
State after:
case inl
tag : Tag
t : Time.From tag.time
h✝ : tag.time < t.val
⊢ tag < { time := t.val, microstep := 0 }

case inr
tag : Tag
t : Time.From tag.time
h✝ : ¬tag.time < t.val
⊢ tag < increment tag

State before:
tag : Tag
t : Time.From tag.time
h✝ : ¬tag.time < t.val
⊢ tag < increment tag
Tactic:
case inr => simp_arith [LT.lt, increment]
State after:
no goals

State before:
tag : Tag
t : Time.From tag.time
h✝ : tag.time < t.val
⊢ tag < { time := t.val, microstep := 0 }
Tactic:
case inl => simp [LT.lt] at *; split <;> simp_all
State after:
no goals

State before:
tag : Tag
t : Time.From tag.time
h✝ : ¬tag.time < t.val
⊢ tag < increment tag
Tactic:
simp_arith [LT.lt, increment]
State after:
no goals

State before:
tag : Tag
t : Time.From tag.time
h✝ : tag.time < t.val
⊢ tag < { time := t.val, microstep := 0 }
Tactic:
simp [LT.lt] at *
State after:
tag : Tag
t : Time.From tag.time
h✝ : tag.time.ns < t.val.ns
⊢ if tag.time = t.val then tag.microstep < 0 else tag.time.ns < t.val.ns

State before:
tag : Tag
t : Time.From tag.time
h✝ : tag.time.ns < t.val.ns
⊢ if tag.time = t.val then tag.microstep < 0 else tag.time.ns < t.val.ns
Tactic:
split <;> simp_all
State after:
no goals