Theorem: Execution.Step.Time.RTC.tag_le (ReactorModel/Execution/Theorems/Trivial.lean)

State before:
α : Type
inst✝ : Proper α
s₁ s₂ : State α
e : RTC s₁ s₂
⊢ s₁.tag ≤ s₂.tag
Tactic:
induction e with
| refl         => exact le_refl _
| trans a _ hi => exact le_trans (le_of_lt a.tag_lt) hi
State after:
no goals

State before:
case refl
α : Type
inst✝ : Proper α
s₁ s₂ s✝ : State α
⊢ s✝.tag ≤ s✝.tag
Tactic:
exact le_refl _
State after:
no goals

State before:
case trans
α : Type
inst✝ : Proper α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a : s₁✝ ↓ₜ s₂✝
a✝ : RTC s₂✝ s₃✝
hi : s₂✝.tag ≤ s₃✝.tag
⊢ s₁✝.tag ≤ s₃✝.tag
Tactic:
exact le_trans (le_of_lt a.tag_lt) hi
State after:
no goals