Theorem: sets_eq (BrownCs22/Demos/01-intro.lean)

State before:
p q r : Prop
s t u : Set ℕ
⊢ (s ∪ t) ∩ u = s ∩ u ∪ t ∩ u
Tactic:
ext x
State after:
case h
p q r : Prop
s t u : Set ℕ
x : ℕ
⊢ x ∈ (s ∪ t) ∩ u ↔ x ∈ s ∩ u ∪ t ∩ u

State before:
case h
p q r : Prop
s t u : Set ℕ
x : ℕ
⊢ x ∈ (s ∪ t) ∩ u ↔ x ∈ s ∩ u ∪ t ∩ u
Tactic:
constructor
State after:
case h.mp
p q r : Prop
s t u : Set ℕ
x : ℕ
⊢ x ∈ (s ∪ t) ∩ u → x ∈ s ∩ u ∪ t ∩ u

case h.mpr
p q r : Prop
s t u : Set ℕ
x : ℕ
⊢ x ∈ s ∩ u ∪ t ∩ u → x ∈ (s ∪ t) ∩ u