case h.mk
α : Type u_1
β : Type u_2
γ : Type ?u.13537
δ : Type ?u.13540
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
⊢ (x, y) ∈ s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ ↔ (x, y) ∈ (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)
α : Type u_1
β : Type u_2
γ : Type ?u.13537
δ : Type ?u.13540
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
⊢ s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ = (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)
ext ⟨x, y⟩
no goals
case h.mk
α : Type u_1
β : Type u_2
γ : Type ?u.13537
δ : Type ?u.13540
s s₁ s₂ : Set α
t t₁ t₂ : Set β
a : α
b : β
x : α
y : β
⊢ (x, y) ∈ s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ ↔ (x, y) ∈ (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)
simp [and_assoc, and_left_comm]