Theorem: Reactor.set.go_preserves
Proof state before:
case cons
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
tail_ih✝ :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
h : ¬c = cpt ∨ ¬(i = head✝ ∨ i ∈ tail✝) ∨ vs i = none
⊢ (match vs head✝ with
      | none => go rtr cpt vs tail✝
      | some v => go (update rtr cpt head✝ v) cpt vs tail✝)[Component.val c][i] =
    some o
Tactic:
split <;> cases h <;> try cases ‹_ ∨ _›
Proof state after:
case cons.h_1.inl
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
tail_ih✝ :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
heq✝ : vs head✝ = none
h✝ : ¬c = cpt
⊢ go rtr cpt vs tail✝[Component.val c][i] = some o

case cons.h_1.inr.inl
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
tail_ih✝ :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
heq✝ : vs head✝ = none
h✝ : ¬(i = head✝ ∨ i ∈ tail✝)
⊢ go rtr cpt vs tail✝[Component.val c][i] = some o

case cons.h_1.inr.inr
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
tail_ih✝ :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
heq✝ : vs head✝ = none
h✝ : vs i = none
⊢ go rtr cpt vs tail✝[Component.val c][i] = some o

case cons.h_2.inl
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
tail_ih✝ :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v✝ : Value
heq✝ : vs head✝ = some v✝
h✝ : ¬c = cpt
⊢ go (update rtr cpt head✝ v✝) cpt vs tail✝[Component.val c][i] = some o

case cons.h_2.inr.inl
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
tail_ih✝ :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v✝ : Value
heq✝ : vs head✝ = some v✝
h✝ : ¬(i = head✝ ∨ i ∈ tail✝)
⊢ go (update rtr cpt head✝ v✝) cpt vs tail✝[Component.val c][i] = some o

case cons.h_2.inr.inr
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
tail_ih✝ :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v✝ : Value
heq✝ : vs head✝ = some v✝
h✝ : vs i = none
⊢ go (update rtr cpt head✝ v✝) cpt vs tail✝[Component.val c][i] = some o