α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : (¬IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun i => x i) ∨ ¬IsBoundedUnder (fun x x_1 => x ≥ x_1) l fun i => x i
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun i => abs (x i)
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i
rw [isBoundedUnder_le_abs, not_and_or] at hbdd
case inl
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun i => x i
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i

case inr
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≥ x_1) l fun i => x i
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : (¬IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun i => x i) ∨ ¬IsBoundedUnder (fun x x_1 => x ≥ x_1) l fun i => x i
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i
obtain hbdd | hbdd := hbdd
case inl.intro
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun i => x i
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i
case inl
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun i => x i
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i
obtain ⟨R, hR⟩ := exists_frequently_lt_of_liminf_ne_top hf
case inl.intro.intro
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun i => x i
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i
case inl.intro
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun i => x i
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i
obtain ⟨q, hq⟩ := exists_rat_gt R
case inl.intro.intro.refine'_1
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun i => x i
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
⊢ ∃ᶠ (i : ι) in l, x i < ↑q

case inl.intro.intro.refine'_2
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun i => x i
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
⊢ ∃ᶠ (i : ι) in l, ↑(q + 1) < x i
case inl.intro.intro
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun i => x i
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i
refine' ⟨q, q + 1, (lt_add_iff_pos_right _).2 zero_lt_one, _, _⟩
case inl.intro.intro.refine'_1
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun i => x i
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun i => x i < ↑q) x_1
⊢ ∀ᶠ (x_1 : ι) in l, ¬(fun n => x n < R) x_1
case inl.intro.intro.refine'_1
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun i => x i
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
⊢ ∃ᶠ (i : ι) in l, x i < ↑q
refine' fun hcon => hR _
no goals
case inl.intro.intro.refine'_1
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun i => x i
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun i => x i < ↑q) x_1
⊢ ∀ᶠ (x_1 : ι) in l, ¬(fun n => x n < R) x_1
filter_upwards [hcon]with x hx using not_lt.2 (lt_of_lt_of_le hq (not_lt.1 hx)).le
case inl.intro.intro.refine'_2
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
hbdd : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x a ≤ x_1
⊢ ∃ᶠ (i : ι) in l, ↑(q + 1) < x i
case inl.intro.intro.refine'_2
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun i => x i
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
⊢ ∃ᶠ (i : ι) in l, ↑(q + 1) < x i
simp only [IsBoundedUnder, IsBounded, eventually_map, eventually_atTop, ge_iff_le,
  not_exists, not_forall, not_le, exists_prop] at hbdd
case inl.intro.intro.refine'_2
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
hbdd : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x a ≤ x_1
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun i => ↑(q + 1) < x i) x_1
⊢ ∀ᶠ (a : ι) in l, x a ≤ ↑(q + 1)
case inl.intro.intro.refine'_2
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
hbdd : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x a ≤ x_1
⊢ ∃ᶠ (i : ι) in l, ↑(q + 1) < x i
refine' fun hcon => hbdd ↑(q + 1) _
no goals
case inl.intro.intro.refine'_2
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
R : ℝ
hR : ∃ᶠ (n : ι) in l, x n < R
q : ℚ
hq : R < ↑q
hbdd : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x a ≤ x_1
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun i => ↑(q + 1) < x i) x_1
⊢ ∀ᶠ (a : ι) in l, x a ≤ ↑(q + 1)
filter_upwards [hcon]with x hx using not_lt.1 hx
case inr.intro
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≥ x_1) l fun i => x i
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i
case inr
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≥ x_1) l fun i => x i
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i
obtain ⟨R, hR⟩ := exists_frequently_lt_of_liminf_ne_top' hf
case inr.intro.intro
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≥ x_1) l fun i => x i
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i
case inr.intro
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≥ x_1) l fun i => x i
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i
obtain ⟨q, hq⟩ := exists_rat_lt R
case inr.intro.intro.refine'_1
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≥ x_1) l fun i => x i
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
⊢ ∃ᶠ (i : ι) in l, x i < ↑(q - 1)

case inr.intro.intro.refine'_2
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≥ x_1) l fun i => x i
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
⊢ ∃ᶠ (i : ι) in l, ↑q < x i
case inr.intro.intro
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≥ x_1) l fun i => x i
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
⊢ ∃ a b, a < b ∧ (∃ᶠ (i : ι) in l, x i < ↑a) ∧ ∃ᶠ (i : ι) in l, ↑b < x i
refine' ⟨q - 1, q, (sub_lt_self_iff _).2 zero_lt_one, _, _⟩
case inr.intro.intro.refine'_1
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
hbdd : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x_1 ≤ x a
⊢ ∃ᶠ (i : ι) in l, x i < ↑(q - 1)
case inr.intro.intro.refine'_1
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≥ x_1) l fun i => x i
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
⊢ ∃ᶠ (i : ι) in l, x i < ↑(q - 1)
simp only [IsBoundedUnder, IsBounded, eventually_map, eventually_atTop, ge_iff_le,
  not_exists, not_forall, not_le, exists_prop] at hbdd
case inr.intro.intro.refine'_1
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
hbdd : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x_1 ≤ x a
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun i => x i < ↑(q - 1)) x_1
⊢ ∀ᶠ (a : ι) in l, ↑(q - 1) ≤ x a
case inr.intro.intro.refine'_1
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
hbdd : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x_1 ≤ x a
⊢ ∃ᶠ (i : ι) in l, x i < ↑(q - 1)
refine' fun hcon => hbdd ↑(q - 1) _
no goals
case inr.intro.intro.refine'_1
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
hbdd : ∀ (x_1 : ℝ), ¬∀ᶠ (a : ι) in l, x_1 ≤ x a
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun i => x i < ↑(q - 1)) x_1
⊢ ∀ᶠ (a : ι) in l, ↑(q - 1) ≤ x a
filter_upwards [hcon]with x hx using not_lt.1 hx
case inr.intro.intro.refine'_2
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≥ x_1) l fun i => x i
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun i => ↑q < x i) x_1
⊢ ∀ᶠ (x_1 : ι) in l, ¬(fun n => R < x n) x_1
case inr.intro.intro.refine'_2
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≥ x_1) l fun i => x i
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
⊢ ∃ᶠ (i : ι) in l, ↑q < x i
refine' fun hcon => hR _
no goals
case inr.intro.intro.refine'_2
α : Type ?u.206583
β : Type ?u.206586
γ : Type ?u.206589
a b c d : ℝ≥0∞
r p q✝ : ℝ≥0
x✝ y z ε ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
ι : Type u_1
l : Filter ι
x : ι → ℝ
hf : liminf (fun i => ↑(↑Real.nnabs (x i))) l ≠ ⊤
hbdd : ¬IsBoundedUnder (fun x x_1 => x ≥ x_1) l fun i => x i
R : ℝ
hR : ∃ᶠ (n : ι) in l, R < x n
q : ℚ
hq : ↑q < R
hcon : ∀ᶠ (x_1 : ι) in l, ¬(fun i => ↑q < x i) x_1
⊢ ∀ᶠ (x_1 : ι) in l, ¬(fun n => R < x n) x_1
filter_upwards [hcon]with x hx using not_lt.2 ((not_lt.1 hx).trans hq.le)