Theorem: Execution.State.Triggers.congr (ReactorModel/Execution/Theorems/State.lean)

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