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

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂ s₂' s₁₂ s₂₁ : State α
c : Change
cpt : Component.Valued
i : ID
e : s₁ -[c]→ s₂
h : ¬Change.Targets c cpt i
⊢ s₁.rtr[Component.val cpt][i] = s₂.rtr[Component.val cpt][i]
Tactic:
cases e <;> try exact .refl _
State after:
case inp
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
cpt : Component.Valued
i i✝ : ID
v✝ : Value
rtr✝ : α
h : ¬Change.Targets (Change.inp i✝ v✝) cpt i
a✝ : LawfulUpdate Component.Valued.inp i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr[Component.val cpt][i] =
    { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr[Component.val cpt][i]

case out
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
cpt : Component.Valued
i i✝ : ID
v✝ : Value
rtr✝ : α
h : ¬Change.Targets (Change.out i✝ v✝) cpt i
a✝ : LawfulUpdate Component.Valued.out i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr[Component.val cpt][i] =
    { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr[Component.val cpt][i]

case stv
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
cpt : Component.Valued
i i✝ : ID
v✝ : Value
rtr✝ : α
h : ¬Change.Targets (Change.stv i✝ v✝) cpt i
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr[Component.val cpt][i] =
    { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr[Component.val cpt][i]

State before:
case inp
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
cpt : Component.Valued
i i✝ : ID
v✝ : Value
rtr✝ : α
h : ¬Change.Targets (Change.inp i✝ v✝) cpt i
a✝ : LawfulUpdate Component.Valued.inp i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr[Component.val cpt][i] =
    { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr[Component.val cpt][i]

case out
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
cpt : Component.Valued
i i✝ : ID
v✝ : Value
rtr✝ : α
h : ¬Change.Targets (Change.out i✝ v✝) cpt i
a✝ : LawfulUpdate Component.Valued.out i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr[Component.val cpt][i] =
    { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr[Component.val cpt][i]

case stv
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
cpt : Component.Valued
i i✝ : ID
v✝ : Value
rtr✝ : α
h : ¬Change.Targets (Change.stv i✝ v✝) cpt i
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr[Component.val cpt][i] =
    { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr[Component.val cpt][i]
Tactic:
all_goals simp [LawfulUpdate.obj?_preserved (Change.Targets.norm_not h) ‹_›]
State after:
no goals

State before:
case mut
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
cpt : Component.Valued
i : ID
x✝ : Change.Mutation
h : ¬Change.Targets (Change.mut x✝) cpt i
⊢ s₁.rtr[Component.val cpt][i] = s₁.rtr[Component.val cpt][i]
Tactic:
exact .refl _
State after:
no goals

State before:
case stv
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂' s₁₂ s₂₁ : State α
cpt : Component.Valued
i i✝ : ID
v✝ : Value
rtr✝ : α
h : ¬Change.Targets (Change.stv i✝ v✝) cpt i
a✝ : LawfulUpdate Component.Valued.stv i✝ v✝ s₁.rtr rtr✝
⊢ s₁.rtr[Component.val cpt][i] =
    { rtr := rtr✝, tag := s₁.tag, progress := s₁.progress, events := s₁.events }.rtr[Component.val cpt][i]
Tactic:
simp [LawfulUpdate.obj?_preserved (Change.Targets.norm_not h) ‹_›]
State after:
no goals