case a
α : Type u_1
β : Type u_2
γ : Type ?u.32
s✝ t✝ s : Set α
t : Set β
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ×ˢ t)
a✝ : α × β
⊢ a✝ ∈ toFinset (s ×ˢ t) ↔ a✝ ∈ toFinset s ×ˢ toFinset t
α : Type u_1
β : Type u_2
γ : Type ?u.32
s✝ t✝ s : Set α
t : Set β
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ×ˢ t)
⊢ toFinset (s ×ˢ t) = toFinset s ×ˢ toFinset t
ext
no goals
case a
α : Type u_1
β : Type u_2
γ : Type ?u.32
s✝ t✝ s : Set α
t : Set β
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ×ˢ t)
a✝ : α × β
⊢ a✝ ∈ toFinset (s ×ˢ t) ↔ a✝ ∈ toFinset s ×ˢ toFinset t
simp