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

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

State before:
σPE σAE σPS✝ σAS✝ σS✝ σP✝ : Interface.Scheme
input : Input σPS✝ σAS✝ σS✝ σP✝
var' var : σPE.vars
val : Interface.Scheme.type σPE var
⊢ ¬var' = var → (if h : var' = var then some ((_ : var = var') ▸ val) else none) = none
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 : σPE.vars
val : Interface.Scheme.type σPE var
⊢ ¬var' = var → (if h : var' = var then some ((_ : var = var') ▸ val) else none) = none
Tactic:
done
State after:
no goals

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

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