[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f g : Filter α
⊢ IsBounded r ⊥ ↔ Nonempty α
[PROOFSTEP]
simp [IsBounded, exists_true_iff_nonempty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f g : Filter α
⊢ IsBounded r ⊤ ↔ ∃ t, ∀ (x : α), r x t
[PROOFSTEP]
simp [IsBounded, eq_univ_iff_forall]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f g : Filter α
s : Set α
⊢ IsBounded r (𝓟 s) ↔ ∃ t, ∀ (x : α), x ∈ s → r x t
[PROOFSTEP]
simp [IsBounded, subset_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f g : Filter α
inst✝ : Preorder β
l : Filter α
u v : α → β
hu : IsBoundedUnder (fun x x_1 => x ≤ x_1) l u
hv : v ≤ᶠ[l] u
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) l v
[PROOFSTEP]
apply hu.imp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f g : Filter α
inst✝ : Preorder β
l : Filter α
u v : α → β
hu : IsBoundedUnder (fun x x_1 => x ≤ x_1) l u
hv : v ≤ᶠ[l] u
⊢ ∀ (a : β), (∀ᶠ (x : β) in map u l, (fun x x_1 => x ≤ x_1) x a) → ∀ᶠ (x : β) in map v l, (fun x x_1 => x ≤ x_1) x a
[PROOFSTEP]
exact fun b hb => (eventually_map.1 hb).mp <| hv.mono fun x => le_trans
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : NeBot l
hf : Tendsto f l atTop
⊢ ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
[PROOFSTEP]
rintro ⟨b, hb⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : NeBot l
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (x : β) in map f l, (fun x x_1 => x ≤ x_1) x b
⊢ False
[PROOFSTEP]
rw [eventually_map] at hb 
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : NeBot l
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (f a) b
⊢ False
[PROOFSTEP]
obtain ⟨b', h⟩ := exists_gt b
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : NeBot l
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (f a) b
b' : β
h : b < b'
⊢ False
[PROOFSTEP]
have hb' := (tendsto_atTop.mp hf) b'
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : NeBot l
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (f a) b
b' : β
h : b < b'
hb' : ∀ᶠ (a : α) in l, b' ≤ f a
⊢ False
[PROOFSTEP]
have : {x : α | f x ≤ b} ∩ {x : α | b' ≤ f x} = ∅ :=
  eq_empty_of_subset_empty fun x hx => (not_le_of_lt h) (le_trans hx.2 hx.1)
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : NeBot l
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (f a) b
b' : β
h : b < b'
hb' : ∀ᶠ (a : α) in l, b' ≤ f a
this : {x | f x ≤ b} ∩ {x | b' ≤ f x} = ∅
⊢ False
[PROOFSTEP]
exact (nonempty_of_mem (hb.and hb')).ne_empty this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝ : SemilatticeSup β
f : α → β
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) cofinite f
⊢ BddAbove (range f)
[PROOFSTEP]
rcases hf with ⟨b, hb⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝ : SemilatticeSup β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x x_1 => x ≤ x_1) x b
⊢ BddAbove (range f)
[PROOFSTEP]
haveI : Nonempty β := ⟨b⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝ : SemilatticeSup β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x x_1 => x ≤ x_1) x b
this : Nonempty β
⊢ BddAbove (range f)
[PROOFSTEP]
rw [← image_univ, ← union_compl_self {x | f x ≤ b}, image_union, bddAbove_union]
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝ : SemilatticeSup β
f : α → β
b : β
hb : ∀ᶠ (x : β) in map f cofinite, (fun x x_1 => x ≤ x_1) x b
this : Nonempty β
⊢ BddAbove (f '' {x | f x ≤ b}) ∧ BddAbove (f '' {x | f x ≤ b}ᶜ)
[PROOFSTEP]
exact ⟨⟨b, ball_image_iff.2 fun x => id⟩, (hb.image f).bddAbove⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝ : SemilatticeSup β
f : ℕ → β
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop f
⊢ BddAbove (range f)
[PROOFSTEP]
rw [← Nat.cofinite_eq_atTop] at hf 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f✝ g : Filter α
inst✝ : SemilatticeSup β
f : ℕ → β
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) cofinite f
⊢ BddAbove (range f)
[PROOFSTEP]
exact hf.bddAbove_range_of_cofinite
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f g : Filter α
⊢ IsCobounded r ⊥ ↔ ∃ b, ∀ (x : α), r b x
[PROOFSTEP]
simp [IsCobounded]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f g : Filter α
⊢ IsCobounded r ⊤ ↔ Nonempty α
[PROOFSTEP]
simp (config := { contextual := true }) [IsCobounded, eq_univ_iff_forall, exists_true_iff_nonempty]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r : α → α → Prop
f g : Filter α
s : Set α
⊢ IsCobounded r (𝓟 s) ↔ ∃ b, ∀ (a : α), (∀ (x : α), x ∈ s → r x a) → r b a
[PROOFSTEP]
simp [IsCobounded, subset_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
l : Filter γ
u : γ → α
a : α
⊢ (∀ᶠ (x : β) in map (fun x => ↑e (u x)) l, (fun x x_1 => x ≤ x_1) x (↑e a)) ↔
    ∀ᶠ (x : α) in map u l, (fun x x_1 => x ≤ x_1) x a
[PROOFSTEP]
simp only [eventually_map, e.le_iff_le]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SemilatticeSup α
f : Filter β
u v : β → α
bu : α
hu : ∀ᶠ (x : β) in f, u x ≤ bu
bv : α
hv : ∀ᶠ (x : β) in f, v x ≤ bv
⊢ ∀ᶠ (x : β) in f, u x ⊔ v x ≤ bu ⊔ bv
[PROOFSTEP]
filter_upwards [hu, hv] with _ using sup_le_sup
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
⊢ (blimsup u f fun x => True) = limsup u f
[PROOFSTEP]
simp [blimsup_eq, limsup_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
⊢ (bliminf u f fun x => True) = liminf u f
[PROOFSTEP]
simp [bliminf_eq, liminf_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ blimsup u f p = limsup (u ∘ Subtype.val) (comap Subtype.val f)
[PROOFSTEP]
simp only [blimsup_eq, limsup_eq, Function.comp_apply, eventually_comap, SetCoe.forall, Subtype.coe_mk, mem_setOf_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ sInf {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = sInf {a | ∀ᶠ (b : β) in f, ∀ (a_1 : { x // p x }), ↑a_1 = b → u ↑a_1 ≤ a}
[PROOFSTEP]
congr
[GOAL]
case e_a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
⊢ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = {a | ∀ᶠ (b : β) in f, ∀ (a_1 : { x // p x }), ↑a_1 = b → u ↑a_1 ≤ a}
[PROOFSTEP]
ext a
[GOAL]
case e_a.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
a : α
⊢ a ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ a ∈ {a | ∀ᶠ (b : β) in f, ∀ (a_1 : { x // p x }), ↑a_1 = b → u ↑a_1 ≤ a}
[PROOFSTEP]
simp_rw [Subtype.forall]
[GOAL]
case e_a.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
p : β → Prop
a : α
⊢ a ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ a ∈ {a | ∀ᶠ (b : β) in f, ∀ (a_1 : β), p a_1 → a_1 = b → u a_1 ≤ a}
[PROOFSTEP]
exact
  eventually_congr
    (eventually_of_forall fun x => ⟨fun hx y hy hxy => hxy.symm ▸ hx (hxy ▸ hy), fun hx hx' => hx x hx' rfl⟩)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
s : Set α
h : BddAbove s
hs : Set.Nonempty s
⊢ limsSup (𝓟 s) = sSup s
[PROOFSTEP]
simp only [limsSup, eventually_principal]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
s : Set α
h : BddAbove s
hs : Set.Nonempty s
⊢ sInf {a | ∀ (x : α), x ∈ s → x ≤ a} = sSup s
[PROOFSTEP]
exact csInf_upper_bounds_eq_csSup h hs
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : ConditionallyCompleteLattice α✝
α : Type u_5
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
⊢ limsup u f = limsup v f
[PROOFSTEP]
rw [limsup_eq]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : ConditionallyCompleteLattice α✝
α : Type u_5
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
⊢ sInf {a | ∀ᶠ (n : α) in f, u n ≤ a} = limsup v f
[PROOFSTEP]
congr with b
[GOAL]
case e_a.h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : ConditionallyCompleteLattice α✝
α : Type u_5
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
b : β
⊢ b ∈ {a | ∀ᶠ (n : α) in f, u n ≤ a} ↔ b ∈ {a | ∀ᶠ (n : β) in map v f, n ≤ a}
[PROOFSTEP]
exact eventually_congr (h.mono fun x hx => by simp [hx])
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : ConditionallyCompleteLattice α✝
α : Type u_5
inst✝ : ConditionallyCompleteLattice β
f : Filter α
u v : α → β
h : ∀ᶠ (a : α) in f, u a = v a
b : β
x : α
hx : u x = v x
⊢ u x ≤ b ↔ v x ∈ {x | (fun n => n ≤ b) x}
[PROOFSTEP]
simp [hx]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
⊢ blimsup u f p = blimsup v f p
[PROOFSTEP]
rw [blimsup_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
⊢ sInf {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = blimsup v f p
[PROOFSTEP]
congr with b
[GOAL]
case e_a.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
b : α
⊢ b ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ b ∈ {a | ∀ᶠ (x : β) in f, p x → v x ≤ a}
[PROOFSTEP]
refine' eventually_congr (h.mono fun x hx => ⟨fun h₁ h₂ => _, fun h₁ h₂ => _⟩)
[GOAL]
case e_a.h.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
b : α
x : β
hx : p x → u x = v x
h₁ : p x → u x ≤ b
h₂ : p x
⊢ v x ≤ b
[PROOFSTEP]
rw [← hx h₂]
[GOAL]
case e_a.h.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
b : α
x : β
hx : p x → u x = v x
h₁ : p x → u x ≤ b
h₂ : p x
⊢ u x ≤ b
[PROOFSTEP]
exact h₁ h₂
[GOAL]
case e_a.h.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
b : α
x : β
hx : p x → u x = v x
h₁ : p x → v x ≤ b
h₂ : p x
⊢ u x ≤ b
[PROOFSTEP]
rw [hx h₂]
[GOAL]
case e_a.h.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u v : β → α
p : β → Prop
h : ∀ᶠ (a : β) in f, p a → u a = v a
b : α
x : β
hx : p x → u x = v x
h₁ : p x → v x ≤ b
h₂ : p x
⊢ v x ≤ b
[PROOFSTEP]
exact h₁ h₂
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : ConditionallyCompleteLattice α✝
α : Type u_5
inst✝¹ : ConditionallyCompleteLattice β
f : Filter α
inst✝ : NeBot f
b : β
⊢ limsup (fun x => b) f = b
[PROOFSTEP]
simpa only [limsup_eq, eventually_const] using csInf_Ici
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
⊢ ⊥ ∈ {a | ∀ᶠ (n : α) in ⊥, n ≤ a}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : β → α
⊢ limsup f ⊥ = ⊥
[PROOFSTEP]
simp [limsup]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
⊢ ⊤ ∈ {a | ∀ᶠ (n : α) in ⊥, a ≤ n}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : β → α
⊢ liminf f ⊥ = ⊤
[PROOFSTEP]
simp [liminf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
⊢ ∀ (b : α), b ∈ {a | ∀ᶠ (n : α) in ⊤, n ≤ a} → ⊤ ≤ b
[PROOFSTEP]
simp [eq_univ_iff_forall]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
⊢ ∀ (b : α), (∀ (x : α), x ≤ b) → b = ⊤
[PROOFSTEP]
exact fun b hb => top_unique <| hb _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
⊢ ∀ (b : α), b ∈ {a | ∀ᶠ (n : α) in ⊤, a ≤ n} → b ≤ ⊥
[PROOFSTEP]
simp [eq_univ_iff_forall]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
⊢ ∀ (b : α), (∀ (x : α), b ≤ x) → b = ⊥
[PROOFSTEP]
exact fun b hb => bot_unique <| hb _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ (blimsup u f fun x => False) = ⊥
[PROOFSTEP]
simp [blimsup_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ (bliminf u f fun x => False) = ⊤
[PROOFSTEP]
simp [bliminf_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
⊢ limsup (fun x => ⊥) f = ⊥
[PROOFSTEP]
rw [limsup_eq, eq_bot_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
⊢ sInf {a | ∀ᶠ (n : β) in f, ⊥ ≤ a} ≤ ⊥
[PROOFSTEP]
exact sInf_le (eventually_of_forall fun _ => le_rfl)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u
[PROOFSTEP]
isBoundedDefault
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ IsCoboundedUnder (fun x x_1 => x ≥ x_1) f u
[PROOFSTEP]
isBoundedDefault
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ ⨅ (i : Set β) (_ : i ∈ f), sSup (u '' id i) = ⨅ (s : Set β) (_ : s ∈ f), ⨆ (a : β) (_ : a ∈ s), u a
[PROOFSTEP]
simp only [sSup_image, id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
u : ℕ → α
⊢ ⨅ (i : ℕ) (_ : True), sSup (u '' Ici i) = ⨅ (n : ℕ), ⨆ (i : ℕ) (_ : i ≥ n), u i
[PROOFSTEP]
simp only [sSup_image, iInf_const]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
u : ℕ → α
⊢ ⨅ (i : ℕ), ⨆ (a : ℕ) (_ : a ∈ Ici i), u a = ⨅ (n : ℕ), ⨆ (i : ℕ) (_ : i ≥ n), u i
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
u : ℕ → α
⊢ limsup u atTop = ⨅ (n : ℕ), ⨆ (i : ℕ), u (i + n)
[PROOFSTEP]
simp only [limsup_eq_iInf_iSup_of_nat, iSup_ge_eq_iSup_nat_add]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
p : ι → Prop
s : ι → Set β
f : Filter β
u : β → α
h : HasBasis f p s
⊢ ⨅ (i : ι) (_ : p i), sSup (u '' s i) = ⨅ (i : ι) (_ : p i), ⨆ (a : β) (_ : a ∈ s i), u a
[PROOFSTEP]
simp only [sSup_image, id]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
⊢ blimsup u f p = blimsup u f q
[PROOFSTEP]
simp only [blimsup_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
⊢ sInf {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = sInf {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}
[PROOFSTEP]
congr
[GOAL]
case e_a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
⊢ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}
[PROOFSTEP]
ext a
[GOAL]
case e_a.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
⊢ a ∈ {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ a ∈ {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}
[PROOFSTEP]
refine' eventually_congr (h.mono fun b hb => _)
[GOAL]
case e_a.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
⊢ p b → u b ≤ a ↔ q b → u b ≤ a
[PROOFSTEP]
cases' eq_or_ne (u b) ⊥ with hu hu
[GOAL]
case e_a.h.inl
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b = ⊥
⊢ p b → u b ≤ a ↔ q b → u b ≤ a
[PROOFSTEP]
simp [hu]
[GOAL]
case e_a.h.inr
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p q : β → Prop
u : β → α
h : ∀ᶠ (x : β) in f, u x ≠ ⊥ → (p x ↔ q x)
a : α
b : β
hb : u b ≠ ⊥ → (p b ↔ q b)
hu : u b ≠ ⊥
⊢ p b → u b ≤ a ↔ q b → u b ≤ a
[PROOFSTEP]
rw [hb hu]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
⊢ blimsup u f p = ⨅ (s : Set β) (_ : s ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ s), u b
[PROOFSTEP]
refine' le_antisymm (sInf_le_sInf _) (iInf_le_iff.mpr fun a ha => le_sInf_iff.mpr fun a' ha' => _)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
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}
[PROOFSTEP]
rintro - ⟨s, rfl⟩
[GOAL]
case refine'_1.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
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}
[PROOFSTEP]
simp only [mem_setOf_eq, le_iInf_iff]
[GOAL]
case refine'_1.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
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
[PROOFSTEP]
conv =>
  congr
  ext
  rw [Imp.swap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
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
[PROOFSTEP]
  congr
  ext
  rw [Imp.swap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
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
[PROOFSTEP]
  congr
  ext
  rw [Imp.swap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
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
[PROOFSTEP]
congr
[GOAL]
case p
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
s : Set β
| fun x => p x → s ∈ f → u x ≤ ⨆ (b : β) (_ : p b ∧ b ∈ s), u b
case f
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
s : Set β
| f
[PROOFSTEP]
ext
[GOAL]
case p.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
s : Set β
x✝ : β
| p x✝ → s ∈ f → u x✝ ≤ ⨆ (b : β) (_ : p b ∧ b ∈ s), u b
case f
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : Filter β
p : β → Prop
u : β → α
s : Set β
| f
[PROOFSTEP]
rw [Imp.swap]
[GOAL]
case refine'_1.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
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
[PROOFSTEP]
refine' eventually_imp_distrib_left.mpr fun h => eventually_iff_exists_mem.2 ⟨s, h, fun x h₁ h₂ => _⟩
[GOAL]
case refine'_1.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
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
[PROOFSTEP]
exact @le_iSup₂ α β (fun b => p b ∧ b ∈ s) _ (fun b _ => u b) x ⟨h₂, h₁⟩
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
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'
[PROOFSTEP]
obtain ⟨s, hs, hs'⟩ := eventually_iff_exists_mem.mp ha'
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
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'
[PROOFSTEP]
have : ∀ (y : β), p y → y ∈ s → u y ≤ a' := fun y ↦ by rw [Imp.swap]; exact hs' y
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
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'
[PROOFSTEP]
rw [Imp.swap]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
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'
[PROOFSTEP]
exact hs' y
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
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'
[PROOFSTEP]
exact (le_iInf_iff.mp (ha s) hs).trans (by simpa only [iSup₂_le_iff, and_imp])
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
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'
[PROOFSTEP]
simpa only [iSup₂_le_iff, and_imp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
p : ℕ → Prop
u : ℕ → α
⊢ blimsup u atTop p = ⨅ (i : ℕ), ⨆ (j : ℕ) (_ : p j ∧ i ≤ j), u j
[PROOFSTEP]
simp only [blimsup_eq_limsup_subtype, Function.comp, (atTop_basis.comap ((↑) : {x | p x} → ℕ)).limsup_eq_iInf_iSup,
  iSup_subtype, iSup_and]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
p : ℕ → Prop
u : ℕ → α
⊢ ⨅ (i : ℕ) (_ : True),
      ⨆ (i_1 : ℕ) (x : i_1 ∈ {x | p x}) (_ : { val := i_1, property := (_ : i_1 ∈ {x | p x}) } ∈ Subtype.val ⁻¹' Ici i),
        u i_1 =
    ⨅ (i : ℕ), ⨆ (j : ℕ) (_ : p j) (_ : i ≤ j), u j
[PROOFSTEP]
simp only [mem_setOf_eq, mem_preimage, mem_Ici, not_le, iInf_pos]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
inst✝¹ : CompleteLattice α
ι : Type u_5
R : Type u_6
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ limsup a F = sInf ((fun I => sSup (a '' I)) '' F.sets)
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
inst✝¹ : CompleteLattice α
ι : Type u_5
R : Type u_6
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ limsup a F ≤ sInf ((fun I => sSup (a '' I)) '' F.sets)
[PROOFSTEP]
rw [limsup_eq]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
inst✝¹ : CompleteLattice α
ι : Type u_5
R : Type u_6
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ sInf {a_1 | ∀ᶠ (n : ι) in F, a n ≤ a_1} ≤ sInf ((fun I => sSup (a '' I)) '' F.sets)
[PROOFSTEP]
refine' sInf_le_sInf fun x hx => _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
inst✝¹ : CompleteLattice α
ι : Type u_5
R : Type u_6
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
x : R
hx : x ∈ (fun I => sSup (a '' I)) '' F.sets
⊢ x ∈ {a_1 | ∀ᶠ (n : ι) in F, a n ≤ a_1}
[PROOFSTEP]
rcases(mem_image _ F.sets x).mp hx with ⟨I, ⟨I_mem_F, hI⟩⟩
[GOAL]
case refine'_1.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
inst✝¹ : CompleteLattice α
ι : Type u_5
R : Type u_6
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
x : R
hx : x ∈ (fun I => sSup (a '' I)) '' F.sets
I : Set ι
I_mem_F : I ∈ F.sets
hI : sSup (a '' I) = x
⊢ x ∈ {a_1 | ∀ᶠ (n : ι) in F, a n ≤ a_1}
[PROOFSTEP]
filter_upwards [I_mem_F] with i hi
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
inst✝¹ : CompleteLattice α
ι : Type u_5
R : Type u_6
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
x : R
hx : x ∈ (fun I => sSup (a '' I)) '' F.sets
I : Set ι
I_mem_F : I ∈ F.sets
hI : sSup (a '' I) = x
i : ι
hi : i ∈ I
⊢ a i ≤ x
[PROOFSTEP]
exact hI ▸ le_sSup (mem_image_of_mem _ hi)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
inst✝¹ : CompleteLattice α
ι : Type u_5
R : Type u_6
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
⊢ sInf ((fun I => sSup (a '' I)) '' F.sets) ≤ limsup a F
[PROOFSTEP]
refine' le_sInf_iff.mpr fun b hb => sInf_le_of_le (mem_image_of_mem _ <| Filter.mem_sets.mpr hb) <| sSup_le _
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
inst✝¹ : CompleteLattice α
ι : Type u_5
R : Type u_6
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
b : R
hb : b ∈ {a_1 | ∀ᶠ (n : R) in map a F, n ≤ a_1}
⊢ ∀ (b_1 : R), b_1 ∈ a '' (a ⁻¹' {x | (fun n => n ≤ b) x}) → b_1 ≤ b
[PROOFSTEP]
rintro _ ⟨_, h, rfl⟩
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
inst✝¹ : CompleteLattice α
ι : Type u_5
R : Type u_6
F : Filter ι
inst✝ : CompleteLattice R
a : ι → R
b : R
hb : b ∈ {a_1 | ∀ᶠ (n : R) in map a F, n ≤ a_1}
w✝ : ι
h : w✝ ∈ a ⁻¹' {x | (fun n => n ≤ b) x}
⊢ a w✝ ≤ b
[PROOFSTEP]
exact h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
⊢ liminf (fun i => f (i + k)) atTop = liminf f atTop
[PROOFSTEP]
simp_rw [liminf_eq_iSup_iInf_of_nat]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : ℕ → α
k : ℕ
⊢ ⨆ (n : ℕ), ⨅ (i : ℕ) (_ : i ≥ n), f (i + k) = ⨆ (n : ℕ), ⨅ (i : ℕ) (_ : i ≥ n), f i
[PROOFSTEP]
exact iSup_iInf_ge_nat_add f k
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α✝
α : Type u_5
β : Type u_6
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
⊢ liminf u f ≤ x
[PROOFSTEP]
rw [liminf_eq]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α✝
α : Type u_5
β : Type u_6
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
⊢ sSup {a | ∀ᶠ (n : α) in f, a ≤ u n} ≤ x
[PROOFSTEP]
refine' sSup_le fun b hb => _
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α✝
α : Type u_5
β : Type u_6
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
b : β
hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}
⊢ b ≤ x
[PROOFSTEP]
have hbx : ∃ᶠ _ in f, b ≤ x := by
  revert h
  rw [← not_imp_not, not_frequently, not_frequently]
  exact fun h => hb.mp (h.mono fun a hbx hba hax => hbx (hba.trans hax))
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α✝
α : Type u_5
β : Type u_6
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
b : β
hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}
⊢ ∃ᶠ (x_1 : α) in f, b ≤ x
[PROOFSTEP]
revert h
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α✝
α : Type u_5
β : Type u_6
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x b : β
hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}
⊢ (∃ᶠ (a : α) in f, u a ≤ x) → ∃ᶠ (x_1 : α) in f, b ≤ x
[PROOFSTEP]
rw [← not_imp_not, not_frequently, not_frequently]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α✝
α : Type u_5
β : Type u_6
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x b : β
hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}
⊢ (∀ᶠ (x_1 : α) in f, ¬b ≤ x) → ∀ᶠ (x_1 : α) in f, ¬u x_1 ≤ x
[PROOFSTEP]
exact fun h => hb.mp (h.mono fun a hbx hba hax => hbx (hba.trans hax))
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α✝
α : Type u_5
β : Type u_6
inst✝ : CompleteLattice β
f : Filter α
u : α → β
x : β
h : ∃ᶠ (a : α) in f, u a ≤ x
b : β
hb : b ∈ {a | ∀ᶠ (n : α) in f, a ≤ u n}
hbx : ∃ᶠ (x_1 : α) in f, b ≤ x
⊢ b ≤ x
[PROOFSTEP]
exact hbx.exists.choose_spec
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ↑f (limsup (fun n => (↑f)^[n] a) atTop) = limsup (fun n => (↑f)^[n] a) atTop
[PROOFSTEP]
rw [limsup_eq_iInf_iSup_of_nat', map_iInf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨅ (i : ℕ), ↑f (⨆ (i_1 : ℕ), (↑f)^[i_1 + i] a) = ⨅ (n : ℕ), ⨆ (i : ℕ), (↑f)^[i + n] a
[PROOFSTEP]
simp_rw [_root_.map_iSup, ← Function.comp_apply (f := f), ← Function.iterate_succ' f, ← Nat.add_succ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨅ (i : ℕ), ⨆ (i_1 : ℕ), (↑f)^[i_1 + Nat.succ i] a = ⨅ (n : ℕ), ⨆ (i : ℕ), (↑f)^[i + n] a
[PROOFSTEP]
conv_rhs => rw [iInf_split _ ((· < ·) (0 : ℕ))]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
| ⨅ (n : ℕ), ⨆ (i : ℕ), (↑f)^[i + n] a
[PROOFSTEP]
rw [iInf_split _ ((· < ·) (0 : ℕ))]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
| ⨅ (n : ℕ), ⨆ (i : ℕ), (↑f)^[i + n] a
[PROOFSTEP]
rw [iInf_split _ ((· < ·) (0 : ℕ))]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
| ⨅ (n : ℕ), ⨆ (i : ℕ), (↑f)^[i + n] a
[PROOFSTEP]
rw [iInf_split _ ((· < ·) (0 : ℕ))]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨅ (i : ℕ), ⨆ (i_1 : ℕ), (↑f)^[i_1 + Nat.succ i] a =
    (⨅ (i : ℕ) (_ : (fun x x_1 => x < x_1) 0 i), ⨆ (i_1 : ℕ), (↑f)^[i_1 + i] a) ⊓
      ⨅ (i : ℕ) (_ : ¬(fun x x_1 => x < x_1) 0 i), ⨆ (i_1 : ℕ), (↑f)^[i_1 + i] a
[PROOFSTEP]
simp only [not_lt, le_zero_iff, iInf_iInf_eq_left, add_zero, iInf_nat_gt_zero_eq, left_eq_inf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨅ (i : ℕ), ⨆ (i_1 : ℕ), (↑f)^[i_1 + Nat.succ i] a ≤ ⨆ (i : ℕ), (↑f)^[i] a
[PROOFSTEP]
refine' (iInf_le (fun i => ⨆ j, f^[j + (i + 1)] a) 0).trans _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ⨆ (j : ℕ), (↑f)^[j + (0 + 1)] a ≤ ⨆ (i : ℕ), (↑f)^[i] a
[PROOFSTEP]
simp only [zero_add, Function.comp_apply, iSup_le_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f : CompleteLatticeHom α α
a : α
⊢ ∀ (i : ℕ), (↑f)^[i + 1] a ≤ ⨆ (i : ℕ), (↑f)^[i] a
[PROOFSTEP]
exact fun i => le_iSup (fun i => f^[i] a) (i + 1)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
h : ∀ (x : β), p x → q x
a : α
ha : a ∈ {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}
⊢ ∀ (x : β), (q x → u x ≤ a) → p x → u x ≤ a
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
h : ∀ (x : β), p x → q x
a : α
ha : a ∈ {a | ∀ᶠ (x : β) in f, q x → a ≤ u x}
⊢ ∀ (x : β), (q x → a ≤ u x) → p x → a ≤ u x
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
⊢ ∀ (x : β), p x ∧ q x → p x
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
⊢ ∀ (x : β), p x ∧ q x → q x
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
⊢ ∀ (x : β), p x → p x ∨ q x
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
⊢ ∀ (x : β), q x → p x ∨ q x
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
e : α ≃o γ
⊢ ↑e (blimsup u f p) = blimsup (↑e ∘ u) f p
[PROOFSTEP]
simp only [blimsup_eq, map_sInf, Function.comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
e : α ≃o γ
⊢ sInf ((fun a => ↑e a) '' {a | ∀ᶠ (x : β) in f, p x → u x ≤ a}) = sInf {a | ∀ᶠ (x : β) in f, p x → ↑e (u x) ≤ a}
[PROOFSTEP]
congr
[GOAL]
case e_a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
e : α ≃o γ
⊢ (fun a => ↑e a) '' {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} = {a | ∀ᶠ (x : β) in f, p x → ↑e (u x) ≤ a}
[PROOFSTEP]
ext c
[GOAL]
case e_a.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
e : α ≃o γ
c : γ
⊢ c ∈ (fun a => ↑e a) '' {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ c ∈ {a | ∀ᶠ (x : β) in f, p x → ↑e (u x) ≤ a}
[PROOFSTEP]
obtain ⟨a, rfl⟩ := e.surjective c
[GOAL]
case e_a.h.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α
f g : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
e : α ≃o γ
a : α
⊢ ↑e a ∈ (fun a => ↑e a) '' {a | ∀ᶠ (x : β) in f, p x → u x ≤ a} ↔ ↑e a ∈ {a | ∀ᶠ (x : β) in f, p x → ↑e (u x) ≤ a}
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α
f g✝ : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
g : sSupHom α γ
⊢ ↑g (blimsup u f p) ≤ blimsup (↑g ∘ u) f p
[PROOFSTEP]
simp only [blimsup_eq_iInf_biSup, Function.comp]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α
f g✝ : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
g : sSupHom α γ
⊢ ↑g (⨅ (s : Set β) (_ : s ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ s), u b) ≤
    ⨅ (s : Set β) (_ : s ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ s), ↑g (u b)
[PROOFSTEP]
refine' ((OrderHomClass.mono g).map_iInf₂_le _).trans _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteLattice α
f g✝ : Filter β
p q : β → Prop
u v : β → α
inst✝ : CompleteLattice γ
g : sSupHom α γ
⊢ ⨅ (i : Set β) (_ : i ∈ f), ↑g (⨆ (b : β) (_ : p b ∧ b ∈ i), u b) ≤
    ⨅ (s : Set β) (_ : s ∈ f), ⨆ (b : β) (_ : p b ∧ b ∈ s), ↑g (u b)
[PROOFSTEP]
simp only [_root_.map_iSup, le_refl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ (blimsup u f fun x => p x ∨ q x) = blimsup u f p ⊔ blimsup u f q
[PROOFSTEP]
refine' le_antisymm _ blimsup_sup_le_or
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ (blimsup u f fun x => p x ∨ q x) ≤ blimsup u f p ⊔ blimsup u f q
[PROOFSTEP]
simp only [blimsup_eq, sInf_sup_eq, sup_sInf_eq, le_iInf₂_iff, mem_setOf_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
⊢ ∀ (i : α),
    (∀ᶠ (x : β) in f, q x → u x ≤ i) →
      ∀ (i_1 : α), (∀ᶠ (x : β) in f, p x → u x ≤ i_1) → sInf {a | ∀ᶠ (x : β) in f, p x ∨ q x → u x ≤ a} ≤ i_1 ⊔ i
[PROOFSTEP]
refine' fun a' ha' a ha => sInf_le ((ha.and ha').mono fun b h hb => _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
a' : α
ha' : ∀ᶠ (x : β) in f, q x → u x ≤ a'
a : α
ha : ∀ᶠ (x : β) in f, p x → u x ≤ a
b : β
h : (p b → u b ≤ a) ∧ (q b → u b ≤ a')
hb : p b ∨ q b
⊢ u b ≤ a ⊔ a'
[PROOFSTEP]
exact Or.elim hb (fun hb => le_sup_of_le_left <| h.1 hb) fun hb => le_sup_of_le_right <| h.2 hb
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
inst✝ : NeBot f
a : α
⊢ a ⊔ limsup u f = limsup (fun x => a ⊔ u x) f
[PROOFSTEP]
simp only [limsup_eq_iInf_iSup, iSup_sup_eq, sup_iInf₂_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
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
[PROOFSTEP]
congr
[GOAL]
case e_s
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
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
[PROOFSTEP]
ext s
[GOAL]
case e_s.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
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
[PROOFSTEP]
congr
[GOAL]
case e_s.h.e_s
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
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
[PROOFSTEP]
ext hs
[GOAL]
case e_s.h.e_s.h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
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
[PROOFSTEP]
congr
[GOAL]
case e_s.h.e_s.h.e_a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
inst✝ : NeBot f
a : α
s : Set β
hs : s ∈ f
⊢ a = ⨆ (x : β) (_ : x ∈ s), a
[PROOFSTEP]
exact (biSup_const (nonempty_of_mem hs)).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteDistribLattice α
f : Filter β
p q : β → Prop
u : β → α
a : α
⊢ a ⊔ liminf u f = liminf (fun x => a ⊔ u x) f
[PROOFSTEP]
simp only [liminf_eq_iSup_iInf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
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
[PROOFSTEP]
rw [sup_comm, biSup_sup (⟨univ, univ_mem⟩ : ∃ i : Set β, i ∈ f)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
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
[PROOFSTEP]
simp_rw [iInf₂_sup_eq, sup_comm (a := a)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
⊢ (limsup u f)ᶜ = liminf (compl ∘ u) f
[PROOFSTEP]
simp only [limsup_eq_iInf_iSup, compl_iInf, compl_iSup, liminf_eq_iSup_iInf, Function.comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
⊢ (liminf u f)ᶜ = limsup (compl ∘ u) f
[PROOFSTEP]
simp only [limsup_eq_iInf_iSup, compl_iInf, compl_iSup, liminf_eq_iSup_iInf, Function.comp_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ limsup u f \ a = limsup (fun b => u b \ a) f
[PROOFSTEP]
simp only [limsup_eq_iInf_iSup, sdiff_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
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ᶜ
[PROOFSTEP]
rw [biInf_inf (⟨univ, univ_mem⟩ : ∃ i : Set β, i ∈ f)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
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ᶜ
[PROOFSTEP]
simp_rw [inf_comm, inf_iSup₂_eq, inf_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst✝ : NeBot f
a : α
⊢ liminf u f \ a = liminf (fun b => u b \ a) f
[PROOFSTEP]
simp only [sdiff_eq, inf_comm (b := aᶜ), inf_liminf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst✝ : NeBot f
a : α
⊢ a \ limsup u f = liminf (fun b => a \ u b) f
[PROOFSTEP]
rw [← compl_inj_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
inst✝ : NeBot f
a : α
⊢ (a \ limsup u f)ᶜ = (liminf (fun b => a \ u b) f)ᶜ
[PROOFSTEP]
simp only [sdiff_eq, liminf_compl, (· ∘ ·), compl_inf, compl_compl, sup_limsup]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ a \ liminf u f = limsup (fun b => a \ u b) f
[PROOFSTEP]
rw [← compl_inj_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : CompleteBooleanAlgebra α
f : Filter β
u : β → α
a : α
⊢ (a \ liminf u f)ᶜ = (limsup (fun b => a \ u b) f)ᶜ
[PROOFSTEP]
simp only [sdiff_eq, limsup_compl, (· ∘ ·), compl_inf, compl_compl, sup_liminf]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ blimsup s cofinite p = {x | Set.Infinite {n | p n ∧ x ∈ s n}}
[PROOFSTEP]
simp only [blimsup_eq, le_eq_subset, eventually_cofinite, not_forall, sInf_eq_sInter, exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ ⋂₀ {a | Set.Finite {x | p x ∧ ¬s x ⊆ a}} = {x | Set.Infinite {n | p n ∧ x ∈ s n}}
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
⊢ x ∈ ⋂₀ {a | Set.Finite {x | p x ∧ ¬s x ⊆ a}} ↔ x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
[PROOFSTEP]
refine' ⟨fun h => _, fun hx t h => _⟩
[GOAL]
case h.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : x ∈ ⋂₀ {a | Set.Finite {x | p x ∧ ¬s x ⊆ a}}
⊢ x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
[PROOFSTEP]
contrapose! h
[GOAL]
case h.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
hx : x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
t : Set α
h : t ∈ {a | Set.Finite {x | p x ∧ ¬s x ⊆ a}}
⊢ x ∈ t
[PROOFSTEP]
contrapose! h
[GOAL]
case h.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : ¬x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
⊢ ¬x ∈ ⋂₀ {a | Set.Finite {x | p x ∧ ¬s x ⊆ a}}
[PROOFSTEP]
simp only [mem_sInter, mem_setOf_eq, not_forall, exists_prop]
[GOAL]
case h.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : ¬x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
⊢ ∃ x_1, Set.Finite {x | p x ∧ ¬s x ⊆ x_1} ∧ ¬x ∈ x_1
[PROOFSTEP]
exact ⟨{ x }ᶜ, by simpa using h, by simp⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : ¬x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
⊢ Set.Finite {x_1 | p x_1 ∧ ¬s x_1 ⊆ {x}ᶜ}
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
h : ¬x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
⊢ ¬x ∈ {x}ᶜ
[PROOFSTEP]
simp
[GOAL]
case h.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
x : α
hx : x ∈ {x | Set.Infinite {n | p n ∧ x ∈ s n}}
t : Set α
h : ¬x ∈ t
⊢ ¬t ∈ {a | Set.Finite {x | p x ∧ ¬s x ⊆ a}}
[PROOFSTEP]
exact hx.mono fun i hi => ⟨hi.1, fun hit => h (hit hi.2)⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ bliminf s cofinite p = {x | Set.Finite {n | p n ∧ ¬x ∈ s n}}
[PROOFSTEP]
rw [← compl_inj_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ (bliminf s cofinite p)ᶜ = {x | Set.Finite {n | p n ∧ ¬x ∈ s n}}ᶜ
[PROOFSTEP]
simp only [bliminf_eq_iSup_biInf, compl_iInf, compl_iSup, ← blimsup_eq_iInf_biSup, cofinite.blimsup_set_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ {x | Set.Infinite {n | p n ∧ x ∈ (s n)ᶜ}} = {x | Set.Finite {n | p n ∧ ¬x ∈ s n}}ᶜ
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ limsup s cofinite = {x | Set.Infinite {n | x ∈ s n}}
[PROOFSTEP]
simp only [← cofinite.blimsup_true s, cofinite.blimsup_set_eq, true_and_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ liminf s cofinite = {x | Set.Finite {n | ¬x ∈ s n}}
[PROOFSTEP]
simp only [← cofinite.bliminf_true s, cofinite.bliminf_set_eq, true_and_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
q : ι → Prop
hl : HasBasis l q b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ blimsup u l p
⊢ ∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
[PROOFSTEP]
rw [blimsup_eq_iInf_biSup] at hx 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
q : ι → Prop
hl : HasBasis l q b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ ⨅ (s : Set β) (_ : s ∈ l), ⨆ (b : β) (_ : p b ∧ b ∈ s), u b
⊢ ∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
[PROOFSTEP]
simp only [iSup_eq_iUnion, iInf_eq_iInter, mem_iInter, mem_iUnion, exists_prop] at hx 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
q : ι → Prop
hl : HasBasis l q b
u : β → Set α
p : β → Prop
x : α
hx : ∀ (i : Set β), i ∈ l → ∃ i_2, (p i_2 ∧ i_2 ∈ i) ∧ x ∈ u i_2
⊢ ∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
[PROOFSTEP]
choose g hg hg' using hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
q : ι → Prop
hl : HasBasis l q b
u : β → Set α
p : β → Prop
x : α
g : (i : Set β) → i ∈ l → β
hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i
hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)
⊢ ∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
[PROOFSTEP]
refine' ⟨fun i : {i | q i} => g (b i) (hl.mem_of_mem i.2), fun i => ⟨_, _⟩⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
q : ι → Prop
hl : HasBasis l q b
u : β → Set α
p : β → Prop
x : α
g : (i : Set β) → i ∈ l → β
hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i
hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)
i : ↑{i | q i}
⊢ x ∈ u ((fun i => g (b ↑i) (_ : b ↑i ∈ l)) i)
[PROOFSTEP]
exact hg' (b i) (hl.mem_of_mem i.2)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
q : ι → Prop
hl : HasBasis l q b
u : β → Set α
p : β → Prop
x : α
g : (i : Set β) → i ∈ l → β
hg : ∀ (i : Set β) (i_1 : i ∈ l), p (g i i_1) ∧ g i i_1 ∈ i
hg' : ∀ (i : Set β) (i_1 : i ∈ l), x ∈ u (g i i_1)
i : ↑{i | q i}
⊢ p ((fun i => g (b ↑i) (_ : b ↑i ∈ l)) i) ∧ (fun i => g (b ↑i) (_ : b ↑i ∈ l)) i ∈ b ↑i
[PROOFSTEP]
exact hg (b i) (hl.mem_of_mem i.2)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
hl : HasBasis l (fun x => True) b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ blimsup u l p
⊢ ∃ f, ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i
[PROOFSTEP]
obtain ⟨f, hf⟩ := exists_forall_mem_of_hasBasis_mem_blimsup hl hx
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
p✝ : ι → Prop
s : ι → Set α
l : Filter β
b : ι → Set β
hl : HasBasis l (fun x => True) b
u : β → Set α
p : β → Prop
x : α
hx : x ∈ blimsup u l p
f : ↑{i | True} → β
hf : ∀ (i : ↑{i | True}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
⊢ ∃ f, ∀ (i : ι), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b i
[PROOFSTEP]
exact ⟨fun i => f ⟨i, trivial⟩, fun i => hf ⟨i, trivial⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder α
a : α
hf : autoParam (IsCobounded (fun x x_1 => x ≤ x_1) f) _auto✝
h : a < limsSup f
⊢ ∃ᶠ (n : α) in f, a < n
[PROOFSTEP]
contrapose! h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder α
a : α
hf : autoParam (IsCobounded (fun x x_1 => x ≤ x_1) f) _auto✝
h : ¬∃ᶠ (n : α) in f, a < n
⊢ limsSup f ≤ a
[PROOFSTEP]
simp only [not_frequently, not_lt] at h 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder α
a : α
hf : autoParam (IsCobounded (fun x x_1 => x ≤ x_1) f) _auto✝
h : ∀ᶠ (x : α) in f, x ≤ a
⊢ limsSup f ≤ a
[PROOFSTEP]
exact limsSup_le_of_le hf h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
⊢ ∀ᶠ (a : α) in f, b < u a
[PROOFSTEP]
obtain ⟨c, hc, hbc⟩ : ∃ (c : β) (_ : c ∈ {c : β | ∀ᶠ n : α in f, c ≤ u n}), b < c :=
  by
  simp_rw [exists_prop]
  exact exists_lt_of_lt_csSup hu h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
⊢ ∃ c x, b < c
[PROOFSTEP]
simp_rw [exists_prop]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
⊢ ∃ c, c ∈ {c | ∀ᶠ (n : α) in f, c ≤ u n} ∧ b < c
[PROOFSTEP]
exact exists_lt_of_lt_csSup hu h
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
f : Filter α
inst✝ : ConditionallyCompleteLinearOrder β
u : α → β
b : β
h : b < liminf u f
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
c : β
hc : c ∈ {c | ∀ᶠ (n : α) in f, c ≤ u n}
hbc : b < c
⊢ ∀ᶠ (a : α) in f, b < u a
[PROOFSTEP]
exact hc.mono fun x hx => lt_of_lt_of_le hbc hx
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
α : Type u_5
β : Type u_6
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu_le : ∃ᶠ (x : α) in f, b ≤ u x
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
⊢ b ≤ limsup u f
[PROOFSTEP]
revert hu_le
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
α : Type u_5
β : Type u_6
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
⊢ (∃ᶠ (x : α) in f, b ≤ u x) → b ≤ limsup u f
[PROOFSTEP]
rw [← not_imp_not, not_frequently]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
α : Type u_5
β : Type u_6
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
⊢ ¬b ≤ limsup u f → ∀ᶠ (x : α) in f, ¬b ≤ u x
[PROOFSTEP]
simp_rw [← lt_iff_not_ge]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
α : Type u_5
β : Type u_6
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
⊢ limsup u f < b → ∀ᶠ (x : α) in f, u x < b
[PROOFSTEP]
exact fun h => eventually_lt_of_limsup_lt h hu
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
α : Type u_5
β : Type u_6
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h : b < limsup u f
⊢ ∃ᶠ (x : α) in f, b < u x
[PROOFSTEP]
contrapose! h
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
α : Type u_5
β : Type u_6
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h : ¬∃ᶠ (x : α) in f, b < u x
⊢ limsup u f ≤ b
[PROOFSTEP]
apply limsSup_le_of_le hu
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
α : Type u_5
β : Type u_6
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h : ¬∃ᶠ (x : α) in f, b < u x
⊢ ∀ᶠ (n : β) in map u f, n ≤ b
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) l (g ∘ f) ↔ IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
[PROOFSTEP]
refine' ⟨_, fun h => h.isBoundedUnder (α := β) hg⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) l (g ∘ f) → IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
[PROOFSTEP]
rintro ⟨c, hc⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (x : γ) in map (g ∘ f) l, (fun x x_1 => x ≤ x_1) x c
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
[PROOFSTEP]
rw [eventually_map] at hc 
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((g ∘ f) a) c
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
[PROOFSTEP]
obtain ⟨b, hb⟩ : ∃ b, ∀ a ≥ b, c < g a := eventually_atTop.1 (hg'.eventually_gt_atTop c)
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((g ∘ f) a) c
b : β
hb : ∀ (a : β), a ≥ b → c < g a
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
[PROOFSTEP]
exact ⟨b, hc.mono fun x hx => not_lt.1 fun h => (hb _ h.le).not_le hx⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => l (v x)) _auto✝
hv_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f v) _auto✝
⊢ l (limsup v f) ≤ limsup (fun x => l (v x)) f
[PROOFSTEP]
refine' le_limsSup_of_le hlv fun c hc => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => l (v x)) _auto✝
hv_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f v) _auto✝
c : γ
hc : ∀ᶠ (n : γ) in map (fun x => l (v x)) f, n ≤ c
⊢ l (limsup v f) ≤ c
[PROOFSTEP]
rw [Filter.eventually_map] at hc 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => l (v x)) _auto✝
hv_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f v) _auto✝
c : γ
hc : ∀ᶠ (a : α) in f, l (v a) ≤ c
⊢ l (limsup v f) ≤ c
[PROOFSTEP]
simp_rw [gc _ _] at hc ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
v : α → β
l : β → γ
u : γ → β
gc : GaloisConnection l u
hlv : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => l (v x)) _auto✝
hv_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f v) _auto✝
c : γ
hc : ∀ᶠ (a : α) in f, v a ≤ u c
⊢ limsup v f ≤ u c
[PROOFSTEP]
exact limsSup_le_of_le hv_co hc
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
ι : Type u_4
γ : Type u_5
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
⊢ ↑g (limsup u f) = limsup (fun x => ↑g (u x)) f
[PROOFSTEP]
refine' le_antisymm ((OrderIso.to_galoisConnection g).l_limsup_le hgu hu_co) _
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
ι : Type u_4
γ : Type u_5
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
⊢ limsup (fun x => ↑g (u x)) f ≤ ↑g (limsup u f)
[PROOFSTEP]
rw [← g.symm.symm_apply_apply <| limsup (fun x => g (u x)) f, g.symm_symm]
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
ι : Type u_4
γ : Type u_5
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
⊢ ↑g (↑(symm g) (limsup (fun x => ↑g (u x)) f)) ≤ ↑g (limsup u f)
[PROOFSTEP]
refine' g.monotone _
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
ι : Type u_4
γ : Type u_5
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
⊢ ↑(symm g) (limsup (fun x => ↑g (u x)) f) ≤ limsup u f
[PROOFSTEP]
have hf : u = fun i => g.symm (g (u i)) := funext fun i => (g.symm_apply_apply (u i)).symm
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
ι : Type u_4
γ : Type u_5
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hf : u = fun i => ↑(symm g) (↑g (u i))
⊢ ↑(symm g) (limsup (fun x => ↑g (u x)) f) ≤ limsup u f
[PROOFSTEP]
nth_rw 2 [hf]
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
ι : Type u_4
γ : Type u_5
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hf : u = fun i => ↑(symm g) (↑g (u i))
⊢ ↑(symm g) (limsup (fun x => ↑g (u x)) f) ≤ limsup (fun i => ↑(symm g) (↑g (u i))) f
[PROOFSTEP]
refine' (OrderIso.to_galoisConnection g.symm).l_limsup_le _ hgu_co
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
ι : Type u_4
γ : Type u_5
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hf : u = fun i => ↑(symm g) (↑g (u i))
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑(symm g) (↑g (u x))
[PROOFSTEP]
simp_rw [g.symm_apply_apply]
[GOAL]
α : Type u_1
β : Type u_2
γ✝ : Type u_3
ι : Type u_4
γ : Type u_5
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : ConditionallyCompleteLattice γ
f : Filter α
u : α → β
g : β ≃o γ
hu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
hgu : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hgu_co : autoParam (IsCoboundedUnder (fun x x_1 => x ≤ x_1) f fun x => ↑g (u x)) _auto✝
hf : u = fun i => ↑(symm g) (↑g (u i))
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) f fun x => u x
[PROOFSTEP]
exact hu
