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

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
e : s₁ ↓ᵢ+ s₂
hm : i ∈ rcns e
hr : rcns e ≮[s₁.rtr] i
⊢ ∃ e', rcns e' = i :: List.erase (rcns e) i
Tactic:
cases e <;> (simp [rcns] at *; try cases ‹_ ∨ _›)
State after:
case single
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
a✝ : s₁ ↓ᵢ s₂
hr : [rcn a✝] ≮[s₁.rtr] i
hm : i = rcn a✝
⊢ ∃ e', rcns e' = i :: List.erase [rcn a✝] i

case trans.inl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
hr : rcn a✝¹ :: rcns a✝ ≮[s₁.rtr] i
h✝ : i = rcn a✝¹
⊢ ∃ e', rcns e' = i :: List.erase (rcn a✝¹ :: rcns a✝) i

case trans.inr
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
hr : rcn a✝¹ :: rcns a✝ ≮[s₁.rtr] i
h✝ : i ∈ rcns a✝
⊢ ∃ e', rcns e' = i :: List.erase (rcn a✝¹ :: rcns a✝) i

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
e : s₁ ↓ᵢ s₂
hr : [rcn e] ≮[s₁.rtr] i
hm : i = rcn e
⊢ ∃ e', rcns e' = i :: List.erase [rcn e] i
Tactic:
case single e =>
  exists single e
  simp [hm, rcns]
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i = rcn e
⊢ ∃ e'_1, rcns e'_1 = i :: List.erase (rcn e :: rcns e') i
Tactic:
case trans.inl e e' h =>
  exists trans e e'
  simp [rcns, h]
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i ∈ rcns e'
⊢ ∃ e'_1, rcns e'_1 = i :: List.erase (rcn e :: rcns e') i
Tactic:
case trans.inr e e' h =>
  have h' := e'.rcns.erase_cons_tail <| by simp only [beq_iff_eq]; exact head_not_mem_tail e e' h
  exact h' ▸ cons_prepend_minimal e e' h hr
State after:
no goals

State before:
case trans
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
hm : i ∈ rcns (trans a✝¹ a✝)
hr : rcns (trans a✝¹ a✝) ≮[s₁.rtr] i
⊢ ∃ e', rcns e' = i :: List.erase (rcns (trans a✝¹ a✝)) i
Tactic:
simp [rcns] at *
State after:
case trans
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
hr : rcn a✝¹ :: rcns a✝ ≮[s₁.rtr] i
hm : i = rcn a✝¹ ∨ i ∈ rcns a✝
⊢ ∃ e', rcns e' = i :: List.erase (rcn a✝¹ :: rcns a✝) i

State before:
case trans
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
hr : rcn a✝¹ :: rcns a✝ ≮[s₁.rtr] i
hm : i = rcn a✝¹ ∨ i ∈ rcns a✝
⊢ ∃ e', rcns e' = i :: List.erase (rcn a✝¹ :: rcns a✝) i
Tactic:
try cases ‹_ ∨ _›
State after:
case trans.inl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
hr : rcn a✝¹ :: rcns a✝ ≮[s₁.rtr] i
h✝ : i = rcn a✝¹
⊢ ∃ e', rcns e' = i :: List.erase (rcn a✝¹ :: rcns a✝) i

case trans.inr
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
hr : rcn a✝¹ :: rcns a✝ ≮[s₁.rtr] i
h✝ : i ∈ rcns a✝
⊢ ∃ e', rcns e' = i :: List.erase (rcn a✝¹ :: rcns a✝) i

State before:
case trans
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
hr : rcn a✝¹ :: rcns a✝ ≮[s₁.rtr] i
hm : i = rcn a✝¹ ∨ i ∈ rcns a✝
⊢ ∃ e', rcns e' = i :: List.erase (rcn a✝¹ :: rcns a✝) i
Tactic:
cases ‹_ ∨ _›
State after:
case trans.inl
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
hr : rcn a✝¹ :: rcns a✝ ≮[s₁.rtr] i
h✝ : i = rcn a✝¹
⊢ ∃ e', rcns e' = i :: List.erase (rcn a✝¹ :: rcns a✝) i

case trans.inr
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
a✝¹ : s₁ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₂
hr : rcn a✝¹ :: rcns a✝ ≮[s₁.rtr] i
h✝ : i ∈ rcns a✝
⊢ ∃ e', rcns e' = i :: List.erase (rcn a✝¹ :: rcns a✝) i

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
e : s₁ ↓ᵢ s₂
hr : [rcn e] ≮[s₁.rtr] i
hm : i = rcn e
⊢ ∃ e', rcns e' = i :: List.erase [rcn e] i
Tactic:
exists single e
State after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
e : s₁ ↓ᵢ s₂
hr : [rcn e] ≮[s₁.rtr] i
hm : i = rcn e
⊢ rcns (single e) = i :: List.erase [rcn e] i

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
e : s₁ ↓ᵢ s₂
hr : [rcn e] ≮[s₁.rtr] i
hm : i = rcn e
⊢ rcns (single e) = i :: List.erase [rcn e] i
Tactic:
simp [hm, rcns]
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i = rcn e
⊢ ∃ e'_1, rcns e'_1 = i :: List.erase (rcn e :: rcns e') i
Tactic:
exists trans e e'
State after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i = rcn e
⊢ rcns (trans e e') = i :: List.erase (rcn e :: rcns e') i

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i = rcn e
⊢ rcns (trans e e') = i :: List.erase (rcn e :: rcns e') i
Tactic:
simp [rcns, h]
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i ∈ rcns e'
⊢ ∃ e'_1, rcns e'_1 = i :: List.erase (rcn e :: rcns e') i
Tactic:
have h' := e'.rcns.erase_cons_tail <| by simp only [beq_iff_eq]; exact head_not_mem_tail e e' h
State after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i ∈ rcns e'
h' : List.erase (rcn e :: rcns e') i = rcn e :: List.erase (rcns e') i
⊢ ∃ e'_1, rcns e'_1 = i :: List.erase (rcn e :: rcns e') i

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i ∈ rcns e'
h' : List.erase (rcn e :: rcns e') i = rcn e :: List.erase (rcns e') i
⊢ ∃ e'_1, rcns e'_1 = i :: List.erase (rcn e :: rcns e') i
Tactic:
exact h' ▸ cons_prepend_minimal e e' h hr
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i ∈ rcns e'
⊢ ¬(?m.91125 == ?m.91124) = true
Tactic:
simp only [beq_iff_eq]
State after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i ∈ rcns e'
⊢ ¬?m.91125 = ?m.91124

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
i : ID
s₂✝ : State α
e : s₁ ↓ᵢ s₂✝
e' : s₂✝ ↓ᵢ+ s₂
hr : rcn e :: rcns e' ≮[s₁.rtr] i
h : i ∈ rcns e'
⊢ ¬?m.91125 = ?m.91124
Tactic:
exact head_not_mem_tail e e' h
State after:
no goals