1 2 3 4 5 6 7 8 9 10 11 12 13 14
import Mathlib.Data.Set.Basic theorem commutativityOfIntersections (s t : Set Nat) : s ∩ t = t ∩ s := by ext x apply Iff.intro intro h1 rw [Set.mem_inter_iff, and_comm] at h1 exact h1 intro h2 rw [Set.mem_inter_iff, and_comm] at h2 -- exact h2
