α : Type ?u.72372
β : Type u_1
γ : Type ?u.72378
ι : Sort u_2
ι' : Sort ?u.72384
ι₂ : Sort ?u.72387
κ : ι → Sort ?u.72392
κ₁ : ι → Sort ?u.72397
κ₂ : ι → Sort ?u.72402
κ' : ι' → Sort ?u.72407
s : Set β
t : ι → Set β
⊢ (⋃ (i : ι), s ∩ t iᶜ) = ⋃ (i : ι), s \ t i
α : Type ?u.72372
β : Type u_1
γ : Type ?u.72378
ι : Sort u_2
ι' : Sort ?u.72384
ι₂ : Sort ?u.72387
κ : ι → Sort ?u.72392
κ₁ : ι → Sort ?u.72397
κ₂ : ι → Sort ?u.72402
κ' : ι' → Sort ?u.72407
s : Set β
t : ι → Set β
⊢ (s \ ⋂ (i : ι), t i) = ⋃ (i : ι), s \ t i
rw [diff_eq, compl_iInter, inter_iUnion]
no goals
α : Type ?u.72372
β : Type u_1
γ : Type ?u.72378
ι : Sort u_2
ι' : Sort ?u.72384
ι₂ : Sort ?u.72387
κ : ι → Sort ?u.72392
κ₁ : ι → Sort ?u.72397
κ₂ : ι → Sort ?u.72402
κ' : ι' → Sort ?u.72407
s : Set β
t : ι → Set β
⊢ (⋃ (i : ι), s ∩ t iᶜ) = ⋃ (i : ι), s \ t i
rfl