Theorem: Execution.State.output_congr (ReactorModel/Execution/Theorems/State.lean)

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
i : ID
hr : autoParam (s₁.rtr = s₂.rtr) _auto✝
ht : autoParam (s₁.tag = s₂.tag) _auto✝
⊢ output s₁ i = output s₂ i
Tactic:
simp [output, input_congr hr ht, hr]
State after:
no goals