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

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
⊢ s₁ = s₂
Tactic:
have := e₁.preserves_tag ▸ e₂.preserves_tag
State after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
this : s₁.tag = s₂.tag
⊢ s₁ = s₂

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
this : s₁.tag = s₂.tag
⊢ s₁ = s₂
Tactic:
have ⟨_, _⟩ := rcns_perm_deterministic e₁ e₂ $ progress_eq_rcns_perm e₁ e₂ hp
State after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
this : s₁.tag = s₂.tag
left✝ : s₁.rtr = s₂.rtr
right✝ : s₁.events = s₂.events
⊢ s₁ = s₂

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
this : s₁.tag = s₂.tag
left✝ : s₁.rtr = s₂.rtr
right✝ : s₁.events = s₂.events
⊢ s₁ = s₂
Tactic:
ext1 <;> try assumption
State after:
no goals

State before:
case events
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ᵢ+ s₁
e₂ : s ↓ᵢ+ s₂
hp : s₁.progress = s₂.progress
this : s₁.tag = s₂.tag
left✝ : s₁.rtr = s₂.rtr
right✝ : s₁.events = s₂.events
⊢ s₁.events = s₂.events
Tactic:
assumption
State after:
no goals