Theorem: Execution.State.input_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✝
⊢ input s₁ i = input s₂ i
Tactic:
simp [input, input.restriction, hr, ht]
State after:
no goals