hypotheses
s
:
Set ℕ
t
:
Set ℕ
ext x
x
:
ℕ
intro h1
h1
:
x ∈ s ∩ t
rw [Set.mem_inter_iff]
h1
:
x ∈ s ∧ x ∈ t
rw [and_comm]
h1
:
x ∈ t ∧ x ∈ s
🎉
exact
h1
🎉
x ∈ t ∩ s
intro h1
x ∈ s ∩ t → x ∈ t ∩ s
h.mp
intro h2
h2
:
x ∈ t ∩ s
rw [Set.mem_inter_iff]
h2
:
x ∈ t ∧ x ∈ s
rw [and_comm]
h2
:
x ∈ s ∧ x ∈ t
🎉
exact
h2
🎉
x ∈ s ∩ t
intro h2
x ∈ t ∩ s → x ∈ s ∩ t
h.mpr
apply Iff.intro
x ∈ s ∩ t ↔ x ∈ t ∩ s
ext x
s ∩ t = t ∩ s