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

State before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
h₁ : s₁.rtr[Component.rcn][i] = some rcn
h₂ : s₂.rtr[Component.rcn][i] = some rcn
⊢ input s₁ i = input s₂ i
Tactic:
simp [input, h₁, h₂]
State after:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
h₁ : s₁.rtr[Component.rcn][i] = some rcn
h₂ : s₂.rtr[Component.rcn][i] = some rcn
⊢ ((fun cpt => input.restriction s₁ rcn cpt) = fun cpt => input.restriction s₂ rcn cpt) ∧ s₁.tag = s₂.tag

State before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
h₁ : s₁.rtr[Component.rcn][i] = some rcn
h₂ : s₂.rtr[Component.rcn][i] = some rcn
⊢ ((fun cpt => input.restriction s₁ rcn cpt) = fun cpt => input.restriction s₂ rcn cpt) ∧ s₁.tag = s₂.tag
Tactic:
refine ⟨?_, e.preserves_tag⟩
State after:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
h₁ : s₁.rtr[Component.rcn][i] = some rcn
h₂ : s₂.rtr[Component.rcn][i] = some rcn
⊢ (fun cpt => input.restriction s₁ rcn cpt) = fun cpt => input.restriction s₂ rcn cpt

State before:
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
h₁ : s₁.rtr[Component.rcn][i] = some rcn
h₂ : s₂.rtr[Component.rcn][i] = some rcn
⊢ (fun cpt => input.restriction s₁ rcn cpt) = fun cpt => input.restriction s₂ rcn cpt
Tactic:
ext1
State after:
case h
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
h₁ : s₁.rtr[Component.rcn][i] = some rcn
h₂ : s₂.rtr[Component.rcn][i] = some rcn
x✝ : Component.Valued
⊢ input.restriction s₁ rcn x✝ = input.restriction s₂ rcn x✝

State before:
case h
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
h₁ : s₁.rtr[Component.rcn][i] = some rcn
h₂ : s₂.rtr[Component.rcn][i] = some rcn
x✝ : Component.Valued
⊢ input.restriction s₁ rcn x✝ = input.restriction s₂ rcn x✝
Tactic:
exact e.indep_restriction_eq hi h₁
State after:
no goals