Theorem: SetTheory.inter_distrib_right (SetTheory/Basic.lean)

State before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ (x ∪ y) ∩ z = x ∩ z ∪ y ∩ z
Tactic:
ext
State after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ (x ∪ y) ∩ z ↔ z✝ ∈ x ∩ z ∪ y ∩ z

State before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ (x ∪ y) ∩ z ↔ z✝ ∈ x ∩ z ∪ y ∩ z
Tactic:
aesop
State after:
no goals