case a.mk
α : Type u_1
β : Type u_2
γ : Type ?u.68532
s s' : Finset α
t t' : Finset β
a✝ : α
b : β
a x : α
y : β
⊢ (x, y) ∈ {a} ×ˢ t ↔ (x, y) ∈ map { toFun := Prod.mk a, inj' := (_ : Function.Injective (Prod.mk a)) } t
α : Type u_1
β : Type u_2
γ : Type ?u.68532
s s' : Finset α
t t' : Finset β
a✝ : α
b : β
a : α
⊢ {a} ×ˢ t = map { toFun := Prod.mk a, inj' := (_ : Function.Injective (Prod.mk a)) } t
ext ⟨x, y⟩
no goals
case a.mk
α : Type u_1
β : Type u_2
γ : Type ?u.68532
s s' : Finset α
t t' : Finset β
a✝ : α
b : β
a x : α
y : β
⊢ (x, y) ∈ {a} ×ˢ t ↔ (x, y) ∈ map { toFun := Prod.mk a, inj' := (_ : Function.Injective (Prod.mk a)) } t
simp [and_left_comm, eq_comm]