-- Mathlib/Topology/Algebra/Order/LiminfLimsup.lean
theorem eventually_le_limsup (hf : IsBoundedUnder (· ≤ ·) f u

Proof state:
case inr
α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
ha : ∃ b, limsup u f < b
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f

Tactic:
by_cases H : IsGLB (Set.Ioi (f.limsup u)) (f.limsup u)

Result:
case pos
α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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

Tactic:
exact H fun x => le_of_lt

Result:
no goals

Proof state:
case h
α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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

Tactic:
contrapose! hy

Result:
case h
α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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

Proof state:
case pos.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u✝ : β → α
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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

Tactic:
exact
  (eventually_countable_forall.2 this).mono fun b hb =>
    ge_of_tendsto hua <| Eventually.of_forall fun n => (hb _).le

Result:
no goals

Proof state:
case neg
α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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

Tactic:
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

Result:
case neg.intro.intro
α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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

Proof state:
case pos
α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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

Tactic:
obtain ⟨u, -, -, hua, hu⟩ := H.exists_seq_antitone_tendsto ha

Result:
case pos.intro.intro.intro.intro
α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u✝ : β → α
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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

Tactic:
simp only [IsGLB, IsGreatest, lowerBounds, upperBounds, Set.mem_Ioi, Set.mem_setOf_eq,
  not_and, not_forall, not_le, exists_prop] at H

Result:
α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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

Proof state:
case h
α : Type u_2
β : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) 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

Tactic:
exact hx hy

Result:
no goals

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

Tactic:
exact Eventually.of_forall fun _ => ha _

Result:
no goals