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