α : Type u_1
β : Type u_2
γ : Type ?u.172865
ι : Type ?u.172868
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ (⨅ (s : Set β) (_ : s ∈ f), ⨆ (a : β) (_ : a ∈ s), u a) ⊓ aᶜ =
    ⨅ (s : Set β) (_ : s ∈ f), ⨆ (a_1 : β) (_ : a_1 ∈ s), u a_1 ⊓ aᶜ
α : Type u_1
β : Type u_2
γ : Type ?u.172865
ι : Type ?u.172868
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ limsup u f \ a = limsup (fun b => u b \ a) f
simp only [limsup_eq_iInf_iSup, sdiff_eq]
α : Type u_1
β : Type u_2
γ : Type ?u.172865
ι : Type ?u.172868
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ (⨅ (i : Set β) (_ : i ∈ f), (⨆ (a : β) (_ : a ∈ i), u a) ⊓ aᶜ) =
    ⨅ (s : Set β) (_ : s ∈ f), ⨆ (a_1 : β) (_ : a_1 ∈ s), u a_1 ⊓ aᶜ
α : Type u_1
β : Type u_2
γ : Type ?u.172865
ι : Type ?u.172868
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ (⨅ (s : Set β) (_ : s ∈ f), ⨆ (a : β) (_ : a ∈ s), u a) ⊓ aᶜ =
    ⨅ (s : Set β) (_ : s ∈ f), ⨆ (a_1 : β) (_ : a_1 ∈ s), u a_1 ⊓ aᶜ
rw [biInf_inf (⟨univ, univ_mem⟩ : ∃ i : Set β, i ∈ f)]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.172865
ι : Type ?u.172868
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ (⨅ (i : Set β) (_ : i ∈ f), (⨆ (a : β) (_ : a ∈ i), u a) ⊓ aᶜ) =
    ⨅ (s : Set β) (_ : s ∈ f), ⨆ (a_1 : β) (_ : a_1 ∈ s), u a_1 ⊓ aᶜ
simp_rw [inf_comm, inf_iSup₂_eq, inf_comm]