case a
α : Type u_1
β : Type u_2
γ : Type ?u.11252
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝ : DecidableEq α
ht : Finset.Nonempty t
i : α
⊢ i ∈ image Prod.fst (s ×ˢ t) ↔ i ∈ s
α : Type u_1
β : Type u_2
γ : Type ?u.11252
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝ : DecidableEq α
ht : Finset.Nonempty t
⊢ image Prod.fst (s ×ˢ t) = s
ext i
no goals
case a
α : Type u_1
β : Type u_2
γ : Type ?u.11252
s s' : Finset α
t t' : Finset β
a : α
b : β
inst✝ : DecidableEq α
ht : Finset.Nonempty t
i : α
⊢ i ∈ image Prod.fst (s ×ˢ t) ↔ i ∈ s
simp [mem_image, ht.bex]