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

State before:
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
c cpt : Component.Valued
vs : ID ⇀ Value
h : c ≠ cpt
⊢ set rtr cpt vs[Component.val c] = rtr[Component.val c]
Tactic:
ext1 i
State after:
case h
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
c cpt : Component.Valued
vs : ID ⇀ Value
h : c ≠ cpt
i : Component.idType (Component.val c)
⊢ set rtr cpt vs[Component.val c][i] = rtr[Component.val c][i]

State before:
case h
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
c cpt : Component.Valued
vs : ID ⇀ Value
h : c ≠ cpt
i : Component.idType (Component.val c)
⊢ set rtr cpt vs[Component.val c][i] = rtr[Component.val c][i]
Tactic:
cases ho : rtr[c][i]
State after:
case h.none
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
c cpt : Component.Valued
vs : ID ⇀ Value
h : c ≠ cpt
i : Component.idType (Component.val c)
ho : rtr[Component.val c][i] = none
⊢ set rtr cpt vs[Component.val c][i] = none

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

State before:
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
c cpt : Component.Valued
vs : ID ⇀ Value
h : c ≠ cpt
i : Component.idType (Component.val c)
val✝ : Component.type α (Component.val c)
ho : rtr[Component.val c][i] = some val✝
⊢ set rtr cpt vs[Component.val c][i] = some val✝
Tactic:
case some => exact set.go_preserves ho (.inl h)
State after:
no goals

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

State before:
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
c cpt : Component.Valued
vs : ID ⇀ Value
h : c ≠ cpt
i : Component.idType (Component.val c)
val✝ : Component.type α (Component.val c)
ho : rtr[Component.val c][i] = some val✝
⊢ set rtr cpt vs[Component.val c][i] = some val✝
Tactic:
exact set.go_preserves ho (.inl h)
State after:
no goals

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