α : Type u_2
β : Type u_1
γ : Type ?u.164326
ι : Type ?u.164329
inst✝¹ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
inst✝ : NeBot f
a : α
⊢ (⨅ (i : Set β) (_ : i ∈ f), a ⊔ ⨆ (a : β) (_ : a ∈ i), u a) =
    ⨅ (s : Set β) (_ : s ∈ f), (⨆ (x : β) (_ : x ∈ s), a) ⊔ ⨆ (x : β) (_ : x ∈ s), u x
α : Type u_2
β : Type u_1
γ : Type ?u.164326
ι : Type ?u.164329
inst✝¹ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
inst✝ : NeBot f
a : α
⊢ a ⊔ limsup u f = limsup (fun x => a ⊔ u x) f
simp only [limsup_eq_iInf_iSup, iSup_sup_eq, sup_iInf₂_eq]
case e_s
α : Type u_2
β : Type u_1
γ : Type ?u.164326
ι : Type ?u.164329
inst✝¹ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
inst✝ : NeBot f
a : α
⊢ (fun i => ⨅ (_ : i ∈ f), a ⊔ ⨆ (a : β) (_ : a ∈ i), u a) = fun s =>
    ⨅ (_ : s ∈ f), (⨆ (x : β) (_ : x ∈ s), a) ⊔ ⨆ (x : β) (_ : x ∈ s), u x
α : Type u_2
β : Type u_1
γ : Type ?u.164326
ι : Type ?u.164329
inst✝¹ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
inst✝ : NeBot f
a : α
⊢ (⨅ (i : Set β) (_ : i ∈ f), a ⊔ ⨆ (a : β) (_ : a ∈ i), u a) =
    ⨅ (s : Set β) (_ : s ∈ f), (⨆ (x : β) (_ : x ∈ s), a) ⊔ ⨆ (x : β) (_ : x ∈ s), u x
congr
case e_s.h
α : Type u_2
β : Type u_1
γ : Type ?u.164326
ι : Type ?u.164329
inst✝¹ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
inst✝ : NeBot f
a : α
s : Set β
⊢ (⨅ (_ : s ∈ f), a ⊔ ⨆ (a : β) (_ : a ∈ s), u a) =
    ⨅ (_ : s ∈ f), (⨆ (x : β) (_ : x ∈ s), a) ⊔ ⨆ (x : β) (_ : x ∈ s), u x
case e_s
α : Type u_2
β : Type u_1
γ : Type ?u.164326
ι : Type ?u.164329
inst✝¹ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
inst✝ : NeBot f
a : α
⊢ (fun i => ⨅ (_ : i ∈ f), a ⊔ ⨆ (a : β) (_ : a ∈ i), u a) = fun s =>
    ⨅ (_ : s ∈ f), (⨆ (x : β) (_ : x ∈ s), a) ⊔ ⨆ (x : β) (_ : x ∈ s), u x
ext s
case e_s.h.e_s
α : Type u_2
β : Type u_1
γ : Type ?u.164326
ι : Type ?u.164329
inst✝¹ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
inst✝ : NeBot f
a : α
s : Set β
⊢ (fun j => a ⊔ ⨆ (a : β) (_ : a ∈ s), u a) = fun x => (⨆ (x : β) (_ : x ∈ s), a) ⊔ ⨆ (x : β) (_ : x ∈ s), u x
case e_s.h
α : Type u_2
β : Type u_1
γ : Type ?u.164326
ι : Type ?u.164329
inst✝¹ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
inst✝ : NeBot f
a : α
s : Set β
⊢ (⨅ (_ : s ∈ f), a ⊔ ⨆ (a : β) (_ : a ∈ s), u a) =
    ⨅ (_ : s ∈ f), (⨆ (x : β) (_ : x ∈ s), a) ⊔ ⨆ (x : β) (_ : x ∈ s), u x
congr
case e_s.h.e_s.h
α : Type u_2
β : Type u_1
γ : Type ?u.164326
ι : Type ?u.164329
inst✝¹ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
inst✝ : NeBot f
a : α
s : Set β
hs : s ∈ f
⊢ (a ⊔ ⨆ (a : β) (_ : a ∈ s), u a) = (⨆ (x : β) (_ : x ∈ s), a) ⊔ ⨆ (x : β) (_ : x ∈ s), u x
case e_s.h.e_s
α : Type u_2
β : Type u_1
γ : Type ?u.164326
ι : Type ?u.164329
inst✝¹ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
inst✝ : NeBot f
a : α
s : Set β
⊢ (fun j => a ⊔ ⨆ (a : β) (_ : a ∈ s), u a) = fun x => (⨆ (x : β) (_ : x ∈ s), a) ⊔ ⨆ (x : β) (_ : x ∈ s), u x
ext hs
case e_s.h.e_s.h.e_a
α : Type u_2
β : Type u_1
γ : Type ?u.164326
ι : Type ?u.164329
inst✝¹ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
inst✝ : NeBot f
a : α
s : Set β
hs : s ∈ f
⊢ a = ⨆ (x : β) (_ : x ∈ s), a
case e_s.h.e_s.h
α : Type u_2
β : Type u_1
γ : Type ?u.164326
ι : Type ?u.164329
inst✝¹ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
inst✝ : NeBot f
a : α
s : Set β
hs : s ∈ f
⊢ (a ⊔ ⨆ (a : β) (_ : a ∈ s), u a) = (⨆ (x : β) (_ : x ∈ s), a) ⊔ ⨆ (x : β) (_ : x ∈ s), u x
congr
no goals
case e_s.h.e_s.h.e_a
α : Type u_2
β : Type u_1
γ : Type ?u.164326
ι : Type ?u.164329
inst✝¹ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
inst✝ : NeBot f
a : α
s : Set β
hs : s ∈ f
⊢ a = ⨆ (x : β) (_ : x ∈ s), a
exact (biSup_const (nonempty_of_mem hs)).symm