internlm/Lean-Github huggingface dataset:
Theorem: Section2sheet6Solutions.tendsTo_neg_const_mul
Proof state before:
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
⊢ TendsTo (fun n => c * a n) (c * t)
Tactic:
have hc' : 0 < -c := neg_pos.mpr hc
Proof state after:
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
⊢ TendsTo (fun n => c * a n) (c * t)
Theorem: Section2sheet6Solutions.tendsTo_neg_const_mul
Proof state before:
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
⊢ TendsTo (fun n => c * a n) (c * t)
Tactic:
intro ε hε
Proof state after:
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => c * a n) n - c * t| < ε
Theorem: Section2sheet6Solutions.tendsTo_neg_const_mul
Proof state before:
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => c * a n) n - c * t| < ε
Tactic:
obtain ⟨X, hX⟩ := h (ε / -c) (div_pos hε hc')
Proof state after:
case intro
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / -c
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => c * a n) n - c * t| < ε
Theorem: Section2sheet6Solutions.tendsTo_neg_const_mul
Proof state before:
case intro
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / -c
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => c * a n) n - c * t| < ε
Tactic:
use X
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / -c
⊢ ∀ (n : ℕ), X ≤ n → |(fun n => c * a n) n - c * t| < ε
Theorem: Section2sheet6Solutions.tendsTo_neg_const_mul
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / -c
⊢ ∀ (n : ℕ), X ≤ n → |(fun n => c * a n) n - c * t| < ε
Tactic:
intro n hn
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / -c
n : ℕ
hn : X ≤ n
⊢ |(fun n => c * a n) n - c * t| < ε
Theorem: Section2sheet6Solutions.tendsTo_neg_const_mul
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - t| < ε / -c
n : ℕ
hn : X ≤ n
⊢ |(fun n => c * a n) n - c * t| < ε
Tactic:
specialize hX n hn
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X n : ℕ
hn : X ≤ n
hX : |a n - t| < ε / -c
⊢ |(fun n => c * a n) n - c * t| < ε
Theorem: Section2sheet6Solutions.tendsTo_neg_const_mul
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X n : ℕ
hn : X ≤ n
hX : |a n - t| < ε / -c
⊢ |(fun n => c * a n) n - c * t| < ε
Tactic:
simp
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X n : ℕ
hn : X ≤ n
hX : |a n - t| < ε / -c
⊢ |c * a n - c * t| < ε
Theorem: Section2sheet6Solutions.tendsTo_neg_const_mul
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X n : ℕ
hn : X ≤ n
hX : |a n - t| < ε / -c
⊢ |c * a n - c * t| < ε
Tactic:
rw [← mul_sub, abs_mul, abs_of_neg hc]
Proof state after:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X n : ℕ
hn : X ≤ n
hX : |a n - t| < ε / -c
⊢ -c * |a n - t| < ε
Theorem: Section2sheet6Solutions.tendsTo_neg_const_mul
Proof state before:
case h
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
c : ℝ
hc : c < 0
hc' : 0 < -c
ε : ℝ
hε : ε > 0
X n : ℕ
hn : X ≤ n
hX : |a n - t| < ε / -c
⊢ -c * |a n - t| < ε
Tactic:
exact (lt_div_iff' hc').mp hX
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_const_mul
Proof state before:
a : ℕ → ℝ
t c : ℝ
h : TendsTo a t
⊢ TendsTo (fun n => c * a n) (c * t)
Tactic:
obtain hc | rfl | hc := lt_trichotomy 0 c
Proof state after:
case inl
a : ℕ → ℝ
t c : ℝ
h : TendsTo a t
hc : 0 < c
⊢ TendsTo (fun n => c * a n) (c * t)

case inr.inl
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
⊢ TendsTo (fun n => 0 * a n) (0 * t)

case inr.inr
a : ℕ → ℝ
t c : ℝ
h : TendsTo a t
hc : c < 0
⊢ TendsTo (fun n => c * a n) (c * t)
Theorem: Section2sheet6Solutions.tendsTo_const_mul
Proof state before:
case inl
a : ℕ → ℝ
t c : ℝ
h : TendsTo a t
hc : 0 < c
⊢ TendsTo (fun n => c * a n) (c * t)
Tactic:
exact tendsTo_pos_const_mul h hc
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_const_mul
Proof state before:
case inr.inl
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
⊢ TendsTo (fun n => 0 * a n) (0 * t)
Tactic:
simpa using tendsTo_const 0
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_const_mul
Proof state before:
case inr.inr
a : ℕ → ℝ
t c : ℝ
h : TendsTo a t
hc : c < 0
⊢ TendsTo (fun n => c * a n) (c * t)
Tactic:
exact tendsTo_neg_const_mul h hc
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_mul_const
Proof state before:
a : ℕ → ℝ
t c : ℝ
h : TendsTo a t
⊢ TendsTo (fun n => a n * c) (t * c)
Tactic:
simpa [mul_comm] using tendsTo_const_mul c h
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_neg'
Proof state before:
a : ℕ → ℝ
t : ℝ
ha : TendsTo a t
⊢ TendsTo (fun n => -a n) (-t)
Tactic:
simpa using tendsTo_const_mul (-1) ha
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_of_tendsTo_sub
Proof state before:
a b : ℕ → ℝ
t u : ℝ
h1 : TendsTo (fun n => a n - b n) t
h2 : TendsTo b u
⊢ TendsTo a (t + u)
Tactic:
simpa using tendsTo_add h1 h2
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_sub_lim_iff
Proof state before:
a : ℕ → ℝ
t : ℝ
⊢ TendsTo a t ↔ TendsTo (fun n => a n - t) 0
Tactic:
constructor
Proof state after:
case mp
a : ℕ → ℝ
t : ℝ
⊢ TendsTo a t → TendsTo (fun n => a n - t) 0

case mpr
a : ℕ → ℝ
t : ℝ
⊢ TendsTo (fun n => a n - t) 0 → TendsTo a t
Theorem: Section2sheet6Solutions.tendsTo_sub_lim_iff
Proof state before:
case mp
a : ℕ → ℝ
t : ℝ
⊢ TendsTo a t → TendsTo (fun n => a n - t) 0
Tactic:
intro h
Proof state after:
case mp
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
⊢ TendsTo (fun n => a n - t) 0
Theorem: Section2sheet6Solutions.tendsTo_sub_lim_iff
Proof state before:
case mp
a : ℕ → ℝ
t : ℝ
h : TendsTo a t
⊢ TendsTo (fun n => a n - t) 0
Tactic:
simpa using tendsTo_sub h (tendsTo_const t)
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_sub_lim_iff
Proof state before:
case mpr
a : ℕ → ℝ
t : ℝ
⊢ TendsTo (fun n => a n - t) 0 → TendsTo a t
Tactic:
intro h
Proof state after:
case mpr
a : ℕ → ℝ
t : ℝ
h : TendsTo (fun n => a n - t) 0
⊢ TendsTo a t
Theorem: Section2sheet6Solutions.tendsTo_sub_lim_iff
Proof state before:
case mpr
a : ℕ → ℝ
t : ℝ
h : TendsTo (fun n => a n - t) 0
⊢ TendsTo a t
Tactic:
simpa using tendsTo_add h (tendsTo_const t)
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_zero_mul_tendsTo_zero
Proof state before:
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
⊢ TendsTo (fun n => a n * b n) 0
Tactic:
intro ε hε
Proof state after:
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => a n * b n) n - 0| < ε
Theorem: Section2sheet6Solutions.tendsTo_zero_mul_tendsTo_zero
Proof state before:
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => a n * b n) n - 0| < ε
Tactic:
obtain ⟨X, hX⟩ := ha ε hε
Proof state after:
case intro
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - 0| < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => a n * b n) n - 0| < ε
Theorem: Section2sheet6Solutions.tendsTo_zero_mul_tendsTo_zero
Proof state before:
case intro
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - 0| < ε
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => a n * b n) n - 0| < ε
Tactic:
obtain ⟨Y, hY⟩ := hb 1 zero_lt_one
Proof state after:
case intro.intro
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - 0| < ε
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - 0| < 1
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => a n * b n) n - 0| < ε
Theorem: Section2sheet6Solutions.tendsTo_zero_mul_tendsTo_zero
Proof state before:
case intro.intro
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - 0| < ε
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - 0| < 1
⊢ ∃ B, ∀ (n : ℕ), B ≤ n → |(fun n => a n * b n) n - 0| < ε
Tactic:
use max X Y
Proof state after:
case h
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - 0| < ε
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - 0| < 1
⊢ ∀ (n : ℕ), max X Y ≤ n → |(fun n => a n * b n) n - 0| < ε
Theorem: Section2sheet6Solutions.tendsTo_zero_mul_tendsTo_zero
Proof state before:
case h
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - 0| < ε
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - 0| < 1
⊢ ∀ (n : ℕ), max X Y ≤ n → |(fun n => a n * b n) n - 0| < ε
Tactic:
intro n hn
Proof state after:
case h
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - 0| < ε
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - 0| < 1
n : ℕ
hn : max X Y ≤ n
⊢ |(fun n => a n * b n) n - 0| < ε
Theorem: Section2sheet6Solutions.tendsTo_zero_mul_tendsTo_zero
Proof state before:
case h
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - 0| < ε
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - 0| < 1
n : ℕ
hn : max X Y ≤ n
⊢ |(fun n => a n * b n) n - 0| < ε
Tactic:
specialize hX n (le_of_max_le_left hn)
Proof state after:
case h
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - 0| < 1
n : ℕ
hn : max X Y ≤ n
hX : |a n - 0| < ε
⊢ |(fun n => a n * b n) n - 0| < ε
Theorem: Section2sheet6Solutions.tendsTo_zero_mul_tendsTo_zero
Proof state before:
case h
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |b n - 0| < 1
n : ℕ
hn : max X Y ≤ n
hX : |a n - 0| < ε
⊢ |(fun n => a n * b n) n - 0| < ε
Tactic:
specialize hY n (le_of_max_le_right hn)
Proof state after:
case h
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X Y n : ℕ
hn : max X Y ≤ n
hX : |a n - 0| < ε
hY : |b n - 0| < 1
⊢ |(fun n => a n * b n) n - 0| < ε
Theorem: Section2sheet6Solutions.tendsTo_zero_mul_tendsTo_zero
Proof state before:
case h
a b : ℕ → ℝ
ha : TendsTo a 0
hb : TendsTo b 0
ε : ℝ
hε : ε > 0
X Y n : ℕ
hn : max X Y ≤ n
hX : |a n - 0| < ε
hY : |b n - 0| < 1
⊢ |(fun n => a n * b n) n - 0| < ε
Tactic:
simpa [abs_mul] using mul_lt_mul'' hX hY
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_mul
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo a t
hb : TendsTo b u
⊢ TendsTo (fun n => a n * b n) (t * u)
Tactic:
rw [tendsTo_sub_lim_iff] at *
Proof state after:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
⊢ TendsTo (fun n => a n * b n - t * u) 0
Theorem: Section2sheet6Solutions.tendsTo_mul
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
⊢ TendsTo (fun n => a n * b n - t * u) 0
Tactic:
have h : ∀ n, a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u := by
  intro n; ring
Proof state after:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => a n * b n - t * u) 0
Theorem: Section2sheet6Solutions.tendsTo_mul
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => a n * b n - t * u) 0
Tactic:
simp [h]
Proof state after:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u) 0
Theorem: Section2sheet6Solutions.tendsTo_mul
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u) 0
Tactic:
rw [show (0 : ℝ) = 0 + t * 0 + 0 * u by simp]
Proof state after:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u) (0 + t * 0 + 0 * u)
Theorem: Section2sheet6Solutions.tendsTo_mul
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u) (0 + t * 0 + 0 * u)
Tactic:
refine' tendsTo_add (tendsTo_add _ _) _
Proof state after:
case refine'_1
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => (a n - t) * (b n - u)) 0

case refine'_2
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => t * (b n - u)) (t * 0)

case refine'_3
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => (a n - t) * u) (0 * u)
Theorem: Section2sheet6Solutions.tendsTo_mul
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
⊢ ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
Tactic:
intro n
Proof state after:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
n : ℕ
⊢ a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
Theorem: Section2sheet6Solutions.tendsTo_mul
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
n : ℕ
⊢ a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
Tactic:
ring
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_mul
Proof state before:
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ 0 = 0 + t * 0 + 0 * u
Tactic:
simp
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_mul
Proof state before:
case refine'_1
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => (a n - t) * (b n - u)) 0
Tactic:
exact tendsTo_zero_mul_tendsTo_zero ha hb
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_mul
Proof state before:
case refine'_2
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => t * (b n - u)) (t * 0)
Tactic:
exact tendsTo_const_mul t hb
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_mul
Proof state before:
case refine'_3
a b : ℕ → ℝ
t u : ℝ
ha : TendsTo (fun n => a n - t) 0
hb : TendsTo (fun n => b n - u) 0
h : ∀ (n : ℕ), a n * b n - t * u = (a n - t) * (b n - u) + t * (b n - u) + (a n - t) * u
⊢ TendsTo (fun n => (a n - t) * u) (0 * u)
Tactic:
exact tendsTo_mul_const u ha
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_unique
Proof state before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
⊢ s = t
Tactic:
by_contra h
Proof state after:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
⊢ False
Theorem: Section2sheet6Solutions.tendsTo_unique
Proof state before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
⊢ False
Tactic:
wlog h2 : s < t
Proof state after:
case inr
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
this : ∀ (a : ℕ → ℝ) (s t : ℝ), TendsTo a s → TendsTo a t → ¬s = t → s < t → False
h2 : ¬s < t
⊢ False

a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
⊢ False
Theorem: Section2sheet6Solutions.tendsTo_unique
Proof state before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
⊢ False
Tactic:
set ε := t - s with hε
Proof state after:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε : ε = t - s
⊢ False
Theorem: Section2sheet6Solutions.tendsTo_unique
Proof state before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε : ε = t - s
⊢ False
Tactic:
have hε : 0 < ε := sub_pos.mpr h2
Proof state after:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
⊢ False
Theorem: Section2sheet6Solutions.tendsTo_unique
Proof state before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
⊢ False
Tactic:
obtain ⟨X, hX⟩ := hs (ε / 2) (by linarith)
Proof state after:
case intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - s| < ε / 2
⊢ False
Theorem: Section2sheet6Solutions.tendsTo_unique
Proof state before:
case intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - s| < ε / 2
⊢ False
Tactic:
obtain ⟨Y, hY⟩ := ht (ε / 2) (by linarith)
Proof state after:
case intro.intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - s| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |a n - t| < ε / 2
⊢ False
Theorem: Section2sheet6Solutions.tendsTo_unique
Proof state before:
case intro.intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - s| < ε / 2
Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |a n - t| < ε / 2
⊢ False
Tactic:
specialize hX (max X Y) (le_max_left X Y)
Proof state after:
case intro.intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
X Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |a n - t| < ε / 2
hX : |a (max X Y) - s| < ε / 2
⊢ False
Theorem: Section2sheet6Solutions.tendsTo_unique
Proof state before:
case intro.intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
X Y : ℕ
hY : ∀ (n : ℕ), Y ≤ n → |a n - t| < ε / 2
hX : |a (max X Y) - s| < ε / 2
⊢ False
Tactic:
specialize hY (max X Y) (le_max_right X Y)
Proof state after:
case intro.intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
X Y : ℕ
hX : |a (max X Y) - s| < ε / 2
hY : |a (max X Y) - t| < ε / 2
⊢ False
Theorem: Section2sheet6Solutions.tendsTo_unique
Proof state before:
case intro.intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
X Y : ℕ
hX : |a (max X Y) - s| < ε / 2
hY : |a (max X Y) - t| < ε / 2
⊢ False
Tactic:
rw [abs_lt] at hX hY
Proof state after:
case intro.intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
X Y : ℕ
hX : -(ε / 2) < a (max X Y) - s ∧ a (max X Y) - s < ε / 2
hY : -(ε / 2) < a (max X Y) - t ∧ a (max X Y) - t < ε / 2
⊢ False
Theorem: Section2sheet6Solutions.tendsTo_unique
Proof state before:
case intro.intro
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
X Y : ℕ
hX : -(ε / 2) < a (max X Y) - s ∧ a (max X Y) - s < ε / 2
hY : -(ε / 2) < a (max X Y) - t ∧ a (max X Y) - t < ε / 2
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_unique
Proof state before:
case inr
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
this : ∀ (a : ℕ → ℝ) (s t : ℝ), TendsTo a s → TendsTo a t → ¬s = t → s < t → False
h2 : ¬s < t
⊢ False
Tactic:
cases' Ne.lt_or_lt h with h3 h3
Proof state after:
case inr.inl
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
this : ∀ (a : ℕ → ℝ) (s t : ℝ), TendsTo a s → TendsTo a t → ¬s = t → s < t → False
h2 : ¬s < t
h3 : s < t
⊢ False

case inr.inr
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
this : ∀ (a : ℕ → ℝ) (s t : ℝ), TendsTo a s → TendsTo a t → ¬s = t → s < t → False
h2 : ¬s < t
h3 : t < s
⊢ False
Theorem: Section2sheet6Solutions.tendsTo_unique
Proof state before:
case inr.inl
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
this : ∀ (a : ℕ → ℝ) (s t : ℝ), TendsTo a s → TendsTo a t → ¬s = t → s < t → False
h2 : ¬s < t
h3 : s < t
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_unique
Proof state before:
case inr.inr
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
this : ∀ (a : ℕ → ℝ) (s t : ℝ), TendsTo a s → TendsTo a t → ¬s = t → s < t → False
h2 : ¬s < t
h3 : t < s
⊢ False
Tactic:
apply this _ _ _ ht hs _ h3
Proof state after:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
this : ∀ (a : ℕ → ℝ) (s t : ℝ), TendsTo a s → TendsTo a t → ¬s = t → s < t → False
h2 : ¬s < t
h3 : t < s
⊢ ¬t = s
Theorem: Section2sheet6Solutions.tendsTo_unique
Proof state before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
this : ∀ (a : ℕ → ℝ) (s t : ℝ), TendsTo a s → TendsTo a t → ¬s = t → s < t → False
h2 : ¬s < t
h3 : t < s
⊢ ¬t = s
Tactic:
exact ne_comm.mp h
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_unique
Proof state before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
⊢ ε / 2 > 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_unique
Proof state before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : ¬s = t
h2 : s < t
ε : ℝ := t - s
hε✝ : ε = t - s
hε : 0 < ε
X : ℕ
hX : ∀ (n : ℕ), X ≤ n → |a n - s| < ε / 2
⊢ ε / 2 > 0
Tactic:
linarith
Proof state after:
no goals
Theorem: Section2sheet6Solutions.eq_zero_of_abs_lt_eps
Proof state before:
r : ℝ
h : ∀ ε > 0, |r| < ε
⊢ r = 0
Tactic:
by_contra h2
Proof state after:
r : ℝ
h : ∀ ε > 0, |r| < ε
h2 : ¬r = 0
⊢ False
Theorem: Section2sheet6Solutions.eq_zero_of_abs_lt_eps
Proof state before:
r : ℝ
h : ∀ ε > 0, |r| < ε
h2 : ¬r = 0
⊢ False
Tactic:
specialize h |r| (abs_pos.mpr h2)
Proof state after:
r : ℝ
h2 : ¬r = 0
h : |r| < |r|
⊢ False
Theorem: Section2sheet6Solutions.eq_zero_of_abs_lt_eps
Proof state before:
r : ℝ
h2 : ¬r = 0
h : |r| < |r|
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: Section2sheet6Solutions.tendsTo_unique'
Proof state before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
⊢ s = t
Tactic:
have h := tendsTo_sub hs ht
Proof state after:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : TendsTo (fun n => a n - a n) (s - t)
⊢ s = t
Theorem: Section2sheet6Solutions.tendsTo_unique'
Proof state before:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : TendsTo (fun n => a n - a n) (s - t)
⊢ s = t
Tactic:
suffices ∀ ε > 0, |t - s| < ε by linarith [eq_zero_of_abs_lt_eps this]
Proof state after:
a : ℕ → ℝ
s t : ℝ
hs : TendsTo a s
ht : TendsTo a t
h : TendsTo (fun n => a n - a n) (s - t)
⊢ ∀ ε > 0, |t - s| < ε