Theorem: Execution.State.schedule_ne_comm (ReactorModel/Execution/Theorems/State.lean)

State before:
α : Type
inst✝ : Hierarchical α
s✝ s₁ s₂ s : State α
i₁ i₂ : ID
t₁ t₂ : Time
v₁ v₂ : Value
h : i₁ ≠ i₂
⊢ schedule (schedule s i₁ t₁ v₁) i₂ t₂ v₂ = schedule (schedule s i₂ t₂ v₂) i₁ t₁ v₁
Tactic:
simp [schedule]
State after:
α : Type
inst✝ : Hierarchical α
s✝ s₁ s₂ s : State α
i₁ i₂ : ID
t₁ t₂ : Time
v₁ v₂ : Value
h : i₁ ≠ i₂
⊢ (Partial.update (Partial.update s.events i₁ fun x => schedule.go x t₁ v₁) i₂ fun x => schedule.go x t₂ v₂) =
    Partial.update (Partial.update s.events i₂ fun x => schedule.go x t₂ v₂) i₁ fun x => schedule.go x t₁ v₁

State before:
α : Type
inst✝ : Hierarchical α
s✝ s₁ s₂ s : State α
i₁ i₂ : ID
t₁ t₂ : Time
v₁ v₂ : Value
h : i₁ ≠ i₂
⊢ (Partial.update (Partial.update s.events i₁ fun x => schedule.go x t₁ v₁) i₂ fun x => schedule.go x t₂ v₂) =
    Partial.update (Partial.update s.events i₂ fun x => schedule.go x t₂ v₂) i₁ fun x => schedule.go x t₁ v₁
Tactic:
apply Partial.update_ne_comm _ h
State after:
no goals