case inl
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : IsTop (limsup u f)
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f

case inr
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : ∃ b, limsup u f < b
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f
obtain ha | ha := isTop_or_exists_gt (f.limsup u)
case pos
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : ∃ b, limsup u f < b
H : IsGLB (Set.Ioi (limsup u f)) (limsup u f)
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f

case neg
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : ∃ b, limsup u f < b
H : ¬IsGLB (Set.Ioi (limsup u f)) (limsup u f)
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f
case inr
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : ∃ b, limsup u f < b
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f
by_cases H : IsGLB (Set.Ioi (f.limsup u)) (f.limsup u)
no goals
case inl
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : IsTop (limsup u f)
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f
exact eventually_of_forall fun _ => ha _
case pos.intro.intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u✝ : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u✝) _auto✝
ha : ∃ b, limsup u✝ f < b
H : IsGLB (Set.Ioi (limsup u✝ f)) (limsup u✝ f)
u : ℕ → α
hua : Tendsto u atTop (𝓝 (limsup u✝ f))
hu : ∀ (n : ℕ), u n ∈ Set.Ioi (limsup u✝ f)
⊢ ∀ᶠ (b : β) in f, u✝ b ≤ limsup u✝ f
case pos
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : ∃ b, limsup u f < b
H : IsGLB (Set.Ioi (limsup u f)) (limsup u f)
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f
obtain ⟨u, -, -, hua, hu⟩ := H.exists_seq_antitone_tendsto ha
case pos.intro.intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u✝ : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u✝) _auto✝
ha : ∃ b, limsup u✝ f < b
H : IsGLB (Set.Ioi (limsup u✝ f)) (limsup u✝ f)
u : ℕ → α
hua : Tendsto u atTop (𝓝 (limsup u✝ f))
hu : ∀ (n : ℕ), u n ∈ Set.Ioi (limsup u✝ f)
this : ∀ (n : ℕ), ∀ᶠ (a : β) in f, u✝ a < u n
⊢ ∀ᶠ (b : β) in f, u✝ b ≤ limsup u✝ f
case pos.intro.intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u✝ : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u✝) _auto✝
ha : ∃ b, limsup u✝ f < b
H : IsGLB (Set.Ioi (limsup u✝ f)) (limsup u✝ f)
u : ℕ → α
hua : Tendsto u atTop (𝓝 (limsup u✝ f))
hu : ∀ (n : ℕ), u n ∈ Set.Ioi (limsup u✝ f)
⊢ ∀ᶠ (b : β) in f, u✝ b ≤ limsup u✝ f
have := fun n => eventually_lt_of_limsup_lt (hu n) hf
no goals
case pos.intro.intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u✝ : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u✝) _auto✝
ha : ∃ b, limsup u✝ f < b
H : IsGLB (Set.Ioi (limsup u✝ f)) (limsup u✝ f)
u : ℕ → α
hua : Tendsto u atTop (𝓝 (limsup u✝ f))
hu : ∀ (n : ℕ), u n ∈ Set.Ioi (limsup u✝ f)
this : ∀ (n : ℕ), ∀ᶠ (a : β) in f, u✝ a < u n
⊢ ∀ᶠ (b : β) in f, u✝ b ≤ limsup u✝ f
exact
  (eventually_countable_forall.2 this).mono fun b hb =>
    ge_of_tendsto hua <| eventually_of_forall fun n => (hb _).le
case neg.intro.intro
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : ∃ b, limsup u f < b
H : ¬IsGLB (Set.Ioi (limsup u f)) (limsup u f)
x : α
hx : ∀ ⦃b : α⦄, limsup u f < b → x ≤ b
xa : limsup u f < x
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f
case neg
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : ∃ b, limsup u f < b
H : ¬IsGLB (Set.Ioi (limsup u f)) (limsup u f)
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f
obtain ⟨x, hx, xa⟩ : ∃ x, (∀ ⦃b⦄, f.limsup u < b → x ≤ b) ∧ f.limsup u < x := by
  simp only [IsGLB, IsGreatest, lowerBounds, upperBounds, Set.mem_Ioi, Set.mem_setOf_eq,
    not_and, not_forall, not_le, exists_prop] at H
  exact H fun x => le_of_lt
case h
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : ∃ b, limsup u f < b
H : ¬IsGLB (Set.Ioi (limsup u f)) (limsup u f)
x : α
hx : ∀ ⦃b : α⦄, limsup u f < b → x ≤ b
xa : limsup u f < x
y : β
hy : u y < x
⊢ u y ≤ limsup u f
case neg.intro.intro
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : ∃ b, limsup u f < b
H : ¬IsGLB (Set.Ioi (limsup u f)) (limsup u f)
x : α
hx : ∀ ⦃b : α⦄, limsup u f < b → x ≤ b
xa : limsup u f < x
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f
filter_upwards [eventually_lt_of_limsup_lt xa hf] with y hy
case h
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : ∃ b, limsup u f < b
H : ¬IsGLB (Set.Ioi (limsup u f)) (limsup u f)
x : α
hx : ∀ ⦃b : α⦄, limsup u f < b → x ≤ b
xa : limsup u f < x
y : β
hy : limsup u f < u y
⊢ x ≤ u y
case h
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : ∃ b, limsup u f < b
H : ¬IsGLB (Set.Ioi (limsup u f)) (limsup u f)
x : α
hx : ∀ ⦃b : α⦄, limsup u f < b → x ≤ b
xa : limsup u f < x
y : β
hy : u y < x
⊢ u y ≤ limsup u f
contrapose! hy
no goals
case h
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : ∃ b, limsup u f < b
H : ¬IsGLB (Set.Ioi (limsup u f)) (limsup u f)
x : α
hx : ∀ ⦃b : α⦄, limsup u f < b → x ≤ b
xa : limsup u f < x
y : β
hy : limsup u f < u y
⊢ x ≤ u y
exact hx hy
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : ∃ b, limsup u f < b
H : (∀ ⦃a : α⦄, limsup u f < a → limsup u f ≤ a) → ∃ x, (∀ ⦃a : α⦄, limsup u f < a → x ≤ a) ∧ limsup u f < x
⊢ ∃ x, (∀ ⦃b : α⦄, limsup u f < b → x ≤ b) ∧ limsup u f < x
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : ∃ b, limsup u f < b
H : ¬IsGLB (Set.Ioi (limsup u f)) (limsup u f)
⊢ ∃ x, (∀ ⦃b : α⦄, limsup u f < b → x ≤ b) ∧ limsup u f < x
simp only [IsGLB, IsGreatest, lowerBounds, upperBounds, Set.mem_Ioi, Set.mem_setOf_eq,
  not_and, not_forall, not_le, exists_prop] at H
no goals
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : ∃ b, limsup u f < b
H : (∀ ⦃a : α⦄, limsup u f < a → limsup u f ≤ a) → ∃ x, (∀ ⦃a : α⦄, limsup u f < a → x ≤ a) ∧ limsup u f < x
⊢ ∃ x, (∀ ⦃b : α⦄, limsup u f < b → x ≤ b) ∧ limsup u f < x
exact H fun x => le_of_lt