ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N : ℕ
⊢ ∃ n, n ≥ N ∧ ∀ (k : ℕ), k < n → u k < u n
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
⊢ ∀ (N : ℕ), ∃ n, n ≥ N ∧ ∀ (k : ℕ), k < n → u k < u n
intro N
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N : ℕ
⊢ ∃ k, k ≤ N ∧ ∀ (l : ℕ), l ≤ N → u l ≤ u k

case intro.intro
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
⊢ ∃ n, n ≥ N ∧ ∀ (k : ℕ), k < n → u k < u n
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N : ℕ
⊢ ∃ n, n ≥ N ∧ ∀ (k : ℕ), k < n → u k < u n
obtain ⟨k : ℕ, - : k ≤ N, hku : ∀ l ≤ N, u l ≤ u k⟩ : ∃ k ≤ N, ∀ l ≤ N, u l ≤ u k
case intro.intro
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
⊢ ∃ n, n ≥ N ∧ ∀ (k : ℕ), k < n → u k < u n
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N : ℕ
⊢ ∃ k, k ≤ N ∧ ∀ (l : ℕ), l ≤ N → u l ≤ u k

case intro.intro
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
⊢ ∃ n, n ≥ N ∧ ∀ (k : ℕ), k < n → u k < u n
exact exists_max_image _ u (finite_le_nat N) ⟨N, le_refl N⟩
case intro.intro
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
⊢ ∃ n, n ≥ N ∧ ∀ (k : ℕ), k < n → u k < u n
case intro.intro
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
⊢ ∃ n, n ≥ N ∧ ∀ (k : ℕ), k < n → u k < u n
have ex : ∃ n ≥ N, u k < u n := exists_lt_of_tendsto_atTop hu _ _
case intro.intro.intro.intro.intro
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
⊢ ∃ n, n ≥ N ∧ ∀ (k : ℕ), k < n → u k < u n
case intro.intro
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
⊢ ∃ n, n ≥ N ∧ ∀ (k : ℕ), k < n → u k < u n
obtain ⟨n : ℕ, hnN : n ≥ N, hnk : u k < u n, hn_min : ∀ m, m < n → N ≤ m → u m ≤ u k⟩ :
    ∃ n ≥ N, u k < u n ∧ ∀ m, m < n → N ≤ m → u m ≤ u k := by
  rcases Nat.findX ex with ⟨n, ⟨hnN, hnk⟩, hn_min⟩
  push_neg  at hn_min
  exact ⟨n, hnN, hnk, hn_min⟩
case intro.intro.intro.intro.intro
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
⊢ ∀ (k : ℕ), k < n → u k < u n
case intro.intro.intro.intro.intro
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
⊢ ∃ n, n ≥ N ∧ ∀ (k : ℕ), k < n → u k < u n
use n, hnN
case intro.intro.intro.intro.intro
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
l : ℕ
hl : l < n
⊢ u l < u n
case intro.intro.intro.intro.intro
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
⊢ ∀ (k : ℕ), k < n → u k < u n
rintro (l : ℕ) (hl : l < n)
no goals
case intro.intro.intro.intro.intro
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
l : ℕ
hl : l < n
hlk : u l ≤ u k
⊢ u l < u n
calc
  u l ≤ u k := hlk
  _ < u n := hnk
case mk.intro.intro
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hn_min : ∀ (m : ℕ), m < n → ¬(m ≥ N ∧ u k < u m)
hnN : n ≥ N
hnk : u k < u n
⊢ ∃ n, n ≥ N ∧ u k < u n ∧ ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
⊢ ∃ n, n ≥ N ∧ u k < u n ∧ ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
rcases Nat.findX ex with ⟨n, ⟨hnN, hnk⟩, hn_min⟩
case mk.intro.intro
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ (m : ℕ), m < n → m ≥ N → u m ≤ u k
⊢ ∃ n, n ≥ N ∧ u k < u n ∧ ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
case mk.intro.intro
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hn_min : ∀ (m : ℕ), m < n → ¬(m ≥ N ∧ u k < u m)
hnN : n ≥ N
hnk : u k < u n
⊢ ∃ n, n ≥ N ∧ u k < u n ∧ ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
push_neg  at hn_min
no goals
case mk.intro.intro
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ (m : ℕ), m < n → m ≥ N → u m ≤ u k
⊢ ∃ n, n ≥ N ∧ u k < u n ∧ ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
exact ⟨n, hnN, hnk, hn_min⟩
case inl
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
l : ℕ
hl : l < n
H : l ≤ N
⊢ u l ≤ u k

case inr
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
l : ℕ
hl : l < n
H : N ≤ l
⊢ u l ≤ u k
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
l : ℕ
hl : l < n
⊢ u l ≤ u k
cases' (le_total l N : l ≤ N ∨ N ≤ l) with H H
no goals
case inl
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
l : ℕ
hl : l < n
H : l ≤ N
⊢ u l ≤ u k
exact hku l H
no goals
case inr
ι : Type ?u.70456
ι' : Type ?u.70459
α : Type ?u.70462
β : Type u_1
γ : Type ?u.70468
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ (l : ℕ), l ≤ N → u l ≤ u k
ex : ∃ n, n ≥ N ∧ u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ (m : ℕ), m < n → N ≤ m → u m ≤ u k
l : ℕ
hl : l < n
H : N ≤ l
⊢ u l ≤ u k
exact hn_min l hl H