Theorem: Execution.State.Closed.progress_nonempty (ReactorModel/Execution/Theorems/State.lean)

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
n : Nontrivial s
h : Closed s
⊢ Set.Nonempty s.progress
Tactic:
simp_all [Closed, ←Partial.Nonempty.iff_ids_nonempty]
State after:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
n : Nontrivial s
h : s.progress = Partial.ids (s.rtr[Component.rcn])
⊢ Partial.Nonempty (s.rtr[Component.rcn])

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
n : Nontrivial s
h : s.progress = Partial.ids (s.rtr[Component.rcn])
⊢ Partial.Nonempty (s.rtr[Component.rcn])
Tactic:
exact n
State after:
no goals