Theorem: Execution.Instantaneous.Closed.mem_rcns_iff (ReactorModel/Execution/Theorems/Grouped/Instantaneous.lean)

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
rcn : ID
e : s₁ ↓ᵢ| s₂
⊢ rcn ∈ rcns e ↔ rcn ∈ s₁.rtr[Component.rcn] ∧ rcn ∉ s₁.progress
Tactic:
simp [Partial.mem_def, e.progress_def ▸ e.exec.mem_rcns_iff (rcn := rcn)]
State after:
no goals