no goals
ι : Type u_1
ι' : Type ?u.32460
α : ι → Type u_2
β : ι → Type ?u.32470
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a : α i
x : (i : ι) × α i
⊢ x ∈ Set.Sigma s₁ t₁ \ Set.Sigma s₂ t₂ ↔ x ∈ Set.Sigma s₁ (t₁ \ t₂) ∪ Set.Sigma (s₁ \ s₂) t₁
by_cases h₁ : x.1 ∈ s₁ <;> by_cases h₂ : x.2 ∈ t₁ x.1 <;> simp [*, ← imp_iff_or_not]