case a.mk
ι : Type u_2
α : ι → Type u_1
β : Type ?u.9726
s✝ s₁ s₂ : Finset ι
t✝ t₁ t₂ : (i : ι) → Finset (α i)
inst✝ : DecidableEq ((i : ι) × α i)
s : Finset ι
t : (i : ι) → Finset (α i)
x : ι
y : α x
⊢ { fst := x, snd := y } ∈ Finset.sigma s t ↔
    { fst := x, snd := y } ∈ Finset.biUnion s fun i => map (Embedding.sigmaMk i) (t i)
ι : Type u_2
α : ι → Type u_1
β : Type ?u.9726
s✝ s₁ s₂ : Finset ι
t✝ t₁ t₂ : (i : ι) → Finset (α i)
inst✝ : DecidableEq ((i : ι) × α i)
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ Finset.sigma s t = Finset.biUnion s fun i => map (Embedding.sigmaMk i) (t i)
ext ⟨x, y⟩
no goals
case a.mk
ι : Type u_2
α : ι → Type u_1
β : Type ?u.9726
s✝ s₁ s₂ : Finset ι
t✝ t₁ t₂ : (i : ι) → Finset (α i)
inst✝ : DecidableEq ((i : ι) × α i)
s : Finset ι
t : (i : ι) → Finset (α i)
x : ι
y : α x
⊢ { fst := x, snd := y } ∈ Finset.sigma s t ↔
    { fst := x, snd := y } ∈ Finset.biUnion s fun i => map (Embedding.sigmaMk i) (t i)
simp [and_left_comm]