Theorem: Execution.Grouped.Steps.tag_le (ReactorModel/Execution/Theorems/Grouped/Steps.lean)

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : Steps s₁ s₂
⊢ s₁.tag ≤ s₂.tag
Tactic:
induction e
State after:
case refl
α : Type
inst✝ : Hierarchical α
s₁ s₂ s✝ : State α
⊢ s✝.tag ≤ s✝.tag

case step
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝¹ : Step s₁✝ s₂✝
a✝ : Steps s₂✝ s₃✝
a_ih✝ : s₂✝.tag ≤ s₃✝.tag
⊢ s₁✝.tag ≤ s₃✝.tag

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s✝ : State α
⊢ s✝.tag ≤ s✝.tag
Tactic:
case refl => rfl
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
e : Step s₁✝ s₂✝
a✝ : Steps s₂✝ s₃✝
hi : s₂✝.tag ≤ s₃✝.tag
⊢ s₁✝.tag ≤ s₃✝.tag
Tactic:
case step e _ hi => exact le_trans e.tag_le hi
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s✝ : State α
⊢ s✝.tag ≤ s✝.tag
Tactic:
rfl
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
e : Step s₁✝ s₂✝
a✝ : Steps s₂✝ s₃✝
hi : s₂✝.tag ≤ s₃✝.tag
⊢ s₁✝.tag ≤ s₃✝.tag
Tactic:
exact le_trans e.tag_le hi
State after:
no goals