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