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

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

case trans
α : Type
inst✝ : Proper α
s s₂ s₃ : State α
i : ID
s₁✝ s₂✝ s₃✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₃✝
a_ih✝ :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂✝),
    i ∈ rcns a✝ → (rcn e :: rcns a✝ ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns a✝) i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn a✝¹ :: rcns a✝ ≮[s₁.rtr] i
hm : i = rcn a✝¹ ∨ i ∈ rcns a✝
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn a✝¹ :: rcns a✝) i

State before:
α : Type
inst✝ : Proper α
s s₂ s₃ : State α
i : ID
s₁✝ s₂✝ : State α
e' : s₁✝ ↓ᵢ s₂✝
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : [rcn e, rcn e'] ≮[s₁.rtr] i
hm : i = rcn e'
⊢ ∃ f, rcns f = i :: rcn e :: List.erase [rcn e'] i
Tactic:
case single e' =>
  have ⟨_, f, f', ⟨hf₁, hf₂⟩⟩ := e.prepend_indep e' $ hm ▸ hr.cons_head
  exists trans f (single f')
  simp [hm, rcns, ←hf₁, ←hf₂]
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i = rcn e' ∨ i ∈ rcns e''
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
case trans s₁ s₂ s₄ e' e'' hi =>
  cases hm
  case inl hm =>
    simp [hm] at hr
    have ⟨_, f, f', ⟨hf₁, hf₂⟩⟩ := e.prepend_indep e' hr.cons_head
    exists trans f $ trans f' e''
    simp [hm, rcns, ←hf₁, ←hf₂]
  case inr hm =>
    have ⟨f, hf⟩ :=  hi e' hm $ hr.cons_tail.equiv e.equiv
    cases f <;> simp [rcns] at hf
    case trans f f'' =>
      have ⟨h₁, h₂⟩ := hf
      have ⟨_, f, f', ⟨hf₁, hf₂⟩⟩ := e.prepend_indep f $ h₁.symm ▸ hr |>.cons_head
      exists trans f $ trans f' f''
      have h₃ := e''.rcns.erase_cons_tail <| by
        simp only [beq_iff_eq]; exact head_not_mem_tail e' e'' hm
      simp [rcns, hf₁, h₁, hf₂, h₂, h₃]
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₂ s₃ : State α
i : ID
s₁✝ s₂✝ : State α
e' : s₁✝ ↓ᵢ s₂✝
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : [rcn e, rcn e'] ≮[s₁.rtr] i
hm : i = rcn e'
⊢ ∃ f, rcns f = i :: rcn e :: List.erase [rcn e'] i
Tactic:
have ⟨_, f, f', ⟨hf₁, hf₂⟩⟩ := e.prepend_indep e' $ hm ▸ hr.cons_head
State after:
α : Type
inst✝ : Proper α
s s₂ s₃ : State α
i : ID
s₁✝ s₂✝ : State α
e' : s₁✝ ↓ᵢ s₂✝
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : [rcn e, rcn e'] ≮[s₁.rtr] i
hm : i = rcn e'
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn e'
hf₂ : rcn f' = rcn e
⊢ ∃ f, rcns f = i :: rcn e :: List.erase [rcn e'] i

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

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

State before:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i = rcn e' ∨ i ∈ rcns e''
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
cases hm
State after:
case inl
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
h✝ : i = rcn e'
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i

case inr
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
h✝ : i ∈ rcns e''
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i

State before:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i = rcn e'
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
case inl hm =>
  simp [hm] at hr
  have ⟨_, f, f', ⟨hf₁, hf₂⟩⟩ := e.prepend_indep e' hr.cons_head
  exists trans f $ trans f' e''
  simp [hm, rcns, ←hf₁, ←hf₂]
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
case inr hm =>
  have ⟨f, hf⟩ :=  hi e' hm $ hr.cons_tail.equiv e.equiv
  cases f <;> simp [rcns] at hf
  case trans f f'' =>
    have ⟨h₁, h₂⟩ := hf
    have ⟨_, f, f', ⟨hf₁, hf₂⟩⟩ := e.prepend_indep f $ h₁.symm ▸ hr |>.cons_head
    exists trans f $ trans f' f''
    have h₃ := e''.rcns.erase_cons_tail <| by
      simp only [beq_iff_eq]; exact head_not_mem_tail e' e'' hm
    simp [rcns, hf₁, h₁, hf₂, h₂, h₃]
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i = rcn e'
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
simp [hm] at hr
State after:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hm : i = rcn e'
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] rcn e'
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i

State before:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hm : i = rcn e'
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] rcn e'
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
have ⟨_, f, f', ⟨hf₁, hf₂⟩⟩ := e.prepend_indep e' hr.cons_head
State after:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hm : i = rcn e'
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] rcn e'
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂
hf₁ : rcn f = rcn e'
hf₂ : rcn f' = rcn e
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i

State before:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hm : i = rcn e'
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] rcn e'
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂
hf₁ : rcn f = rcn e'
hf₂ : rcn f' = rcn e
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
exists trans f $ trans f' e''
State after:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hm : i = rcn e'
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] rcn e'
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂
hf₁ : rcn f = rcn e'
hf₂ : rcn f' = rcn e
⊢ rcns (trans f (trans f' e'')) = i :: rcn e :: List.erase (rcn e' :: rcns e'') i

State before:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hm : i = rcn e'
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] rcn e'
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂
hf₁ : rcn f = rcn e'
hf₂ : rcn f' = rcn e
⊢ rcns (trans f (trans f' e'')) = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
simp [hm, rcns, ←hf₁, ←hf₂]
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
have ⟨f, hf⟩ :=  hi e' hm $ hr.cons_tail.equiv e.equiv
State after:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
f : s₁✝ ↓ᵢ+ s₄
hf : rcns f = i :: rcn e' :: List.erase (rcns e'') i
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i

State before:
α : Type
inst✝ : Proper α
s s₂✝ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
f : s₁✝ ↓ᵢ+ s₄
hf : rcns f = i :: rcn e' :: List.erase (rcns e'') i
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
cases f <;> simp [rcns] at hf
State after:
case trans
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
a✝¹ : s₁✝ ↓ᵢ s₂✝
a✝ : s₂✝ ↓ᵢ+ s₄
hf : rcn a✝¹ = i ∧ rcns a✝ = rcn e' :: List.erase (rcns e'') i
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i

State before:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
case trans f f'' =>
  have ⟨h₁, h₂⟩ := hf
  have ⟨_, f, f', ⟨hf₁, hf₂⟩⟩ := e.prepend_indep f $ h₁.symm ▸ hr |>.cons_head
  exists trans f $ trans f' f''
  have h₃ := e''.rcns.erase_cons_tail <| by
    simp only [beq_iff_eq]; exact head_not_mem_tail e' e'' hm
  simp [rcns, hf₁, h₁, hf₂, h₂, h₃]
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
have ⟨h₁, h₂⟩ := hf
State after:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
h₁ : rcn f = i
h₂ : rcns f'' = rcn e' :: List.erase (rcns e'') i
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i

State before:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
h₁ : rcn f = i
h₂ : rcns f'' = rcn e' :: List.erase (rcns e'') i
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
have ⟨_, f, f', ⟨hf₁, hf₂⟩⟩ := e.prepend_indep f $ h₁.symm ▸ hr |>.cons_head
State after:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f✝ : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f✝ = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
h₁ : rcn f✝ = i
h₂ : rcns f'' = rcn e' :: List.erase (rcns e'') i
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn f✝
hf₂ : rcn f' = rcn e
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i

State before:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f✝ : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f✝ = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
h₁ : rcn f✝ = i
h₂ : rcns f'' = rcn e' :: List.erase (rcns e'') i
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn f✝
hf₂ : rcn f' = rcn e
⊢ ∃ f, rcns f = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
exists trans f $ trans f' f''
State after:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f✝ : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f✝ = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
h₁ : rcn f✝ = i
h₂ : rcns f'' = rcn e' :: List.erase (rcns e'') i
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn f✝
hf₂ : rcn f' = rcn e
⊢ rcns (trans f (trans f' f'')) = i :: rcn e :: List.erase (rcn e' :: rcns e'') i

State before:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f✝ : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f✝ = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
h₁ : rcn f✝ = i
h₂ : rcns f'' = rcn e' :: List.erase (rcns e'') i
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn f✝
hf₂ : rcn f' = rcn e
⊢ rcns (trans f (trans f' f'')) = i :: rcn e :: 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'' hm
State after:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f✝ : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f✝ = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
h₁ : rcn f✝ = i
h₂ : rcns f'' = rcn e' :: List.erase (rcns e'') i
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn f✝
hf₂ : rcn f' = rcn e
h₃ : List.erase (rcn e' :: rcns e'') i = rcn e' :: List.erase (rcns e'') i
⊢ rcns (trans f (trans f' f'')) = i :: rcn e :: List.erase (rcn e' :: rcns e'') i

State before:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f✝ : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f✝ = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
h₁ : rcn f✝ = i
h₂ : rcns f'' = rcn e' :: List.erase (rcns e'') i
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn f✝
hf₂ : rcn f' = rcn e
h₃ : List.erase (rcn e' :: rcns e'') i = rcn e' :: List.erase (rcns e'') i
⊢ rcns (trans f (trans f' f'')) = i :: rcn e :: List.erase (rcn e' :: rcns e'') i
Tactic:
simp [rcns, hf₁, h₁, hf₂, h₂, h₃]
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f✝ : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f✝ = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
h₁ : rcn f✝ = i
h₂ : rcns f'' = rcn e' :: List.erase (rcns e'') i
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn f✝
hf₂ : rcn f' = rcn e
⊢ ¬(?m.81182 == ?m.81181) = true
Tactic:
simp only [beq_iff_eq]
State after:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f✝ : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f✝ = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
h₁ : rcn f✝ = i
h₂ : rcns f'' = rcn e' :: List.erase (rcns e'') i
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn f✝
hf₂ : rcn f' = rcn e
⊢ ¬?m.81182 = ?m.81181

State before:
α : Type
inst✝ : Proper α
s s₂✝¹ s₃ : State α
i : ID
s₁✝ s₂ s₄ : State α
e' : s₁✝ ↓ᵢ s₂
e'' : s₂ ↓ᵢ+ s₄
hi :
  ∀ {s₁ : State α} (e : s₁ ↓ᵢ s₂),
    i ∈ rcns e'' → (rcn e :: rcns e'' ≮[s₁.rtr] i) → ∃ f, rcns f = i :: rcn e :: List.erase (rcns e'') i
s₁ : State α
e : s₁ ↓ᵢ s₁✝
hr : rcn e :: rcn e' :: rcns e'' ≮[s₁.rtr] i
hm : i ∈ rcns e''
s₂✝ : State α
f✝ : s₁✝ ↓ᵢ s₂✝
f'' : s₂✝ ↓ᵢ+ s₄
hf : rcn f✝ = i ∧ rcns f'' = rcn e' :: List.erase (rcns e'') i
h₁ : rcn f✝ = i
h₂ : rcns f'' = rcn e' :: List.erase (rcns e'') i
w✝ : State α
f : s₁ ↓ᵢ w✝
f' : w✝ ↓ᵢ s₂✝
hf₁ : rcn f = rcn f✝
hf₂ : rcn f' = rcn e
⊢ ¬?m.81182 = ?m.81181
Tactic:
exact head_not_mem_tail e' e'' hm
State after:
no goals