Theorem: exercise3_7 (LeanCourse/Assignments/Solutions/Solutions3.lean)

State before:
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
⊢ ∀ (n : ℕ), u n ≤ l
Tactic:
intro n
State after:
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
⊢ u n ≤ l

State before:
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
⊢ u n ≤ l
Tactic:
by_contra hn
State after:
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
⊢ False

State before:
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
⊢ False
Tactic:
have : u n > l := by exact not_le.mp hn
State after:
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
this : u n > l
⊢ False

State before:
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
this : u n > l
⊢ False
Tactic:
obtain ⟨N, hN⟩ := h1 (u n - l) (by linarith)
State after:
case intro
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
this : u n > l
N : ℕ
hN : ∀ n_1 ≥ N, |u n_1 - l| < u n - l
⊢ False

State before:
case intro
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
this : u n > l
N : ℕ
hN : ∀ n_1 ≥ N, |u n_1 - l| < u n - l
⊢ False
Tactic:
specialize hN (max n N) (by apply?)
State after:
case intro
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
this : u n > l
N : ℕ
hN : |u (max n N) - l| < u n - l
⊢ False

State before:
case intro
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
this : u n > l
N : ℕ
hN : |u (max n N) - l| < u n - l
⊢ False
Tactic:
rw [← not_le] at hN
State after:
case intro
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
this : u n > l
N : ℕ
hN : ¬u n - l ≤ |u (max n N) - l|
⊢ False

State before:
case intro
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
this : u n > l
N : ℕ
hN : ¬u n - l ≤ |u (max n N) - l|
⊢ False
Tactic:
apply hN
State after:
case intro
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
this : u n > l
N : ℕ
hN : ¬u n - l ≤ |u (max n N) - l|
⊢ u n - l ≤ |u (max n N) - l|

State before:
case intro
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
this : u n > l
N : ℕ
hN : ¬u n - l ≤ |u (max n N) - l|
⊢ u n - l ≤ |u (max n N) - l|
Tactic:
have : u n ≤ u (max n N) := h2 _ _ (by apply?)
State after:
case intro
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
this✝ : u n > l
N : ℕ
hN : ¬u n - l ≤ |u (max n N) - l|
this : u n ≤ u (max n N)
⊢ u n - l ≤ |u (max n N) - l|

State before:
case intro
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
this✝ : u n > l
N : ℕ
hN : ¬u n - l ≤ |u (max n N) - l|
this : u n ≤ u (max n N)
⊢ u n - l ≤ |u (max n N) - l|
Tactic:
rw [abs_eq_self.2]
State after:
case intro
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
this✝ : u n > l
N : ℕ
hN : ¬u n - l ≤ |u (max n N) - l|
this : u n ≤ u (max n N)
⊢ u n - l ≤ u (max n N) - l

case intro
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
this✝ : u n > l
N : ℕ
hN : ¬u n - l ≤ |u (max n N) - l|
this : u n ≤ u (max n N)
⊢ 0 ≤ u (max n N) - l

State before:
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
⊢ u n > l
Tactic:
exact not_le.mp hn
State after:
no goals

State before:
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
this : u n > l
⊢ u n - l > 0
Tactic:
linarith
State after:
no goals

State before:
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
this : u n > l
N : ℕ
hN : ∀ n_1 ≥ N, |u n_1 - l| < u n - l
⊢ max n N ≥ N
Tactic:
apply?
State after:
no goals

State before:
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
this : u n > l
N : ℕ
hN : ¬u n - l ≤ |u (max n N) - l|
⊢ n ≤ max n N
Tactic:
apply?
State after:
no goals

State before:
case intro
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
this✝ : u n > l
N : ℕ
hN : ¬u n - l ≤ |u (max n N) - l|
this : u n ≤ u (max n N)
⊢ u n - l ≤ u (max n N) - l
Tactic:
gcongr
State after:
no goals

State before:
case intro
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
this✝ : u n > l
N : ℕ
hN : ¬u n - l ≤ |u (max n N) - l|
this : u n ≤ u (max n N)
⊢ 0 ≤ u (max n N) - l
Tactic:
rw [sub_nonneg]
State after:
case intro
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
this✝ : u n > l
N : ℕ
hN : ¬u n - l ≤ |u (max n N) - l|
this : u n ≤ u (max n N)
⊢ l ≤ u (max n N)

State before:
case intro
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
this✝ : u n > l
N : ℕ
hN : ¬u n - l ≤ |u (max n N) - l|
this : u n ≤ u (max n N)
⊢ l ≤ u (max n N)
Tactic:
linarith
State after:
no goals