Theorem: Execution.Step.Exec.not_trivial (ReactorModel/Execution/Theorems/Trivial.lean)

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e : s₁ ↓ₑ s₂
⊢ ¬State.Trivial s₁
Tactic:
by_contra ht
State after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e : s₁ ↓ₑ s₂
ht : State.Trivial s₁
⊢ False

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e : s₁ ↓ₑ s₂
ht : State.Trivial s₁
⊢ False
Tactic:
simp [State.Trivial, Partial.empty_iff] at ht
State after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e : s₁ ↓ₑ s₂
ht : ∀ (a : Component.idType Component.rcn), s₁.rtr[Component.rcn][a] = none
⊢ False

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e : s₁ ↓ₑ s₂
ht : ∀ (a : Component.idType Component.rcn), s₁.rtr[Component.rcn][a] = none
⊢ False
Tactic:
cases (Partial.mem_iff.mp e.allows_rcn.mem).choose_spec ▸ ht e.rcn
State after:
no goals