case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.111946
ι : Type ?u.111949
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ (range fun s => ⨅ (_ : s ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ s), u b) ⊆ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}

case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.111946
ι : Type ?u.111949
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
a : α
ha : ∀ (i : Set β), a ≤ ⨅ (_ : i ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ i), u b
a' : α
ha' : a' ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}
⊢ a ≤ a'
α : Type u_2
β : Type u_1
γ : Type ?u.111946
ι : Type ?u.111949
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ blimsup u f p = ⨅ (s : Set β) (_ : s ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ s), u b
refine' le_antisymm (sInf_le_sInf _) (iInf_le_iff.mpr fun a ha => le_sInf_iff.mpr fun a' ha' => _)
case refine'_1.intro
α : Type u_2
β : Type u_1
γ : Type ?u.111946
ι : Type ?u.111949
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
s : Set β
⊢ (fun s => ⨅ (_ : s ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ s), u b) s ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.111946
ι : Type ?u.111949
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ (range fun s => ⨅ (_ : s ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ s), u b) ⊆ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}
rintro - ⟨s, rfl⟩
case refine'_1.intro
α : Type u_2
β : Type u_1
γ : Type ?u.111946
ι : Type ?u.111949
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
s : Set β
⊢ ∀ᶠ (x : β) in f, p x → s ∈ f → u x ≤ ⨆ (b : β) (_ : p b ∧ b ∈ s), u b
case refine'_1.intro
α : Type u_2
β : Type u_1
γ : Type ?u.111946
ι : Type ?u.111949
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
s : Set β
⊢ (fun s => ⨅ (_ : s ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ s), u b) s ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}
simp only [mem_setOf_eq, le_iInf_iff]
case refine'_1.intro
α : Type u_2
β : Type u_1
γ : Type ?u.111946
ι : Type ?u.111949
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
s : Set β
⊢ ∀ᶠ (x : β) in f, s ∈ f → p x → u x ≤ ⨆ (b : β) (_ : p b ∧ b ∈ s), u b
case refine'_1.intro
α : Type u_2
β : Type u_1
γ : Type ?u.111946
ι : Type ?u.111949
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
s : Set β
⊢ ∀ᶠ (x : β) in f, p x → s ∈ f → u x ≤ ⨆ (b : β) (_ : p b ∧ b ∈ s), u b
conv =>
  congr
  ext
  rw [Imp.swap]
case refine'_1.intro
α : Type u_2
β : Type u_1
γ : Type ?u.111946
ι : Type ?u.111949
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
s : Set β
h : s ∈ f
x : β
h₁ : x ∈ s
h₂ : p x
⊢ u x ≤ ⨆ (b : β) (_ : p b ∧ b ∈ s), u b
case refine'_1.intro
α : Type u_2
β : Type u_1
γ : Type ?u.111946
ι : Type ?u.111949
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
s : Set β
⊢ ∀ᶠ (x : β) in f, s ∈ f → p x → u x ≤ ⨆ (b : β) (_ : p b ∧ b ∈ s), u b
refine'
  eventually_imp_distrib_left.mpr fun h => eventually_iff_exists_mem.2 ⟨s, h, fun x h₁ h₂ => _⟩
no goals
case refine'_1.intro
α : Type u_2
β : Type u_1
γ : Type ?u.111946
ι : Type ?u.111949
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
s : Set β
h : s ∈ f
x : β
h₁ : x ∈ s
h₂ : p x
⊢ u x ≤ ⨆ (b : β) (_ : p b ∧ b ∈ s), u b
exact @le_iSup₂ α β (fun b => p b ∧ b ∈ s) _ (fun b _ => u b) x ⟨h₂, h₁⟩
case refine'_2.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.111946
ι : Type ?u.111949
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
a : α
ha : ∀ (i : Set β), a ≤ ⨅ (_ : i ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ i), u b
a' : α
ha' : a' ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}
s : Set β
hs : s ∈ f
hs' : ∀ (y : β), y ∈ s → p y → u y ≤ a'
⊢ a ≤ a'
case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.111946
ι : Type ?u.111949
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
a : α
ha : ∀ (i : Set β), a ≤ ⨅ (_ : i ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ i), u b
a' : α
ha' : a' ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}
⊢ a ≤ a'
obtain ⟨s, hs, hs'⟩ := eventually_iff_exists_mem.mp ha'
case refine'_2.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.111946
ι : Type ?u.111949
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
a : α
ha : ∀ (i : Set β), a ≤ ⨅ (_ : i ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ i), u b
a' : α
ha' : a' ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}
s : Set β
hs : s ∈ f
hs' : ∀ (y : β), y ∈ s → p y → u y ≤ a'
this : ∀ (y : β), p y → y ∈ s → u y ≤ a'
⊢ a ≤ a'
case refine'_2.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.111946
ι : Type ?u.111949
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
a : α
ha : ∀ (i : Set β), a ≤ ⨅ (_ : i ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ i), u b
a' : α
ha' : a' ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}
s : Set β
hs : s ∈ f
hs' : ∀ (y : β), y ∈ s → p y → u y ≤ a'
⊢ a ≤ a'
have : ∀ (y : β), p y → y ∈ s → u y ≤ a' := fun y ↦ by rw [Imp.swap]; exact hs' y
no goals
case refine'_2.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.111946
ι : Type ?u.111949
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
a : α
ha : ∀ (i : Set β), a ≤ ⨅ (_ : i ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ i), u b
a' : α
ha' : a' ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}
s : Set β
hs : s ∈ f
hs' : ∀ (y : β), y ∈ s → p y → u y ≤ a'
this : ∀ (y : β), p y → y ∈ s → u y ≤ a'
⊢ a ≤ a'
exact (le_iInf_iff.mp (ha s) hs).trans (by simpa only [iSup₂_le_iff, and_imp] )
α : Type u_2
β : Type u_1
γ : Type ?u.111946
ι : Type ?u.111949
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
a : α
ha : ∀ (i : Set β), a ≤ ⨅ (_ : i ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ i), u b
a' : α
ha' : a' ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}
s : Set β
hs : s ∈ f
hs' : ∀ (y : β), y ∈ s → p y → u y ≤ a'
y : β
⊢ y ∈ s → p y → u y ≤ a'
α : Type u_2
β : Type u_1
γ : Type ?u.111946
ι : Type ?u.111949
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
a : α
ha : ∀ (i : Set β), a ≤ ⨅ (_ : i ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ i), u b
a' : α
ha' : a' ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}
s : Set β
hs : s ∈ f
hs' : ∀ (y : β), y ∈ s → p y → u y ≤ a'
y : β
⊢ p y → y ∈ s → u y ≤ a'
rw [Imp.swap]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.111946
ι : Type ?u.111949
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
a : α
ha : ∀ (i : Set β), a ≤ ⨅ (_ : i ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ i), u b
a' : α
ha' : a' ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}
s : Set β
hs : s ∈ f
hs' : ∀ (y : β), y ∈ s → p y → u y ≤ a'
y : β
⊢ y ∈ s → p y → u y ≤ a'
exact hs' y
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.111946
ι : Type ?u.111949
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
a : α
ha : ∀ (i : Set β), a ≤ ⨅ (_ : i ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ i), u b
a' : α
ha' : a' ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}
s : Set β
hs : s ∈ f
hs' : ∀ (y : β), y ∈ s → p y → u y ≤ a'
this : ∀ (y : β), p y → y ∈ s → u y ≤ a'
⊢ (⨆ (b : β) (_ : p b ∧ b ∈ s), u b) ≤ a'
simpa only [iSup₂_le_iff, and_imp]