case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.187657
ι : Type ?u.187660
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
α : Type u_1
β : Type u_2
γ : Type ?u.187657
ι : Type ?u.187660
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
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
no goals
case intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.187657
ι : Type ?u.187660
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
exact hc.mono fun x hx => lt_of_lt_of_le hbc hx
α : Type u_1
β : Type u_2
γ : Type ?u.187657
ι : Type ?u.187660
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
α : Type u_1
β : Type u_2
γ : Type ?u.187657
ι : Type ?u.187660
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
simp_rw [exists_prop]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.187657
ι : Type ?u.187660
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
exact exists_lt_of_lt_csSup hu h