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

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
e : s₁ ↓ᵢ+ s₂
⊢ rcn ∈ rcns e ↔ rcn ∈ s₂.progress ∧ rcn ∉ s₁.progress
Tactic:
simp [e.progress_eq, or_and_right]
State after:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
e : s₁ ↓ᵢ+ s₂
⊢ rcn ∈ rcns e → rcn ∉ s₁.progress

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
rcn : ID
e : s₁ ↓ᵢ+ s₂
⊢ rcn ∈ rcns e → rcn ∉ s₁.progress
Tactic:
exact e.mem_rcns_not_mem_progress
State after:
no goals