case h.mk
ι : Type u_1
ι' : Type ?u.8988
α : ι → Type u_2
β : ι → Type ?u.8998
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a : α i
x : ι
y : α x
⊢ { fst := x, snd := y } ∈ Set.Sigma s₁ t₁ ∩ Set.Sigma s₂ t₂ ↔
    { fst := x, snd := y } ∈ Set.Sigma (s₁ ∩ s₂) fun i => t₁ i ∩ t₂ i
ι : Type u_1
ι' : Type ?u.8988
α : ι → Type u_2
β : ι → Type ?u.8998
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a : α i
⊢ Set.Sigma s₁ t₁ ∩ Set.Sigma s₂ t₂ = Set.Sigma (s₁ ∩ s₂) fun i => t₁ i ∩ t₂ i
ext ⟨x, y⟩
no goals
case h.mk
ι : Type u_1
ι' : Type ?u.8988
α : ι → Type u_2
β : ι → Type ?u.8998
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x✝ : (i : ι) × α i
i j : ι
a : α i
x : ι
y : α x
⊢ { fst := x, snd := y } ∈ Set.Sigma s₁ t₁ ∩ Set.Sigma s₂ t₂ ↔
    { fst := x, snd := y } ∈ Set.Sigma (s₁ ∩ s₂) fun i => t₁ i ∩ t₂ i
simp [and_assoc, and_left_comm]