no goals
ι : Type u_1
α : ι → Type u_3
β : ι → Type u_2
s s₁ s₂ : Set ι
t✝ t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ (pi s fun j => t j (update f i a j)) = pi ({i} ∪ s \ {i}) fun j => t j (update f i a j)
rw [union_diff_self, union_eq_self_of_subset_left (singleton_subset_iff.2 hi)]
case hi
ι : Type u_1
α : ι → Type u_3
β : ι → Type u_2
s s₁ s₂ : Set ι
t✝ t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ ¬i ∈ s \ {i}
ι : Type u_1
α : ι → Type u_3
β : ι → Type u_2
s s₁ s₂ : Set ι
t✝ t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ (pi ({i} ∪ s \ {i}) fun j => t j (update f i a j)) = {x | x i ∈ t i a} ∩ pi (s \ {i}) fun j => t j (f j)
rw [union_pi, singleton_pi', update_same, pi_update_of_not_mem]
no goals
case hi
ι : Type u_1
α : ι → Type u_3
β : ι → Type u_2
s s₁ s₂ : Set ι
t✝ t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
hi : i ∈ s
f : (j : ι) → α j
a : α i
t : (j : ι) → α j → Set (β j)
⊢ ¬i ∈ s \ {i}
simp