Theorem: Execution.State.Over.exists_unprocessed_of_not_closed (ReactorModel/Execution/Theorems/StateOver.lean)

State before:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr rtr₁ : α
s : State.Over rtr
hc : ¬Closed s.toState
⊢ ∃ i ∈ s.rtr[Component.rcn], i ∉ s.progress
Tactic:
have ⟨i, _, _⟩ := Set.exists_of_ssubset $ s.progress_ssubset_of_not_closed hc
State after:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr rtr₁ : α
s : State.Over rtr
hc : ¬Closed s.toState
i : ID
left✝ : i ∈ Partial.ids (s.rtr[Component.rcn])
right✝ : i ∉ s.progress
⊢ ∃ i ∈ s.rtr[Component.rcn], i ∉ s.progress

State before:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr rtr₁ : α
s : State.Over rtr
hc : ¬Closed s.toState
i : ID
left✝ : i ∈ Partial.ids (s.rtr[Component.rcn])
right✝ : i ∉ s.progress
⊢ ∃ i ∈ s.rtr[Component.rcn], i ∉ s.progress
Tactic:
exists i
State after:
no goals