no goals
F : Type ?u.136149
α : Type u_1
β : Type ?u.136155
𝕜 : Type ?u.136158
E : Type ?u.136161
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s✝ t✝ : Finset α
n : ℕ
s t u : Finset α
hus : u ⊆ s ∪ t
hcard : card u = ↑mulRothNumber (s ∪ t)
hu : MulSalemSpencer ↑u
⊢ card u = card (u ∩ s ∪ u ∩ t)
rw [← inter_distrib_left, (inter_eq_left_iff_subset _ _).2 hus]