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

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
h : rcn e₁ ≮[s₁.rtr] rcn e₂
⊢ ∃ s₂' e₁' e₂', rcn e₁' = rcn e₂ ∧ rcn e₂' = rcn e₁
Tactic:
have ⟨s₂', _, e₁', e₂', h₁, h₂, h⟩ := prepend_indep' e₁ e₂ h
State after:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
h✝ : rcn e₁ ≮[s₁.rtr] rcn e₂
s₂' w✝ : State α
e₁' : s₁ ↓ᵢ s₂'
e₂' : s₂' ↓ᵢ w✝
h₁ : rcn e₁' = rcn e₂
h₂ : rcn e₂' = rcn e₁
h : w✝ = s₃
⊢ ∃ s₂' e₁' e₂', rcn e₁' = rcn e₂ ∧ rcn e₂' = rcn e₁

State before:
α : Type
inst✝ : Proper α
s₁ s₂ s₃ : State α
e₁ : s₁ ↓ᵢ s₂
e₂ : s₂ ↓ᵢ s₃
h✝ : rcn e₁ ≮[s₁.rtr] rcn e₂
s₂' w✝ : State α
e₁' : s₁ ↓ᵢ s₂'
e₂' : s₂' ↓ᵢ w✝
h₁ : rcn e₁' = rcn e₂
h₂ : rcn e₂' = rcn e₁
h : w✝ = s₃
⊢ ∃ s₂' e₁' e₂', rcn e₁' = rcn e₂ ∧ rcn e₂' = rcn e₁
Tactic:
subst h
State after:
α : Type
inst✝ : Proper α
s₁ s₂ : State α
e₁ : s₁ ↓ᵢ s₂
s₂' w✝ : State α
e₁' : s₁ ↓ᵢ s₂'
e₂' : s₂' ↓ᵢ w✝
h₂ : rcn e₂' = rcn e₁
e₂ : s₂ ↓ᵢ w✝
h : rcn e₁ ≮[s₁.rtr] rcn e₂
h₁ : rcn e₁' = rcn e₂
⊢ ∃ s₂' e₁' e₂', rcn e₁' = rcn e₂ ∧ rcn e₂' = rcn e₁

State before:
α : Type
inst✝ : Proper α
s₁ s₂ : State α
e₁ : s₁ ↓ᵢ s₂
s₂' w✝ : State α
e₁' : s₁ ↓ᵢ s₂'
e₂' : s₂' ↓ᵢ w✝
h₂ : rcn e₂' = rcn e₁
e₂ : s₂ ↓ᵢ w✝
h : rcn e₁ ≮[s₁.rtr] rcn e₂
h₁ : rcn e₁' = rcn e₂
⊢ ∃ s₂' e₁' e₂', rcn e₁' = rcn e₂ ∧ rcn e₂' = rcn e₁
Tactic:
exists s₂', e₁', e₂'
State after:
no goals