ι : Type u_1
ι' : Type ?u.9903
α : ι → Type u_2
β : ι → Type ?u.9913
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a : α i
⊢ α i
ι : Type u_1
ι' : Type ?u.9903
α : ι → Type u_2
β : ι → Type ?u.9913
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a : α i
⊢ Set.Sigma (insert i s) t = Sigma.mk i '' t i ∪ Set.Sigma s t
rw [insert_eq, union_sigma, singleton_sigma]
no goals
ι : Type u_1
ι' : Type ?u.9903
α : ι → Type u_2
β : ι → Type ?u.9913
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
u : Set ((i : ι) × α i)
x : (i : ι) × α i
i j : ι
a : α i
⊢ α i
exact a