α : Type ?u.72035
β : Type u_2
γ : Type ?u.72041
ι : Sort u_1
ι' : Sort ?u.72047
ι₂ : Sort ?u.72050
κ : ι → Sort ?u.72055
κ₁ : ι → Sort ?u.72060
κ₂ : ι → Sort ?u.72065
κ' : ι' → Sort ?u.72070
inst✝ : Nonempty ι
s : Set β
t : ι → Set β
⊢ (⋂ (i : ι), s ∩ t iᶜ) = ⋂ (i : ι), s \ t i
α : Type ?u.72035
β : Type u_2
γ : Type ?u.72041
ι : Sort u_1
ι' : Sort ?u.72047
ι₂ : Sort ?u.72050
κ : ι → Sort ?u.72055
κ₁ : ι → Sort ?u.72060
κ₂ : ι → Sort ?u.72065
κ' : ι' → Sort ?u.72070
inst✝ : Nonempty ι
s : Set β
t : ι → Set β
⊢ (s \ ⋃ (i : ι), t i) = ⋂ (i : ι), s \ t i
rw [diff_eq, compl_iUnion, inter_iInter]
no goals
α : Type ?u.72035
β : Type u_2
γ : Type ?u.72041
ι : Sort u_1
ι' : Sort ?u.72047
ι₂ : Sort ?u.72050
κ : ι → Sort ?u.72055
κ₁ : ι → Sort ?u.72060
κ₂ : ι → Sort ?u.72065
κ' : ι' → Sort ?u.72070
inst✝ : Nonempty ι
s : Set β
t : ι → Set β
⊢ (⋂ (i : ι), s ∩ t iᶜ) = ⋂ (i : ι), s \ t i
rfl