Theorem: Execution.State.NextTag.isLeast (ReactorModel/Execution/Theorems/State.lean)

State before:
α : Type
inst✝ : Hierarchical α
s✝ s₁ s₂ : State α
g : Time.Tag
s : State α
n : NextTag s g
⊢ g ∈ lowerBounds {g' | g' ∈ scheduledTags s ∧ s.tag < g'}
Tactic:
simp [lowerBounds]
State after:
α : Type
inst✝ : Hierarchical α
s✝ s₁ s₂ : State α
g : Time.Tag
s : State α
n : NextTag s g
⊢ ∀ ⦃a : Time.Tag⦄, a ∈ scheduledTags s → s.tag < a → g ≤ a

State before:
α : Type
inst✝ : Hierarchical α
s✝ s₁ s₂ : State α
g : Time.Tag
s : State α
n : NextTag s g
⊢ ∀ ⦃a : Time.Tag⦄, a ∈ scheduledTags s → s.tag < a → g ≤ a
Tactic:
exact n.least
State after:
no goals