case a.mk
α : Type u_1
β : Type u_2
γ : Type ?u.72393
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ (s ∪ s') ×ˢ t ↔ (x, y) ∈ s ×ˢ t ∪ s' ×ˢ t
α : Type u_1
β : Type u_2
γ : Type ?u.72393
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (s ∪ s') ×ˢ t = s ×ˢ t ∪ s' ×ˢ t
ext ⟨x, y⟩
no goals
case a.mk
α : Type u_1
β : Type u_2
γ : Type ?u.72393
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ (s ∪ s') ×ˢ t ↔ (x, y) ∈ s ×ˢ t ∪ s' ×ˢ t
simp only [or_and_right, mem_union, mem_product]