Theorem: Execution.Step.Apply.preserves_tag (ReactorModel/Execution/Theorems/Step/Apply.lean)

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₁' s₂ s₂' s₁₂ s₂₁ : State α
c : Change
e : s₁ -[c]→ s₂
⊢ s₁.tag = s₂.tag
Tactic:
cases e <;> simp [schedule_preserves_tag]
State after:
no goals