Theorem: Execution.Step.Exec.indep_output_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
⊢ output s₁ i = output s₂ i
Tactic:
simp [output]
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
⊢ (match s₁.rtr[Component.rcn][i], [], fun x => x.body (input s₁ i) with
    | some x, x_1, f => f x
    | none, y, x => y) =
    match s₂.rtr[Component.rcn][i], [], fun x => x.body (input s₂ i) with
    | some x, x_1, f => f x
    | none, y, x => y

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
⊢ (match s₁.rtr[Component.rcn][i], [], fun x => x.body (input s₁ i) with
    | some x, x_1, f => f x
    | none, y, x => y) =
    match s₂.rtr[Component.rcn][i], [], fun x => x.body (input s₂ i) with
    | some x, x_1, f => f x
    | none, y, x => y
Tactic:
have he := Equivalent.obj?_rcn_eq e.equiv
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
he : s₁.rtr[Component.rcn] = s₂.rtr[Component.rcn]
⊢ (match s₁.rtr[Component.rcn][i], [], fun x => x.body (input s₁ i) with
    | some x, x_1, f => f x
    | none, y, x => y) =
    match s₂.rtr[Component.rcn][i], [], fun x => x.body (input s₂ i) with
    | some x, x_1, f => f x
    | none, y, x => y

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
he : s₁.rtr[Component.rcn] = s₂.rtr[Component.rcn]
⊢ (match s₁.rtr[Component.rcn][i], [], fun x => x.body (input s₁ i) with
    | some x, x_1, f => f x
    | none, y, x => y) =
    match s₂.rtr[Component.rcn][i], [], fun x => x.body (input s₂ i) with
    | some x, x_1, f => f x
    | none, y, x => y
Tactic:
cases h : s₁.rtr[.rcn][i] <;> simp [he ▸ h]
State after:
case some
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
he : s₁.rtr[Component.rcn] = s₂.rtr[Component.rcn]
val✝ : Component.type α Component.rcn
h : s₁.rtr[Component.rcn][i] = some val✝
⊢ val✝.body (input s₁ i) = val✝.body (input s₂ i)

State before:
case some
α : Type
inst✝ : Proper α
s s₁ : State α
rcn : Reaction
s₂ : State α
i : ID
e : s₁ ↓ₑ s₂
hi : Execution.Step.Exec.rcn e ≮[s₁.rtr]≯ i
he : s₁.rtr[Component.rcn] = s₂.rtr[Component.rcn]
val✝ : Component.type α Component.rcn
h : s₁.rtr[Component.rcn][i] = some val✝
⊢ val✝.body (input s₁ i) = val✝.body (input s₂ i)
Tactic:
simp [e.indep_input_eq hi h $ he ▸ h]
State after:
no goals