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

State before:
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
⊢ unprocessed s₂ = unprocessed s₁ \ {rcn e}
Tactic:
ext i
State after:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
i : ID
⊢ i ∈ unprocessed s₂ ↔ i ∈ unprocessed s₁ \ {rcn e}

State before:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
i : ID
⊢ i ∈ unprocessed s₂ ↔ i ∈ unprocessed s₁ \ {rcn e}
Tactic:
simp [State.unprocessed, Equivalent.obj?_rcn_eq e.equiv, and_assoc, e.progress_eq]
State after:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
i : ID
⊢ i ∈ s₂.rtr[Component.rcn] → (i ∉ Set.insert (rcn e) s₁.progress ↔ i ∉ s₁.progress ∧ ¬i = rcn e)

State before:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
i : ID
⊢ i ∈ s₂.rtr[Component.rcn] → (i ∉ Set.insert (rcn e) s₁.progress ↔ i ∉ s₁.progress ∧ ¬i = rcn e)
Tactic:
intro _
State after:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
i : ID
a✝ : i ∈ s₂.rtr[Component.rcn]
⊢ i ∉ Set.insert (rcn e) s₁.progress ↔ i ∉ s₁.progress ∧ ¬i = rcn e

State before:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
i : ID
a✝ : i ∈ s₂.rtr[Component.rcn]
⊢ i ∉ Set.insert (rcn e) s₁.progress ↔ i ∉ s₁.progress ∧ ¬i = rcn e
Tactic:
simp [Set.insert]
State after:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
i : ID
a✝ : i ∈ s₂.rtr[Component.rcn]
⊢ ¬(i = rcn e ∨ i ∈ s₁.progress) ↔ i ∉ s₁.progress ∧ ¬i = rcn e

State before:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
i : ID
a✝ : i ∈ s₂.rtr[Component.rcn]
⊢ ¬(i = rcn e ∨ i ∈ s₁.progress) ↔ i ∉ s₁.progress ∧ ¬i = rcn e
Tactic:
push_neg
State after:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
i : ID
a✝ : i ∈ s₂.rtr[Component.rcn]
⊢ i ≠ rcn e ∧ i ∉ s₁.progress ↔ i ∉ s₁.progress ∧ i ≠ rcn e

State before:
case h
α : Type
inst✝ : Hierarchical α
s₁ s₂ : State α
e : s₁ ↓ₑ s₂
i : ID
a✝ : i ∈ s₂.rtr[Component.rcn]
⊢ i ≠ rcn e ∧ i ∉ s₁.progress ↔ i ∉ s₁.progress ∧ i ≠ rcn e
Tactic:
simp [and_comm]
State after:
no goals