internlm/Lean-Github huggingface dataset:
Theorem: exercise3_4
Proof 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'
Proof 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| < ε
Theorem: exercise3_4
Proof 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''
Proof 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| < ε
Theorem: exercise3_4
Proof 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
Proof 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| < ε
Theorem: exercise3_4
Proof 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)
Proof 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| < ε
Theorem: exercise3_4
Proof 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)
Proof 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| < ε
Theorem: exercise3_4
Proof 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
Proof 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| < ε
Theorem: exercise3_4
Proof 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
Proof 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| < ε
Theorem: exercise3_4
Proof 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' ⊢
Proof 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 < ε
Theorem: exercise3_4
Proof 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
Proof 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 < ε
Theorem: exercise3_4
Proof 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'
Proof 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 < ε
Theorem: exercise3_4
Proof 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
Proof 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 < ε
Theorem: exercise3_4
Proof 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
Proof state after:
no goals
Theorem: exercise3_4
Proof 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
Proof state after:
no goals
Theorem: exercise3_5
Proof state before:
⊢ SequentialLimit (fun n => 1 / (↑n + 1)) 0
Tactic:
intro ε hε
Proof state after:
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun n => 1 / (↑n + 1)) n - 0| < ε
Theorem: exercise3_5
Proof state before:
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun n => 1 / (↑n + 1)) n - 0| < ε
Tactic:
use ⌈1 / ε⌉₊
Proof state after:
case h
ε : ℝ
hε : ε > 0
⊢ ∀ n ≥ ⌈1 / ε⌉₊, |(fun n => 1 / (↑n + 1)) n - 0| < ε
Theorem: exercise3_5
Proof state before:
case h
ε : ℝ
hε : ε > 0
⊢ ∀ n ≥ ⌈1 / ε⌉₊, |(fun n => 1 / (↑n + 1)) n - 0| < ε
Tactic:
intro n hn
Proof state after:
case h
ε : ℝ
hε : ε > 0
n : ℕ
hn : n ≥ ⌈1 / ε⌉₊
⊢ |(fun n => 1 / (↑n + 1)) n - 0| < ε
Theorem: exercise3_5
Proof state before:
case h
ε : ℝ
hε : ε > 0
n : ℕ
hn : n ≥ ⌈1 / ε⌉₊
⊢ |(fun n => 1 / (↑n + 1)) n - 0| < ε
Tactic:
simp at hn
Proof state after:
case h
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ |(fun n => 1 / (↑n + 1)) n - 0| < ε
Theorem: exercise3_5
Proof state before:
case h
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ |(fun n => 1 / (↑n + 1)) n - 0| < ε
Tactic:
simp [abs_inv]
Proof state after:
case h
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ |↑n + 1|⁻¹ < ε
Theorem: exercise3_5
Proof state before:
case h
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ |↑n + 1|⁻¹ < ε
Tactic:
rw [inv_lt]
Proof state after:
case h
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ ε⁻¹ < |↑n + 1|

case h.ha
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ 0 < |↑n + 1|

case h.hb
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ 0 < ε
Theorem: exercise3_5
Proof state before:
case h
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ ε⁻¹ < |↑n + 1|
Tactic:
have fact1 : (n : ℝ) + 1 ≤ |(n : ℝ) + 1| := by apply?
Proof state after:
case h
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
fact1 : ↑n + 1 ≤ |↑n + 1|
⊢ ε⁻¹ < |↑n + 1|
Theorem: exercise3_5
Proof state before:
case h
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
fact1 : ↑n + 1 ≤ |↑n + 1|
⊢ ε⁻¹ < |↑n + 1|
Tactic:
linarith
Proof state after:
no goals
Theorem: exercise3_5
Proof state before:
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ ↑n + 1 ≤ |↑n + 1|
Tactic:
apply?
Proof state after:
no goals
Theorem: exercise3_5
Proof state before:
case h.ha
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ 0 < |↑n + 1|
Tactic:
rw [abs_pos]
Proof state after:
case h.ha
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ ↑n + 1 ≠ 0
Theorem: exercise3_5
Proof state before:
case h.ha
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ ↑n + 1 ≠ 0
Tactic:
apply?
Proof state after:
no goals
Theorem: exercise3_5
Proof state before:
case h.hb
ε : ℝ
hε : ε > 0
n : ℕ
hn : ε⁻¹ ≤ ↑n
⊢ 0 < ε
Tactic:
assumption
Proof state after:
no goals
Theorem: convergesTo_mul_const
Proof state before:
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
⊢ SequentialLimit (fun n => c * s n) (c * a)
Tactic:
intro ε hε
Proof state after:
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun n => c * s n) n - c * a| < ε
Theorem: convergesTo_mul_const
Proof state before:
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun n => c * s n) n - c * a| < ε
Tactic:
obtain ⟨N, hN⟩ := hs (ε / max |c| 1) (by positivity)
Proof state after:
case intro
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε / max |c| 1
⊢ ∃ N, ∀ n ≥ N, |(fun n => c * s n) n - c * a| < ε
Theorem: convergesTo_mul_const
Proof state before:
case intro
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε / max |c| 1
⊢ ∃ N, ∀ n ≥ N, |(fun n => c * s n) n - c * a| < ε
Tactic:
use N
Proof state after:
case h
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε / max |c| 1
⊢ ∀ n ≥ N, |(fun n => c * s n) n - c * a| < ε
Theorem: convergesTo_mul_const
Proof state before:
case h
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε / max |c| 1
⊢ ∀ n ≥ N, |(fun n => c * s n) n - c * a| < ε
Tactic:
intro n hn
Proof state after:
case h
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε / max |c| 1
n : ℕ
hn : n ≥ N
⊢ |(fun n => c * s n) n - c * a| < ε
Theorem: convergesTo_mul_const
Proof state before:
case h
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N : ℕ
hN : ∀ n ≥ N, |s n - a| < ε / max |c| 1
n : ℕ
hn : n ≥ N
⊢ |(fun n => c * s n) n - c * a| < ε
Tactic:
specialize hN n hn
Proof state after:
case h
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ |(fun n => c * s n) n - c * a| < ε
Theorem: convergesTo_mul_const
Proof state before:
case h
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ |(fun n => c * s n) n - c * a| < ε
Tactic:
simp
Proof state after:
case h
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ |c * s n - c * a| < ε
Theorem: convergesTo_mul_const
Proof state before:
case h
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ |c * s n - c * a| < ε
Tactic:
calc |c * s n - c * a|
    = |c * (s n - a)| := by ring
  _ = |c| * |s n - a| := by exact abs_mul c (s n - a)
  _ ≤ max |c| 1 * |s n - a| := by gcongr; exact le_max_left |c| 1
  _ < max |c| 1 * (ε / max |c| 1) := by gcongr
  _ = ε := by refine mul_div_cancel' ε ?hb; positivity
Proof state after:
no goals
Theorem: convergesTo_mul_const
Proof state before:
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
⊢ ε / max |c| 1 > 0
Tactic:
positivity
Proof state after:
no goals
Theorem: convergesTo_mul_const
Proof state before:
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ |c * s n - c * a| = |c * (s n - a)|
Tactic:
ring
Proof state after:
no goals
Theorem: convergesTo_mul_const
Proof state before:
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ |c * (s n - a)| = |c| * |s n - a|
Tactic:
exact abs_mul c (s n - a)
Proof state after:
no goals
Theorem: convergesTo_mul_const
Proof state before:
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ |c| * |s n - a| ≤ max |c| 1 * |s n - a|
Tactic:
gcongr
Proof state after:
case h
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ |c| ≤ max |c| 1
Theorem: convergesTo_mul_const
Proof state before:
case h
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ |c| ≤ max |c| 1
Tactic:
exact le_max_left |c| 1
Proof state after:
no goals
Theorem: convergesTo_mul_const
Proof state before:
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ max |c| 1 * |s n - a| < max |c| 1 * (ε / max |c| 1)
Tactic:
gcongr
Proof state after:
no goals
Theorem: convergesTo_mul_const
Proof state before:
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ max |c| 1 * (ε / max |c| 1) = ε
Tactic:
refine mul_div_cancel' ε ?hb
Proof state after:
case hb
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ max |c| 1 ≠ 0
Theorem: convergesTo_mul_const
Proof state before:
case hb
s : ℕ → ℝ
a c : ℝ
hs : SequentialLimit s a
ε : ℝ
hε : ε > 0
N n : ℕ
hn : n ≥ N
hN : |s n - a| < ε / max |c| 1
⊢ max |c| 1 ≠ 0
Tactic:
positivity
Proof state after:
no goals
Theorem: use_me
Proof state before:
⊢ SequentialLimit (fun n => -1 / (↑n + 1)) 0
Tactic:
have : SequentialLimit (fun n ↦ (-1) * (1 / (n+1))) (-1 * 0) :=
  convergesTo_mul_const (-1) exercise3_5
Proof state after:
this : SequentialLimit (fun n => -1 * (1 / (↑n + 1))) (-1 * 0)
⊢ SequentialLimit (fun n => -1 / (↑n + 1)) 0
Theorem: use_me
Proof state before:
this : SequentialLimit (fun n => -1 * (1 / (↑n + 1))) (-1 * 0)
⊢ SequentialLimit (fun n => -1 / (↑n + 1)) 0
Tactic:
simp at this
Proof state after:
this : SequentialLimit (fun n => -(↑n + 1)⁻¹) 0
⊢ SequentialLimit (fun n => -1 / (↑n + 1)) 0
Theorem: use_me
Proof state before:
this : SequentialLimit (fun n => -(↑n + 1)⁻¹) 0
⊢ SequentialLimit (fun n => -1 / (↑n + 1)) 0
Tactic:
simp [neg_div, this]
Proof state after:
no goals
Theorem: exercise3_6
Proof state before:
⊢ SequentialLimit (fun n => sin ↑n / (↑n + 1)) 0
Tactic:
apply exercise3_4 use_me exercise3_5
Proof state after:
case hs₁s₂

⊢ ∀ (n : ℕ), -1 / (↑n + 1) ≤ sin ↑n / (↑n + 1)

case hs₂s₃

⊢ ∀ (n : ℕ), sin ↑n / (↑n + 1) ≤ 1 / (↑n + 1)
Theorem: exercise3_6
Proof state before:
case hs₁s₂

⊢ ∀ (n : ℕ), -1 / (↑n + 1) ≤ sin ↑n / (↑n + 1)
Tactic:
intro n
Proof state after:
case hs₁s₂
n : ℕ
⊢ -1 / (↑n + 1) ≤ sin ↑n / (↑n + 1)
Theorem: exercise3_6
Proof state before:
case hs₁s₂
n : ℕ
⊢ -1 / (↑n + 1) ≤ sin ↑n / (↑n + 1)
Tactic:
gcongr
Proof state after:
case hs₁s₂.h
n : ℕ
⊢ -1 ≤ sin ↑n
Theorem: exercise3_6
Proof state before:
case hs₁s₂.h
n : ℕ
⊢ -1 ≤ sin ↑n
Tactic:
apply?
Proof state after:
no goals
Theorem: exercise3_6
Proof state before:
case hs₂s₃

⊢ ∀ (n : ℕ), sin ↑n / (↑n + 1) ≤ 1 / (↑n + 1)
Tactic:
intro n
Proof state after:
case hs₂s₃
n : ℕ
⊢ sin ↑n / (↑n + 1) ≤ 1 / (↑n + 1)
Theorem: exercise3_6
Proof state before:
case hs₂s₃
n : ℕ
⊢ sin ↑n / (↑n + 1) ≤ 1 / (↑n + 1)
Tactic:
gcongr
Proof state after:
case hs₂s₃.h
n : ℕ
⊢ sin ↑n ≤ 1
Theorem: exercise3_6
Proof state before:
case hs₂s₃.h
n : ℕ
⊢ sin ↑n ≤ 1
Tactic:
apply?
Proof state after:
no goals
Theorem: exercise3_7
Proof state before:
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
⊢ ∀ (n : ℕ), u n ≤ l
Tactic:
intro n
Proof state after:
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
⊢ u n ≤ l
Theorem: exercise3_7
Proof state before:
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
⊢ u n ≤ l
Tactic:
by_contra hn
Proof state after:
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
⊢ False
Theorem: exercise3_7
Proof 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
Proof state after:
u : ℕ → ℝ
l : ℝ
h1 : SequentialLimit u l
h2 : NondecreasingSequence u
n : ℕ
hn : ¬u n ≤ l
this : u n > l
⊢ False
Theorem: exercise3_7
Proof 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)
Proof 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
Theorem: exercise3_7
Proof 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?)
Proof 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
Theorem: exercise3_7
Proof 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
Proof 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
Theorem: exercise3_7
Proof 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
Proof 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|
Theorem: exercise3_7
Proof 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?)
Proof 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|
Theorem: exercise3_7
Proof 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]
Proof 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
Theorem: exercise3_7
Proof 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
Proof state after:
no goals
Theorem: exercise3_7
Proof 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
Proof state after:
no goals
Theorem: exercise3_7
Proof 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?
Proof state after:
no goals
Theorem: exercise3_7
Proof 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?
Proof state after:
no goals
Theorem: exercise3_7
Proof 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
Proof state after:
no goals
Theorem: exercise3_7
Proof 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]
Proof 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)
Theorem: exercise3_7
Proof 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
Proof state after:
no goals
Theorem: exercise3_8
Proof state before:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ f '' s ∩ t = f '' (s ∩ f ⁻¹' t)
Tactic:
ext y
Proof state after:
case h
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
y : β
⊢ y ∈ f '' s ∩ t ↔ y ∈ f '' (s ∩ f ⁻¹' t)
Theorem: exercise3_8
Proof state before:
case h
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
y : β
⊢ y ∈ f '' s ∩ t ↔ y ∈ f '' (s ∩ f ⁻¹' t)
Tactic:
constructor
Proof state after:
case h.mp
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
y : β
⊢ y ∈ f '' s ∩ t → y ∈ f '' (s ∩ f ⁻¹' t)

case h.mpr
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
y : β
⊢ y ∈ f '' (s ∩ f ⁻¹' t) → y ∈ f '' s ∩ t