Theorem: Execution.Step.Time.deterministic (ReactorModel/Execution/Theorems/Step/Time.lean)

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ₜ s₁
e₂ : s ↓ₜ s₂
⊢ s₁ = s₂
Tactic:
have hn := e₁.next_tag.deterministic e₂.next_tag
State after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ₜ s₁
e₂ : s ↓ₜ s₂
hn : s₁.tag = s₂.tag
⊢ s₁ = s₂

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ₜ s₁
e₂ : s ↓ₜ s₂
hn : s₁.tag = s₂.tag
⊢ s₁ = s₂
Tactic:
have hr := hn ▸ e₁.refreshed |>.deterministic e₂.refreshed
State after:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ₜ s₁
e₂ : s ↓ₜ s₂
hn : s₁.tag = s₂.tag
hr : s₁.rtr = s₂.rtr
⊢ s₁ = s₂

State before:
α : Type
inst✝ : Proper α
s s₁ s₂ : State α
e₁ : s ↓ₜ s₁
e₂ : s ↓ₜ s₂
hn : s₁.tag = s₂.tag
hr : s₁.rtr = s₂.rtr
⊢ s₁ = s₂
Tactic:
ext1 <;> simp [hn, hr, e₁.progress_empty, e₂.progress_empty, e₁.events_eq, e₂.events_eq]
State after:
no goals