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

State before:
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
⊢ SequentialLimit s₂ a
Tactic:
intro ε hε
State after:
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, |s₂ n - a| < ε

State before:
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, |s₂ n - a| < ε
Tactic:
obtain ⟨N, hN⟩ := hs₁ ε hε
State after:
case intro
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s₁ n - a| < ε
⊢ ∃ N, ∀ n ≥ N, |s₂ n - a| < ε

State before:
case intro
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s₁ n - a| < ε
⊢ ∃ N, ∀ n ≥ N, |s₂ n - a| < ε
Tactic:
obtain ⟨N', hN'⟩ := hs₃ ε hε
State after:
case intro.intro
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s₁ n - a| < ε
N' : ℕ
hN' : ∀ n ≥ N', |s₃ n - a| < ε
⊢ ∃ N, ∀ n ≥ N, |s₂ n - a| < ε

State before:
case intro.intro
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s₁ n - a| < ε
N' : ℕ
hN' : ∀ n ≥ N', |s₃ n - a| < ε
⊢ ∃ N, ∀ n ≥ N, |s₂ n - a| < ε
Tactic:
let N'' := max N N'
State after:
case intro.intro
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s₁ n - a| < ε
N' : ℕ
hN' : ∀ n ≥ N', |s₃ n - a| < ε
N'' : ℕ := max N N'
⊢ ∃ N, ∀ n ≥ N, |s₂ n - a| < ε

State before:
case intro.intro
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s₁ n - a| < ε
N' : ℕ
hN' : ∀ n ≥ N', |s₃ n - a| < ε
N'' : ℕ := max N N'
⊢ ∃ N, ∀ n ≥ N, |s₂ n - a| < ε
Tactic:
use N''
State after:
case h
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s₁ n - a| < ε
N' : ℕ
hN' : ∀ n ≥ N', |s₃ n - a| < ε
N'' : ℕ := max N N'
⊢ ∀ n ≥ N'', |s₂ n - a| < ε

State before:
case h
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s₁ n - a| < ε
N' : ℕ
hN' : ∀ n ≥ N', |s₃ n - a| < ε
N'' : ℕ := max N N'
⊢ ∀ n ≥ N'', |s₂ n - a| < ε
Tactic:
intro n hn
State after:
case h
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s₁ n - a| < ε
N' : ℕ
hN' : ∀ n ≥ N', |s₃ n - a| < ε
N'' : ℕ := max N N'
n : ℕ
hn : n ≥ N''
⊢ |s₂ n - a| < ε

State before:
case h
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s₁ n - a| < ε
N' : ℕ
hN' : ∀ n ≥ N', |s₃ n - a| < ε
N'' : ℕ := max N N'
n : ℕ
hn : n ≥ N''
⊢ |s₂ n - a| < ε
Tactic:
specialize hN n (le_of_max_le_left hn)
State after:
case h
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
ε : ℝ
hε : ε > 0
N N' : ℕ
hN' : ∀ n ≥ N', |s₃ n - a| < ε
N'' : ℕ := max N N'
n : ℕ
hn : n ≥ N''
hN : |s₁ n - a| < ε
⊢ |s₂ n - a| < ε

State before:
case h
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
ε : ℝ
hε : ε > 0
N N' : ℕ
hN' : ∀ n ≥ N', |s₃ n - a| < ε
N'' : ℕ := max N N'
n : ℕ
hn : n ≥ N''
hN : |s₁ n - a| < ε
⊢ |s₂ n - a| < ε
Tactic:
specialize hN' n (le_of_max_le_right hn)
State after:
case h
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
ε : ℝ
hε : ε > 0
N N' : ℕ
N'' : ℕ := max N N'
n : ℕ
hn : n ≥ N''
hN : |s₁ n - a| < ε
hN' : |s₃ n - a| < ε
⊢ |s₂ n - a| < ε

State before:
case h
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₁s₂ : ∀ (n : ℕ), s₁ n ≤ s₂ n
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
ε : ℝ
hε : ε > 0
N N' : ℕ
N'' : ℕ := max N N'
n : ℕ
hn : n ≥ N''
hN : |s₁ n - a| < ε
hN' : |s₃ n - a| < ε
⊢ |s₂ n - a| < ε
Tactic:
specialize hs₁s₂ n
State after:
case h
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
ε : ℝ
hε : ε > 0
N N' : ℕ
N'' : ℕ := max N N'
n : ℕ
hn : n ≥ N''
hN : |s₁ n - a| < ε
hN' : |s₃ n - a| < ε
hs₁s₂ : s₁ n ≤ s₂ n
⊢ |s₂ n - a| < ε

State before:
case h
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
hs₂s₃ : ∀ (n : ℕ), s₂ n ≤ s₃ n
ε : ℝ
hε : ε > 0
N N' : ℕ
N'' : ℕ := max N N'
n : ℕ
hn : n ≥ N''
hN : |s₁ n - a| < ε
hN' : |s₃ n - a| < ε
hs₁s₂ : s₁ n ≤ s₂ n
⊢ |s₂ n - a| < ε
Tactic:
specialize hs₂s₃ n
State after:
case h
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
ε : ℝ
hε : ε > 0
N N' : ℕ
N'' : ℕ := max N N'
n : ℕ
hn : n ≥ N''
hN : |s₁ n - a| < ε
hN' : |s₃ n - a| < ε
hs₁s₂ : s₁ n ≤ s₂ n
hs₂s₃ : s₂ n ≤ s₃ n
⊢ |s₂ n - a| < ε

State before:
case h
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
ε : ℝ
hε : ε > 0
N N' : ℕ
N'' : ℕ := max N N'
n : ℕ
hn : n ≥ N''
hN : |s₁ n - a| < ε
hN' : |s₃ n - a| < ε
hs₁s₂ : s₁ n ≤ s₂ n
hs₂s₃ : s₂ n ≤ s₃ n
⊢ |s₂ n - a| < ε
Tactic:
rw [abs_lt] at hN hN' ⊢
State after:
case h
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
ε : ℝ
hε : ε > 0
N N' : ℕ
N'' : ℕ := max N N'
n : ℕ
hn : n ≥ N''
hN : -ε < s₁ n - a ∧ s₁ n - a < ε
hN' : -ε < s₃ n - a ∧ s₃ n - a < ε
hs₁s₂ : s₁ n ≤ s₂ n
hs₂s₃ : s₂ n ≤ s₃ n
⊢ -ε < s₂ n - a ∧ s₂ n - a < ε

State before:
case h
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
ε : ℝ
hε : ε > 0
N N' : ℕ
N'' : ℕ := max N N'
n : ℕ
hn : n ≥ N''
hN : -ε < s₁ n - a ∧ s₁ n - a < ε
hN' : -ε < s₃ n - a ∧ s₃ n - a < ε
hs₁s₂ : s₁ n ≤ s₂ n
hs₂s₃ : s₂ n ≤ s₃ n
⊢ -ε < s₂ n - a ∧ s₂ n - a < ε
Tactic:
obtain ⟨h₁N, h₂N⟩ := hN
State after:
case h.intro
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
ε : ℝ
hε : ε > 0
N N' : ℕ
N'' : ℕ := max N N'
n : ℕ
hn : n ≥ N''
hN' : -ε < s₃ n - a ∧ s₃ n - a < ε
hs₁s₂ : s₁ n ≤ s₂ n
hs₂s₃ : s₂ n ≤ s₃ n
h₁N : -ε < s₁ n - a
h₂N : s₁ n - a < ε
⊢ -ε < s₂ n - a ∧ s₂ n - a < ε

State before:
case h.intro
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
ε : ℝ
hε : ε > 0
N N' : ℕ
N'' : ℕ := max N N'
n : ℕ
hn : n ≥ N''
hN' : -ε < s₃ n - a ∧ s₃ n - a < ε
hs₁s₂ : s₁ n ≤ s₂ n
hs₂s₃ : s₂ n ≤ s₃ n
h₁N : -ε < s₁ n - a
h₂N : s₁ n - a < ε
⊢ -ε < s₂ n - a ∧ s₂ n - a < ε
Tactic:
obtain ⟨h₁N', h₂N'⟩ := hN'
State after:
case h.intro.intro
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
ε : ℝ
hε : ε > 0
N N' : ℕ
N'' : ℕ := max N N'
n : ℕ
hn : n ≥ N''
hs₁s₂ : s₁ n ≤ s₂ n
hs₂s₃ : s₂ n ≤ s₃ n
h₁N : -ε < s₁ n - a
h₂N : s₁ n - a < ε
h₁N' : -ε < s₃ n - a
h₂N' : s₃ n - a < ε
⊢ -ε < s₂ n - a ∧ s₂ n - a < ε

State before:
case h.intro.intro
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
ε : ℝ
hε : ε > 0
N N' : ℕ
N'' : ℕ := max N N'
n : ℕ
hn : n ≥ N''
hs₁s₂ : s₁ n ≤ s₂ n
hs₂s₃ : s₂ n ≤ s₃ n
h₁N : -ε < s₁ n - a
h₂N : s₁ n - a < ε
h₁N' : -ε < s₃ n - a
h₂N' : s₃ n - a < ε
⊢ -ε < s₂ n - a ∧ s₂ n - a < ε
Tactic:
constructor
State after:
case h.intro.intro.left
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
ε : ℝ
hε : ε > 0
N N' : ℕ
N'' : ℕ := max N N'
n : ℕ
hn : n ≥ N''
hs₁s₂ : s₁ n ≤ s₂ n
hs₂s₃ : s₂ n ≤ s₃ n
h₁N : -ε < s₁ n - a
h₂N : s₁ n - a < ε
h₁N' : -ε < s₃ n - a
h₂N' : s₃ n - a < ε
⊢ -ε < s₂ n - a

case h.intro.intro.right
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
ε : ℝ
hε : ε > 0
N N' : ℕ
N'' : ℕ := max N N'
n : ℕ
hn : n ≥ N''
hs₁s₂ : s₁ n ≤ s₂ n
hs₂s₃ : s₂ n ≤ s₃ n
h₁N : -ε < s₁ n - a
h₂N : s₁ n - a < ε
h₁N' : -ε < s₃ n - a
h₂N' : s₃ n - a < ε
⊢ s₂ n - a < ε

State before:
case h.intro.intro.left
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
ε : ℝ
hε : ε > 0
N N' : ℕ
N'' : ℕ := max N N'
n : ℕ
hn : n ≥ N''
hs₁s₂ : s₁ n ≤ s₂ n
hs₂s₃ : s₂ n ≤ s₃ n
h₁N : -ε < s₁ n - a
h₂N : s₁ n - a < ε
h₁N' : -ε < s₃ n - a
h₂N' : s₃ n - a < ε
⊢ -ε < s₂ n - a
Tactic:
linarith
State after:
no goals

State before:
case h.intro.intro.right
s₁ s₂ s₃ : ℕ → ℝ
a : ℝ
hs₁ : SequentialLimit s₁ a
hs₃ : SequentialLimit s₃ a
ε : ℝ
hε : ε > 0
N N' : ℕ
N'' : ℕ := max N N'
n : ℕ
hn : n ≥ N''
hs₁s₂ : s₁ n ≤ s₂ n
hs₂s₃ : s₂ n ≤ s₃ n
h₁N : -ε < s₁ n - a
h₂N : s₁ n - a < ε
h₁N' : -ε < s₃ n - a
h₂N' : s₃ n - a < ε
⊢ s₂ n - a < ε
Tactic:
linarith
State after:
no goals