case h.mk
α : Type u_1
β : Type u_2
γ : Type ?u.30243
δ : Type ?u.30246
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
a : α
b : β
s : Set α
t : Set β
x : β
y : α
⊢ (x, y) ∈ Prod.swap ⁻¹' s ×ˢ t ↔ (x, y) ∈ t ×ˢ s
α : Type u_1
β : Type u_2
γ : Type ?u.30243
δ : Type ?u.30246
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
a : α
b : β
s : Set α
t : Set β
⊢ Prod.swap ⁻¹' s ×ˢ t = t ×ˢ s
ext ⟨x, y⟩
no goals
case h.mk
α : Type u_1
β : Type u_2
γ : Type ?u.30243
δ : Type ?u.30246
s✝ s₁ s₂ : Set α
t✝ t₁ t₂ : Set β
a : α
b : β
s : Set α
t : Set β
x : β
y : α
⊢ (x, y) ∈ Prod.swap ⁻¹' s ×ˢ t ↔ (x, y) ∈ t ×ˢ s
simp [and_comm]