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

State before:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr✝ rtr₁ : α
s : State.Over rtr✝
rtr : α
rcn : ID
h : rcn ∈ rtr[Component.rcn]
⊢ ¬Closed (forcing rtr rcn).toState
Tactic:
simp [State.Closed, forcing]
State after:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr✝ rtr₁ : α
s : State.Over rtr✝
rtr : α
rcn : ID
h : rcn ∈ rtr[Component.rcn]
⊢ rcn ∈ Partial.ids (rtr[Component.rcn])

State before:
α : Type
inst✝¹ : Hierarchical α
inst✝ : Reactor.Finite α
rtr✝ rtr₁ : α
s : State.Over rtr✝
rtr : α
rcn : ID
h : rcn ∈ rtr[Component.rcn]
⊢ rcn ∈ Partial.ids (rtr[Component.rcn])
Tactic:
exact h
State after:
no goals