have ⟨i, _, _⟩ := Set.exists_of_ssubset $ s.progress_ssubset_of_not_closed hc
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr rtr₁ : α
s : State.Over rtr
hc : ¬Closed s.toState
⊢ ∃ i ∈ s.rtr[Component.rcn], i ∉ s.progress
α : 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