Theorem: Execution.Step.Apply.events_congr (ReactorModel/Execution/Theorems/Step/Apply.lean)

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂ s₂' s₁₂ s₂₁ : State α
c : Change
e : s₁ -[c]→ s₂
e' : s₁' -[c]→ s₂'
he : s₁.events = s₁'.events
⊢ s₂.events = s₂'.events
Tactic:
cases e <;> cases e' <;> simp [he]
State after:
case act.act
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₁₂ s₂₁ : State α
he : s₁.events = s₁'.events
i✝ : ID
t✝ : _root_.Time
v✝ : Value
⊢ (schedule s₁ i✝ t✝ v✝).events = (schedule s₁' i✝ t✝ v✝).events

State before:
case act.act
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₁₂ s₂₁ : State α
he : s₁.events = s₁'.events
i✝ : ID
t✝ : _root_.Time
v✝ : Value
⊢ (schedule s₁ i✝ t✝ v✝).events = (schedule s₁' i✝ t✝ v✝).events
Tactic:
exact schedule_events_congr he
State after:
no goals