Theorem: Set.insert_union' (ReactorModel/Extensions.lean)

State before:
α : Type u_1
s₁ s₂ : Set α
a : α
⊢ insert a s₁ ∪ s₂ = s₁ ∪ insert a s₂
Tactic:
rw [Set.insert_union, Set.union_comm, ←Set.insert_union, Set.union_comm]
State after:
no goals