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

State before:
α : Type
inst✝ : Proper α
c₁ c₂ : Change
s s₁ s₂ s₁₂ s₂₁ : State α
ht : Change.target c₁ ≠ Change.target c₂ ∨ Change.target c₁ = none
e₁ : s -[c₁]→ s₁
e₁₂ : s₁ -[c₂]→ s₁₂
e₂ : s -[c₂]→ s₂
e₂₁ : s₂ -[c₁]→ s₂₁
⊢ s₁₂ = s₂₁
Tactic:
cases e₁ <;> cases e₁₂ <;> cases e₂ <;> cases e₂₁ <;> simp [Change.target] at ht ⊢
State after:
case inp.inp.inp.inp
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.inp i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.inp i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : ¬i✝¹ = i✝
⊢ rtr✝² = rtr✝

case inp.out.out.inp
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.out i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.inp i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : True
⊢ rtr✝² = rtr✝

case inp.stv.stv.inp
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.stv i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.inp i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : True
⊢ rtr✝² = rtr✝

case inp.act.act.inp
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ s.rtr rtr✝¹
i✝ : ID
t✝ : _root_.Time
v✝ : Value
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
ht : True
⊢ schedule { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }

case inp.mut.mut.inp
α : Type
inst✝ : Proper α
s : State α
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝¹
x✝ : Change.Mutation
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝
ht : True
⊢ rtr✝¹ = rtr✝

case out.inp.inp.out
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.inp i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.out i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : True
⊢ rtr✝² = rtr✝

case out.out.out.out
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.out i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.out i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : ¬i✝¹ = i✝
⊢ rtr✝² = rtr✝

case out.stv.stv.out
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.stv i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.out i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : True
⊢ rtr✝² = rtr✝

case out.act.act.out
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ s.rtr rtr✝¹
i✝ : ID
t✝ : _root_.Time
v✝ : Value
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
ht : True
⊢ schedule { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }

case out.mut.mut.out
α : Type
inst✝ : Proper α
s : State α
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝¹
x✝ : Change.Mutation
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝
ht : True
⊢ rtr✝¹ = rtr✝

case stv.inp.inp.stv
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.inp i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.stv i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : True
⊢ rtr✝² = rtr✝

case stv.out.out.stv
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.out i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.stv i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : True
⊢ rtr✝² = rtr✝

case stv.stv.stv.stv
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.stv i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.stv i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : ¬i✝¹ = i✝
⊢ rtr✝² = rtr✝

case stv.act.act.stv
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝¹
i✝ : ID
t✝ : _root_.Time
v✝ : Value
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
ht : True
⊢ schedule { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }

case stv.mut.mut.stv
α : Type
inst✝ : Proper α
s : State α
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
x✝ : Change.Mutation
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝
ht : True
⊢ rtr✝¹ = rtr✝

case act.inp.inp.act
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.inp i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝
ht : True
⊢ { rtr := rtr✝¹, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹

case act.out.out.act
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.out i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝
ht : True
⊢ { rtr := rtr✝¹, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹

case act.stv.stv.act
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝
ht : True
⊢ { rtr := rtr✝¹, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹

case act.act.act.act
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝¹ : _root_.Time
v✝¹ : Value
i✝ : ID
t✝ : _root_.Time
v✝ : Value
ht : ¬i✝¹ = i✝
⊢ schedule (schedule s i✝¹ t✝¹ v✝¹) i✝ t✝ v✝ = schedule (schedule s i✝ t✝ v✝) i✝¹ t✝¹ v✝¹

case mut.inp.inp.mut
α : Type
inst✝ : Proper α
s : State α
x✝ : Change.Mutation
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝
ht : True
⊢ rtr✝¹ = rtr✝

case mut.out.out.mut
α : Type
inst✝ : Proper α
s : State α
x✝ : Change.Mutation
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝
ht : True
⊢ rtr✝¹ = rtr✝

case mut.stv.stv.mut
α : Type
inst✝ : Proper α
s : State α
x✝ : Change.Mutation
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝
ht : True
⊢ rtr✝¹ = rtr✝

State before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝¹ : _root_.Time
v✝¹ : Value
i✝ : ID
t✝ : _root_.Time
v✝ : Value
ht : ¬i✝¹ = i✝
⊢ schedule (schedule s i✝¹ t✝¹ v✝¹) i✝ t✝ v✝ = schedule (schedule s i✝ t✝ v✝) i✝¹ t✝¹ v✝¹
Tactic:
case act.act.act.act =>               exact schedule_ne_comm ht
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ s.rtr rtr✝¹
i✝ : ID
t✝ : _root_.Time
v✝ : Value
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
ht : True
⊢ schedule { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }
Tactic:
case inp.act.act.inp u₁ _ _ _ _ u₂ => cases LawfulUpdate.unique u₁ u₂; rfl
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ s.rtr rtr✝¹
i✝ : ID
t✝ : _root_.Time
v✝ : Value
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
ht : True
⊢ schedule { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }
Tactic:
case out.act.act.out u₁ _ _ _ _ u₂ => cases LawfulUpdate.unique u₁ u₂; rfl
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝¹
i✝ : ID
t✝ : _root_.Time
v✝ : Value
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
ht : True
⊢ schedule { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }
Tactic:
case stv.act.act.stv u₁ _ _ _ _ u₂ => cases LawfulUpdate.unique u₁ u₂; rfl
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.inp i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝¹
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝
ht : True
⊢ { rtr := rtr✝¹, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹
Tactic:
case act.inp.inp.act u₁ _ u₂       => cases LawfulUpdate.unique u₁ u₂; rfl
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.out i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝¹
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝
ht : True
⊢ { rtr := rtr✝¹, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹
Tactic:
case act.out.out.act u₁ _ u₂       => cases LawfulUpdate.unique u₁ u₂; rfl
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.stv i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝¹
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝
ht : True
⊢ { rtr := rtr✝¹, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹
Tactic:
case act.stv.stv.act u₁ _ u₂       => cases LawfulUpdate.unique u₁ u₂; rfl
State after:
no goals

State before:
case inp.inp.inp.inp
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.inp i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.inp i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : ¬i✝¹ = i✝
⊢ rtr✝² = rtr✝

case inp.out.out.inp
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.out i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.inp i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : True
⊢ rtr✝² = rtr✝

case inp.stv.stv.inp
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.stv i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.inp i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : True
⊢ rtr✝² = rtr✝

case inp.mut.mut.inp
α : Type
inst✝ : Proper α
s : State α
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝¹
x✝ : Change.Mutation
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝
ht : True
⊢ rtr✝¹ = rtr✝

case out.inp.inp.out
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.inp i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.out i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : True
⊢ rtr✝² = rtr✝

case out.out.out.out
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.out i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.out i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : ¬i✝¹ = i✝
⊢ rtr✝² = rtr✝

case out.stv.stv.out
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.stv i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.out i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : True
⊢ rtr✝² = rtr✝

case out.mut.mut.out
α : Type
inst✝ : Proper α
s : State α
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝¹
x✝ : Change.Mutation
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝
ht : True
⊢ rtr✝¹ = rtr✝

case stv.inp.inp.stv
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.inp i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.stv i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : True
⊢ rtr✝² = rtr✝

case stv.out.out.stv
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.out i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.stv i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : True
⊢ rtr✝² = rtr✝

case stv.stv.stv.stv
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.stv i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.stv i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : ¬i✝¹ = i✝
⊢ rtr✝² = rtr✝

case stv.mut.mut.stv
α : Type
inst✝ : Proper α
s : State α
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
x✝ : Change.Mutation
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝
ht : True
⊢ rtr✝¹ = rtr✝

case mut.inp.inp.mut
α : Type
inst✝ : Proper α
s : State α
x✝ : Change.Mutation
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝
ht : True
⊢ rtr✝¹ = rtr✝

case mut.out.out.mut
α : Type
inst✝ : Proper α
s : State α
x✝ : Change.Mutation
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝
ht : True
⊢ rtr✝¹ = rtr✝

case mut.stv.stv.mut
α : Type
inst✝ : Proper α
s : State α
x✝ : Change.Mutation
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝
ht : True
⊢ rtr✝¹ = rtr✝
Tactic:
all_goals
  try exact LawfulUpdate.unique ‹_› ‹_›
  try case _ u₁ _ _ _ u₂ _ u₃ _ u₄ => exact LawfulUpdate.ne_comm u₁ u₂ u₃ u₄ $ by simp [ht]
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝¹ : _root_.Time
v✝¹ : Value
i✝ : ID
t✝ : _root_.Time
v✝ : Value
ht : ¬i✝¹ = i✝
⊢ schedule (schedule s i✝¹ t✝¹ v✝¹) i✝ t✝ v✝ = schedule (schedule s i✝ t✝ v✝) i✝¹ t✝¹ v✝¹
Tactic:
exact schedule_ne_comm ht
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ s.rtr rtr✝¹
i✝ : ID
t✝ : _root_.Time
v✝ : Value
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
ht : True
⊢ schedule { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }
Tactic:
cases LawfulUpdate.unique u₁ u₂
State after:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ s.rtr rtr✝
i✝ : ID
t✝ : _root_.Time
v✝ : Value
ht : True
u₂ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
⊢ schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }

State before:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ s.rtr rtr✝
i✝ : ID
t✝ : _root_.Time
v✝ : Value
ht : True
u₂ : LawfulUpdate Component.Valued.inp i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
⊢ schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }
Tactic:
rfl
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ s.rtr rtr✝¹
i✝ : ID
t✝ : _root_.Time
v✝ : Value
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
ht : True
⊢ schedule { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }
Tactic:
cases LawfulUpdate.unique u₁ u₂
State after:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ s.rtr rtr✝
i✝ : ID
t✝ : _root_.Time
v✝ : Value
ht : True
u₂ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
⊢ schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }

State before:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ s.rtr rtr✝
i✝ : ID
t✝ : _root_.Time
v✝ : Value
ht : True
u₂ : LawfulUpdate Component.Valued.out i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
⊢ schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }
Tactic:
rfl
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝¹
i✝ : ID
t✝ : _root_.Time
v✝ : Value
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
ht : True
⊢ schedule { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }
Tactic:
cases LawfulUpdate.unique u₁ u₂
State after:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝
i✝ : ID
t✝ : _root_.Time
v✝ : Value
ht : True
u₂ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
⊢ schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }

State before:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝
i✝ : ID
t✝ : _root_.Time
v✝ : Value
ht : True
u₂ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ (schedule s i✝ t✝ v✝).rtr rtr✝
⊢ schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝ t✝ v✝ =
    { rtr := rtr✝, tag := (schedule s i✝ t✝ v✝).tag, progress := (schedule s i✝ t✝ v✝).progress,
      events := (schedule s i✝ t✝ v✝).events }
Tactic:
rfl
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.inp i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝¹
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝
ht : True
⊢ { rtr := rtr✝¹, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹
Tactic:
cases LawfulUpdate.unique u₁ u₂
State after:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.inp i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝
ht : True
u₂ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝
⊢ { rtr := rtr✝, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹

State before:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.inp i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝
ht : True
u₂ : LawfulUpdate Component.Valued.inp i✝ v✝ s.rtr rtr✝
⊢ { rtr := rtr✝, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹
Tactic:
rfl
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.out i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝¹
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝
ht : True
⊢ { rtr := rtr✝¹, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹
Tactic:
cases LawfulUpdate.unique u₁ u₂
State after:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.out i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝
ht : True
u₂ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝
⊢ { rtr := rtr✝, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹

State before:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.out i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝
ht : True
u₂ : LawfulUpdate Component.Valued.out i✝ v✝ s.rtr rtr✝
⊢ { rtr := rtr✝, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹
Tactic:
rfl
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝¹ : α
u₁ : LawfulUpdate Component.Valued.stv i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝¹
rtr✝ : α
u₂ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝
ht : True
⊢ { rtr := rtr✝¹, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹
Tactic:
cases LawfulUpdate.unique u₁ u₂
State after:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.stv i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝
ht : True
u₂ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝
⊢ { rtr := rtr✝, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹

State before:
case refl
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
t✝ : _root_.Time
v✝¹ : Value
i✝ : ID
v✝ : Value
rtr✝ : α
u₁ : LawfulUpdate Component.Valued.stv i✝ v✝ (schedule s i✝¹ t✝ v✝¹).rtr rtr✝
ht : True
u₂ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝
⊢ { rtr := rtr✝, tag := (schedule s i✝¹ t✝ v✝¹).tag, progress := (schedule s i✝¹ t✝ v✝¹).progress,
      events := (schedule s i✝¹ t✝ v✝¹).events } =
    schedule { rtr := rtr✝, tag := s.tag, progress := s.progress, events := s.events } i✝¹ t✝ v✝¹
Tactic:
rfl
State after:
no goals

State before:
case mut.stv.stv.mut
α : Type
inst✝ : Proper α
s : State α
x✝ : Change.Mutation
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝
ht : True
⊢ rtr✝¹ = rtr✝
Tactic:
try exact LawfulUpdate.unique ‹_› ‹_›
State after:
no goals

State before:
case stv.stv.stv.stv
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
a✝³ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
a✝² :
  LawfulUpdate Component.Valued.stv i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ :
  LawfulUpdate Component.Valued.stv i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : ¬i✝¹ = i✝
⊢ rtr✝² = rtr✝
Tactic:
try case _ u₁ _ _ _ u₂ _ u₃ _ u₄ => exact LawfulUpdate.ne_comm u₁ u₂ u₃ u₄ $ by simp [ht]
State after:
no goals

State before:
case mut.stv.stv.mut
α : Type
inst✝ : Proper α
s : State α
x✝ : Change.Mutation
i✝ : ID
v✝ : Value
rtr✝¹ : α
a✝¹ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝
ht : True
⊢ rtr✝¹ = rtr✝
Tactic:
exact LawfulUpdate.unique ‹_› ‹_›
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
u₁ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
u₂ :
  LawfulUpdate Component.Valued.stv i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
u₃ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
u₄ :
  LawfulUpdate Component.Valued.stv i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : ¬i✝¹ = i✝
⊢ rtr✝² = rtr✝
Tactic:
case _ u₁ _ _ _ u₂ _ u₃ _ u₄ => exact LawfulUpdate.ne_comm u₁ u₂ u₃ u₄ $ by simp [ht]
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
u₁ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
u₂ :
  LawfulUpdate Component.Valued.stv i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
u₃ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
u₄ :
  LawfulUpdate Component.Valued.stv i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : ¬i✝¹ = i✝
⊢ rtr✝² = rtr✝
Tactic:
exact LawfulUpdate.ne_comm u₁ u₂ u₃ u₄ $ by simp [ht]
State after:
no goals

State before:
α : Type
inst✝ : Proper α
s : State α
i✝¹ : ID
v✝¹ : Value
rtr✝³ : α
u₁ : LawfulUpdate Component.Valued.stv i✝¹ v✝¹ s.rtr rtr✝³
i✝ : ID
v✝ : Value
rtr✝² : α
u₂ :
  LawfulUpdate Component.Valued.stv i✝ v✝ { rtr := rtr✝³, tag := s.tag, progress := s.progress, events := s.events }.rtr
    rtr✝²
rtr✝¹ : α
u₃ : LawfulUpdate Component.Valued.stv i✝ v✝ s.rtr rtr✝¹
rtr✝ : α
u₄ :
  LawfulUpdate Component.Valued.stv i✝¹ v✝¹
    { rtr := rtr✝¹, tag := s.tag, progress := s.progress, events := s.events }.rtr rtr✝
ht : ¬i✝¹ = i✝
⊢ Component.Valued.stv ≠ Component.Valued.stv ∨ i✝¹ ≠ i✝
Tactic:
simp [ht]
State after:
no goals