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