Theorem: Reactor.set_updated' (ReactorModel/Objects/Reactor/Theorems/Accessible.lean)

State before:
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
⊢ set rtr cpt vs[Component.val cpt] = fun i => do
    let x ← rtr[Component.val cpt][i]
    some (Option.getD (vs i) x)
Tactic:
ext1 i
State after:
case h
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
i : Component.idType (Component.val cpt)
⊢ set rtr cpt vs[Component.val cpt][i] = do
    let x ← rtr[Component.val cpt][i]
    some (Option.getD (vs i) x)

State before:
case h
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
i : Component.idType (Component.val cpt)
⊢ set rtr cpt vs[Component.val cpt][i] = do
    let x ← rtr[Component.val cpt][i]
    some (Option.getD (vs i) x)
Tactic:
cases ho : rtr[cpt][i] <;> simp [bind, ho, Option.getD] <;> try split
State after:
case h.none
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
i : Component.idType (Component.val cpt)
ho : rtr[Component.val cpt][i] = none
⊢ set rtr cpt vs[Component.val cpt][i] = none

case h.some.h_1
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
i : Component.idType (Component.val cpt)
val✝ : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some val✝
opt✝ : Option Value
x✝ : Value
heq✝ : vs i = some x✝
⊢ set rtr cpt vs[Component.val cpt][i] = some x✝

case h.some.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
i : Component.idType (Component.val cpt)
val✝ : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some val✝
opt✝ : Option Value
heq✝ : vs i = none
⊢ set rtr cpt vs[Component.val cpt][i] = some val✝

State before:
case h.some
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
i : Component.idType (Component.val cpt)
val✝ : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some val✝
⊢ set rtr cpt vs[Component.val cpt][i] =
    some
      (match vs i with
      | some x => x
      | none => val✝)
Tactic:
split
State after:
case h.some.h_1
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
i : Component.idType (Component.val cpt)
val✝ : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some val✝
opt✝ : Option Value
x✝ : Value
heq✝ : vs i = some x✝
⊢ set rtr cpt vs[Component.val cpt][i] = some x✝

case h.some.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
i : Component.idType (Component.val cpt)
val✝ : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some val✝
opt✝ : Option Value
heq✝ : vs i = none
⊢ set rtr cpt vs[Component.val cpt][i] = some val✝

State before:
case h.none
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
i : Component.idType (Component.val cpt)
ho : rtr[Component.val cpt][i] = none
⊢ set rtr cpt vs[Component.val cpt][i] = none
Tactic:
exact Equivalent.obj?_none_iff set_equiv |>.mp ho
State after:
no goals

State before:
case h.some.h_1
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
i : Component.idType (Component.val cpt)
val✝ : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some val✝
opt✝ : Option Value
x✝ : Value
heq✝ : vs i = some x✝
⊢ set rtr cpt vs[Component.val cpt][i] = some x✝
Tactic:
exact set.go_updated ho ‹_› $ mem_ids_iff.mpr ⟨_, ho⟩
State after:
no goals

State before:
case h.some.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
i : Component.idType (Component.val cpt)
val✝ : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some val✝
opt✝ : Option Value
heq✝ : vs i = none
⊢ set rtr cpt vs[Component.val cpt][i] = some val✝
Tactic:
exact set.go_preserves ho $ .inr $ .inr ‹_›
State after:
no goals