Theorem: ReactionT.setState_other_state (Runtime/Reaction/Lemmas.lean)

State before:
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σS✝.vars
val : Interface.Scheme.type σS✝ var
⊢ var' ≠ var → Output.state (setState var val input).fst var' = Input.state input var'
Tactic:
simp [setState]
State after:
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σS✝.vars
val : Interface.Scheme.type σS✝ var
⊢ ¬var' = var → (if h : var' = var then (_ : var = var') ▸ val else Input.state input var') = Input.state input var'

State before:
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σS✝.vars
val : Interface.Scheme.type σS✝ var
⊢ ¬var' = var → (if h : var' = var then (_ : var = var') ▸ val else Input.state input var') = Input.state input var'
Tactic:
first | done | rfl | intro h; simp [h]
State after:
no goals

State before:
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σS✝.vars
val : Interface.Scheme.type σS✝ var
⊢ ¬var' = var → (if h : var' = var then (_ : var = var') ▸ val else Input.state input var') = Input.state input var'
Tactic:
done
State after:
no goals

State before:
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σS✝.vars
val : Interface.Scheme.type σS✝ var
⊢ ¬var' = var → (if h : var' = var then (_ : var = var') ▸ val else Input.state input var') = Input.state input var'
Tactic:
intro h
State after:
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σS✝.vars
val : Interface.Scheme.type σS✝ var
h : ¬var' = var
⊢ (if h : var' = var then (_ : var = var') ▸ val else Input.state input var') = Input.state input var'

State before:
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σS✝.vars
val : Interface.Scheme.type σS✝ var
h : ¬var' = var
⊢ (if h : var' = var then (_ : var = var') ▸ val else Input.state input var') = Input.state input var'
Tactic:
simp [h]
State after:
no goals