α : Type u_1
β : Type u_2
γ : Type ?u.166973
ι : Type ?u.166976
inst✝ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
a : α
⊢ (a ⊔ ⨆ (s : Set β) (_ : s ∈ f), ⨅ (a : β) (_ : a ∈ s), u a) =
    ⨆ (s : Set β) (_ : s ∈ f), ⨅ (a_1 : β) (_ : a_1 ∈ s), a ⊔ u a_1
α : Type u_1
β : Type u_2
γ : Type ?u.166973
ι : Type ?u.166976
inst✝ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
a : α
⊢ a ⊔ liminf u f = liminf (fun x => a ⊔ u x) f
simp only [liminf_eq_iSup_iInf]
α : Type u_1
β : Type u_2
γ : Type ?u.166973
ι : Type ?u.166976
inst✝ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
a : α
⊢ (⨆ (i : Set β) (_ : i ∈ f), (⨅ (a : β) (_ : a ∈ i), u a) ⊔ a) =
    ⨆ (s : Set β) (_ : s ∈ f), ⨅ (a_1 : β) (_ : a_1 ∈ s), a ⊔ u a_1
α : Type u_1
β : Type u_2
γ : Type ?u.166973
ι : Type ?u.166976
inst✝ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
a : α
⊢ (a ⊔ ⨆ (s : Set β) (_ : s ∈ f), ⨅ (a : β) (_ : a ∈ s), u a) =
    ⨆ (s : Set β) (_ : s ∈ f), ⨅ (a_1 : β) (_ : a_1 ∈ s), a ⊔ u a_1
rw [sup_comm, biSup_sup (⟨univ, univ_mem⟩ : ∃ i : Set β, i ∈ f)]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.166973
ι : Type ?u.166976
inst✝ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
a : α
⊢ (⨆ (i : Set β) (_ : i ∈ f), (⨅ (a : β) (_ : a ∈ i), u a) ⊔ a) =
    ⨆ (s : Set β) (_ : s ∈ f), ⨅ (a_1 : β) (_ : a_1 ∈ s), a ⊔ u a_1
simp_rw [iInf₂_sup_eq, sup_comm (a := a)]