Theorem: Execution.Step.Exec.indep_restriction_eq (ReactorModel/Execution/Theorems/Step/Exec.lean)

State before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
cpt : Component.Valued
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
ho : s₁.rtr[Component.rcn][i] = some rcn
⊢ input.restriction s₁ rcn cpt = input.restriction s₂ rcn cpt
Tactic:
simp [input.restriction]
State after:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
cpt : Component.Valued
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
ho : s₁.rtr[Component.rcn][i] = some rcn
⊢ Partial.restrict (s₁.rtr[Component.val cpt]) {i | { cpt := cpt, id := i } ∈ rcn.deps Kind.in} =
    Partial.restrict (s₂.rtr[Component.val cpt]) {i | { cpt := cpt, id := i } ∈ rcn.deps Kind.in}

State before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
cpt : Component.Valued
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
ho : s₁.rtr[Component.rcn][i] = some rcn
⊢ Partial.restrict (s₁.rtr[Component.val cpt]) {i | { cpt := cpt, id := i } ∈ rcn.deps Kind.in} =
    Partial.restrict (s₂.rtr[Component.val cpt]) {i | { cpt := cpt, id := i } ∈ rcn.deps Kind.in}
Tactic:
apply Partial.ext_restrict
State after:
case h
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
cpt : Component.Valued
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
ho : s₁.rtr[Component.rcn][i] = some rcn
⊢ ∀ a ∈ {i | { cpt := cpt, id := i } ∈ rcn.deps Kind.in}, s₁.rtr[Component.val cpt][a] = s₂.rtr[Component.val cpt][a]

State before:
case h
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
cpt : Component.Valued
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
ho : s₁.rtr[Component.rcn][i] = some rcn
⊢ ∀ a ∈ {i | { cpt := cpt, id := i } ∈ rcn.deps Kind.in}, s₁.rtr[Component.val cpt][a] = s₂.rtr[Component.val cpt][a]
Tactic:
intro _ hd
State after:
case h
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
cpt : Component.Valued
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
ho : s₁.rtr[Component.rcn][i] = some rcn
a✝ : Component.idType (Component.val cpt)
hd : a✝ ∈ {i | { cpt := cpt, id := i } ∈ rcn.deps Kind.in}
⊢ s₁.rtr[Component.val cpt][a✝] = s₂.rtr[Component.val cpt][a✝]

State before:
case h
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
cpt : Component.Valued
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
ho : s₁.rtr[Component.rcn][i] = some rcn
a✝ : Component.idType (Component.val cpt)
hd : a✝ ∈ {i | { cpt := cpt, id := i } ∈ rcn.deps Kind.in}
⊢ s₁.rtr[Component.val cpt][a✝] = s₂.rtr[Component.val cpt][a✝]
Tactic:
exact e.applied_rtr_eq ▸ e.apply.preserves_unchanged $ State.target_not_mem_indep_output ho hi hd
State after:
no goals