Theorem: Execution.Grouped.Tail.closed_to_none (ReactorModel/Execution/Theorems/Grouped/Tail.lean)

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
h : State.Closed s₁
e : Tail s₁ s₂
⊢ s₁ = s₂
Tactic:
cases e
State after:
case none
α : Type
inst✝ : Hierarchical α
s₁ : State α
h : State.Closed s₁
⊢ s₁ = s₁

case some
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
h : State.Closed s₁
a✝ : s₁ ↓ᵢ+ s₂
⊢ s₁ = s₂

State before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
h : State.Closed s₁
⊢ s₁ = s₁
Tactic:
case none => rfl
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
h : State.Closed s₁
e : s₁ ↓ᵢ+ s₂
⊢ s₁ = s₂
Tactic:
case some e => exact absurd h e.not_closed
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ : State α
h : State.Closed s₁
⊢ s₁ = s₁
Tactic:
rfl
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
h : State.Closed s₁
e : s₁ ↓ᵢ+ s₂
⊢ s₁ = s₂
Tactic:
exact absurd h e.not_closed
State after:
no goals