internlm/Lean-Github huggingface dataset:
Theorem: C03S06.convergesTo_mul_const
Proof state before:
case h.e'_1.h
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : c = 0
x✝ : ℕ
⊢ 0 * s x✝ = 0
Tactic:
ring
Proof state after:
no goals
Theorem: C03S06.convergesTo_mul_constαα
Proof state before:
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
⊢ ConvergesTo (fun n => c * s n) (c * a)
Tactic:
by_cases h : c = 0
Proof state after:
case pos
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : c = 0
⊢ ConvergesTo (fun n => c * s n) (c * a)

case neg
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
⊢ ConvergesTo (fun n => c * s n) (c * a)
Theorem: C03S06.convergesTo_mul_constαα
Proof state before:
case neg
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
⊢ ConvergesTo (fun n => c * s n) (c * a)
Tactic:
have acpos : 0 < |c| := abs_pos.mpr h
Proof state after:
case neg
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
⊢ ConvergesTo (fun n => c * s n) (c * a)
Theorem: C03S06.convergesTo_mul_constαα
Proof state before:
case neg
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
⊢ ConvergesTo (fun n => c * s n) (c * a)
Tactic:
intro ε εpos
Proof state after:
case neg
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun n => c * s n) n - c * a| < ε
Theorem: C03S06.convergesTo_mul_constαα
Proof state before:
case neg
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun n => c * s n) n - c * a| < ε
Tactic:
dsimp
Proof state after:
case neg
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |c * s n - c * a| < ε
Theorem: C03S06.convergesTo_mul_constαα
Proof state before:
case neg
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |c * s n - c * a| < ε
Tactic:
have εcpos : 0 < ε / |c| := by apply div_pos εpos acpos
Proof state after:
case neg
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
εcpos : 0 < ε / |c|
⊢ ∃ N, ∀ n ≥ N, |c * s n - c * a| < ε
Theorem: C03S06.convergesTo_mul_constαα
Proof state before:
case neg
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
εcpos : 0 < ε / |c|
⊢ ∃ N, ∀ n ≥ N, |c * s n - c * a| < ε
Tactic:
rcases cs (ε / |c|) εcpos with ⟨Ns, hs⟩
Proof state after:
case neg.intro
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
εcpos : 0 < ε / |c|
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / |c|
⊢ ∃ N, ∀ n ≥ N, |c * s n - c * a| < ε
Theorem: C03S06.convergesTo_mul_constαα
Proof state before:
case neg.intro
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
εcpos : 0 < ε / |c|
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / |c|
⊢ ∃ N, ∀ n ≥ N, |c * s n - c * a| < ε
Tactic:
use Ns
Proof state after:
case h
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
εcpos : 0 < ε / |c|
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / |c|
⊢ ∀ n ≥ Ns, |c * s n - c * a| < ε
Theorem: C03S06.convergesTo_mul_constαα
Proof state before:
case h
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
εcpos : 0 < ε / |c|
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / |c|
⊢ ∀ n ≥ Ns, |c * s n - c * a| < ε
Tactic:
intro n ngt
Proof state after:
case h
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
εcpos : 0 < ε / |c|
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / |c|
n : ℕ
ngt : n ≥ Ns
⊢ |c * s n - c * a| < ε
Theorem: C03S06.convergesTo_mul_constαα
Proof state before:
case h
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
εcpos : 0 < ε / |c|
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / |c|
n : ℕ
ngt : n ≥ Ns
⊢ |c * s n - c * a| < ε
Tactic:
calc
  |c * s n - c * a| = |c| * |s n - a| := by rw [← abs_mul, mul_sub]
  _ < |c| * (ε / |c|) := (mul_lt_mul_of_pos_left (hs n ngt) acpos)
  _ = ε := mul_div_cancel₀ _ (ne_of_lt acpos).symm
Proof state after:
no goals
Theorem: C03S06.convergesTo_mul_constαα
Proof state before:
case pos
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : c = 0
⊢ ConvergesTo (fun n => c * s n) (c * a)
Tactic:
convert convergesTo_const 0
Proof state after:
case h.e'_1.h
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : c = 0
x✝ : ℕ
⊢ c * s x✝ = 0

case h.e'_2
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : c = 0
⊢ c * a = 0
Theorem: C03S06.convergesTo_mul_constαα
Proof state before:
case h.e'_2
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : c = 0
⊢ c * a = 0
Tactic:
rw [h]
Proof state after:
case h.e'_2
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : c = 0
⊢ 0 * a = 0
Theorem: C03S06.convergesTo_mul_constαα
Proof state before:
case h.e'_2
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : c = 0
⊢ 0 * a = 0
Tactic:
ring
Proof state after:
no goals
Theorem: C03S06.convergesTo_mul_constαα
Proof state before:
case h.e'_1.h
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : c = 0
x✝ : ℕ
⊢ c * s x✝ = 0
Tactic:
rw [h]
Proof state after:
case h.e'_1.h
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : c = 0
x✝ : ℕ
⊢ 0 * s x✝ = 0
Theorem: C03S06.convergesTo_mul_constαα
Proof state before:
case h.e'_1.h
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : c = 0
x✝ : ℕ
⊢ 0 * s x✝ = 0
Tactic:
ring
Proof state after:
no goals
Theorem: C03S06.convergesTo_mul_constαα
Proof state before:
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
⊢ 0 < ε / |c|
Tactic:
apply div_pos εpos acpos
Proof state after:
no goals
Theorem: C03S06.convergesTo_mul_constαα
Proof state before:
s : ℕ → ℝ
a c : ℝ
cs : ConvergesTo s a
h : ¬c = 0
acpos : 0 < |c|
ε : ℝ
εpos : ε > 0
εcpos : 0 < ε / |c|
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / |c|
n : ℕ
ngt : n ≥ Ns
⊢ |c * s n - c * a| = |c| * |s n - a|
Tactic:
rw [← abs_mul, mul_sub]
Proof state after:
no goals
Theorem: C03S06.exists_abs_le_of_convergesTo
Proof state before:
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
⊢ ∃ N b, ∀ (n : ℕ), N ≤ n → |s n| < b
Tactic:
rcases cs 1 zero_lt_one with ⟨N, h⟩
Proof state after:
case intro
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
⊢ ∃ N b, ∀ (n : ℕ), N ≤ n → |s n| < b
Theorem: C03S06.exists_abs_le_of_convergesTo
Proof state before:
case intro
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
⊢ ∃ N b, ∀ (n : ℕ), N ≤ n → |s n| < b
Tactic:
use N, |a| + 1
Proof state after:
case h
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
⊢ ∀ (n : ℕ), N ≤ n → |s n| < |a| + 1
Theorem: C03S06.exists_abs_le_of_convergesTo
Proof state before:
case h
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
⊢ ∀ (n : ℕ), N ≤ n → |s n| < |a| + 1
Tactic:
sorry
Proof state after:
no goals
Theorem: C03S06.exists_abs_le_of_convergesToαα
Proof state before:
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
⊢ ∃ N b, ∀ (n : ℕ), N ≤ n → |s n| < b
Tactic:
rcases cs 1 zero_lt_one with ⟨N, h⟩
Proof state after:
case intro
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
⊢ ∃ N b, ∀ (n : ℕ), N ≤ n → |s n| < b
Theorem: C03S06.exists_abs_le_of_convergesToαα
Proof state before:
case intro
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
⊢ ∃ N b, ∀ (n : ℕ), N ≤ n → |s n| < b
Tactic:
use N, |a| + 1
Proof state after:
case h
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
⊢ ∀ (n : ℕ), N ≤ n → |s n| < |a| + 1
Theorem: C03S06.exists_abs_le_of_convergesToαα
Proof state before:
case h
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
⊢ ∀ (n : ℕ), N ≤ n → |s n| < |a| + 1
Tactic:
intro n ngt
Proof state after:
case h
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
n : ℕ
ngt : N ≤ n
⊢ |s n| < |a| + 1
Theorem: C03S06.exists_abs_le_of_convergesToαα
Proof state before:
case h
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
n : ℕ
ngt : N ≤ n
⊢ |s n| < |a| + 1
Tactic:
calc
  |s n| = |s n - a + a| := by
    congr
    abel
  _ ≤ |s n - a| + |a| := (abs_add _ _)
  _ < |a| + 1 := by linarith [h n ngt]
Proof state after:
no goals
Theorem: C03S06.exists_abs_le_of_convergesToαα
Proof state before:
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
n : ℕ
ngt : N ≤ n
⊢ |s n| = |s n - a + a|
Tactic:
congr
Proof state after:
case e_a
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
n : ℕ
ngt : N ≤ n
⊢ s n = s n - a + a
Theorem: C03S06.exists_abs_le_of_convergesToαα
Proof state before:
case e_a
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
n : ℕ
ngt : N ≤ n
⊢ s n = s n - a + a
Tactic:
abel
Proof state after:
no goals
Theorem: C03S06.exists_abs_le_of_convergesToαα
Proof state before:
s : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
N : ℕ
h : ∀ n ≥ N, |s n - a| < 1
n : ℕ
ngt : N ≤ n
⊢ |s n - a| + |a| < |a| + 1
Tactic:
linarith [h n ngt]
Proof state after:
no goals
Theorem: C03S06.aux
Proof state before:
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
⊢ ConvergesTo (fun n => s n * t n) 0
Tactic:
intro ε εpos
Proof state after:
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun n => s n * t n) n - 0| < ε
Theorem: C03S06.aux
Proof state before:
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun n => s n * t n) n - 0| < ε
Tactic:
dsimp
Proof state after:
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Theorem: C03S06.aux
Proof state before:
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Tactic:
rcases exists_abs_le_of_convergesTo cs with ⟨N₀, B, h₀⟩
Proof state after:
case intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Theorem: C03S06.aux
Proof state before:
case intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Tactic:
have Bpos : 0 < B := lt_of_le_of_lt (abs_nonneg _) (h₀ N₀ (le_refl _))
Proof state after:
case intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Theorem: C03S06.aux
Proof state before:
case intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Tactic:
have pos₀ : ε / B > 0 := div_pos εpos Bpos
Proof state after:
case intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
pos₀ : ε / B > 0
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Theorem: C03S06.aux
Proof state before:
case intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
pos₀ : ε / B > 0
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Tactic:
rcases ct _ pos₀ with ⟨N₁, h₁⟩
Proof state after:
case intro.intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
pos₀ : ε / B > 0
N₁ : ℕ
h₁ : ∀ n ≥ N₁, |t n - 0| < ε / B
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Theorem: C03S06.aux
Proof state before:
case intro.intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
pos₀ : ε / B > 0
N₁ : ℕ
h₁ : ∀ n ≥ N₁, |t n - 0| < ε / B
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Tactic:
sorry
Proof state after:
no goals
Theorem: C03S06.auxαα
Proof state before:
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
⊢ ConvergesTo (fun n => s n * t n) 0
Tactic:
intro ε εpos
Proof state after:
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun n => s n * t n) n - 0| < ε
Theorem: C03S06.auxαα
Proof state before:
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun n => s n * t n) n - 0| < ε
Tactic:
dsimp
Proof state after:
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Theorem: C03S06.auxαα
Proof state before:
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Tactic:
rcases exists_abs_le_of_convergesTo cs with ⟨N₀, B, h₀⟩
Proof state after:
case intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Theorem: C03S06.auxαα
Proof state before:
case intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Tactic:
have Bpos : 0 < B := lt_of_le_of_lt (abs_nonneg _) (h₀ N₀ (le_refl _))
Proof state after:
case intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Theorem: C03S06.auxαα
Proof state before:
case intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Tactic:
have pos₀ : ε / B > 0 := div_pos εpos Bpos
Proof state after:
case intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
pos₀ : ε / B > 0
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Theorem: C03S06.auxαα
Proof state before:
case intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
pos₀ : ε / B > 0
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Tactic:
rcases ct _ pos₀ with ⟨N₁, h₁⟩
Proof state after:
case intro.intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
pos₀ : ε / B > 0
N₁ : ℕ
h₁ : ∀ n ≥ N₁, |t n - 0| < ε / B
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Theorem: C03S06.auxαα
Proof state before:
case intro.intro.intro
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
pos₀ : ε / B > 0
N₁ : ℕ
h₁ : ∀ n ≥ N₁, |t n - 0| < ε / B
⊢ ∃ N, ∀ n ≥ N, |s n * t n - 0| < ε
Tactic:
use max N₀ N₁
Proof state after:
case h
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
pos₀ : ε / B > 0
N₁ : ℕ
h₁ : ∀ n ≥ N₁, |t n - 0| < ε / B
⊢ ∀ n ≥ max N₀ N₁, |s n * t n - 0| < ε
Theorem: C03S06.auxαα
Proof state before:
case h
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
pos₀ : ε / B > 0
N₁ : ℕ
h₁ : ∀ n ≥ N₁, |t n - 0| < ε / B
⊢ ∀ n ≥ max N₀ N₁, |s n * t n - 0| < ε
Tactic:
intro n ngt
Proof state after:
case h
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
pos₀ : ε / B > 0
N₁ : ℕ
h₁ : ∀ n ≥ N₁, |t n - 0| < ε / B
n : ℕ
ngt : n ≥ max N₀ N₁
⊢ |s n * t n - 0| < ε
Theorem: C03S06.auxαα
Proof state before:
case h
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
pos₀ : ε / B > 0
N₁ : ℕ
h₁ : ∀ n ≥ N₁, |t n - 0| < ε / B
n : ℕ
ngt : n ≥ max N₀ N₁
⊢ |s n * t n - 0| < ε
Tactic:
have ngeN₀ : n ≥ N₀ := le_of_max_le_left ngt
Proof state after:
case h
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
pos₀ : ε / B > 0
N₁ : ℕ
h₁ : ∀ n ≥ N₁, |t n - 0| < ε / B
n : ℕ
ngt : n ≥ max N₀ N₁
ngeN₀ : n ≥ N₀
⊢ |s n * t n - 0| < ε
Theorem: C03S06.auxαα
Proof state before:
case h
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
pos₀ : ε / B > 0
N₁ : ℕ
h₁ : ∀ n ≥ N₁, |t n - 0| < ε / B
n : ℕ
ngt : n ≥ max N₀ N₁
ngeN₀ : n ≥ N₀
⊢ |s n * t n - 0| < ε
Tactic:
have ngeN₁ : n ≥ N₁ := le_of_max_le_right ngt
Proof state after:
case h
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
pos₀ : ε / B > 0
N₁ : ℕ
h₁ : ∀ n ≥ N₁, |t n - 0| < ε / B
n : ℕ
ngt : n ≥ max N₀ N₁
ngeN₀ : n ≥ N₀
ngeN₁ : n ≥ N₁
⊢ |s n * t n - 0| < ε
Theorem: C03S06.auxαα
Proof state before:
case h
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
pos₀ : ε / B > 0
N₁ : ℕ
h₁ : ∀ n ≥ N₁, |t n - 0| < ε / B
n : ℕ
ngt : n ≥ max N₀ N₁
ngeN₀ : n ≥ N₀
ngeN₁ : n ≥ N₁
⊢ |s n * t n - 0| < ε
Tactic:
calc
  |s n * t n - 0| = |s n| * |t n - 0| := by rw [sub_zero, abs_mul, sub_zero]
  _ < B * (ε / B) := (mul_lt_mul'' (h₀ n ngeN₀) (h₁ n ngeN₁) (abs_nonneg _) (abs_nonneg _))
  _ = ε := mul_div_cancel₀ _ (ne_of_lt Bpos).symm
Proof state after:
no goals
Theorem: C03S06.auxαα
Proof state before:
s t : ℕ → ℝ
a : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t 0
ε : ℝ
εpos : ε > 0
N₀ : ℕ
B : ℝ
h₀ : ∀ (n : ℕ), N₀ ≤ n → |s n| < B
Bpos : 0 < B
pos₀ : ε / B > 0
N₁ : ℕ
h₁ : ∀ n ≥ N₁, |t n - 0| < ε / B
n : ℕ
ngt : n ≥ max N₀ N₁
ngeN₀ : n ≥ N₀
ngeN₁ : n ≥ N₁
⊢ |s n * t n - 0| = |s n| * |t n - 0|
Tactic:
rw [sub_zero, abs_mul, sub_zero]
Proof state after:
no goals
Theorem: C03S06.convergesTo_mul
Proof state before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
⊢ ConvergesTo (fun n => s n * t n) (a * b)
Tactic:
have h₁ : ConvergesTo (fun n ↦ s n * (t n + -b)) 0 := by
  apply aux cs
  convert convergesTo_add ct (convergesTo_const (-b))
  ring
Proof state after:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
⊢ ConvergesTo (fun n => s n * t n) (a * b)
Theorem: C03S06.convergesTo_mul
Proof state before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
⊢ ConvergesTo (fun n => s n * t n) (a * b)
Tactic:
have := convergesTo_add h₁ (convergesTo_mul_const b cs)
Proof state after:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
this : ConvergesTo (fun n => s n * (t n + -b) + b * s n) (0 + b * a)
⊢ ConvergesTo (fun n => s n * t n) (a * b)
Theorem: C03S06.convergesTo_mul
Proof state before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
this : ConvergesTo (fun n => s n * (t n + -b) + b * s n) (0 + b * a)
⊢ ConvergesTo (fun n => s n * t n) (a * b)
Tactic:
convert convergesTo_add h₁ (convergesTo_mul_const b cs) using 1
Proof state after:
case h.e'_1
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
this : ConvergesTo (fun n => s n * (t n + -b) + b * s n) (0 + b * a)
⊢ (fun n => s n * t n) = fun n => s n * (t n + -b) + b * s n

case h.e'_2
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
this : ConvergesTo (fun n => s n * (t n + -b) + b * s n) (0 + b * a)
⊢ a * b = 0 + b * a
Theorem: C03S06.convergesTo_mul
Proof state before:
case h.e'_2
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
this : ConvergesTo (fun n => s n * (t n + -b) + b * s n) (0 + b * a)
⊢ a * b = 0 + b * a
Tactic:
ring
Proof state after:
no goals
Theorem: C03S06.convergesTo_mul
Proof state before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
⊢ ConvergesTo (fun n => s n * (t n + -b)) 0
Tactic:
apply aux cs
Proof state after:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
⊢ ConvergesTo (fun n => t n + -b) 0
Theorem: C03S06.convergesTo_mul
Proof state before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
⊢ ConvergesTo (fun n => t n + -b) 0
Tactic:
convert convergesTo_add ct (convergesTo_const (-b))
Proof state after:
case h.e'_2
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
⊢ 0 = b + -b
Theorem: C03S06.convergesTo_mul
Proof state before:
case h.e'_2
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
⊢ 0 = b + -b
Tactic:
ring
Proof state after:
no goals
Theorem: C03S06.convergesTo_mul
Proof state before:
case h.e'_1
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
this : ConvergesTo (fun n => s n * (t n + -b) + b * s n) (0 + b * a)
⊢ (fun n => s n * t n) = fun n => s n * (t n + -b) + b * s n
Tactic:
ext
Proof state after:
case h.e'_1.h
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
this : ConvergesTo (fun n => s n * (t n + -b) + b * s n) (0 + b * a)
x✝ : ℕ
⊢ s x✝ * t x✝ = s x✝ * (t x✝ + -b) + b * s x✝
Theorem: C03S06.convergesTo_mul
Proof state before:
case h.e'_1.h
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
h₁ : ConvergesTo (fun n => s n * (t n + -b)) 0
this : ConvergesTo (fun n => s n * (t n + -b) + b * s n) (0 + b * a)
x✝ : ℕ
⊢ s x✝ * t x✝ = s x✝ * (t x✝ + -b) + b * s x✝
Tactic:
ring
Proof state after:
no goals
Theorem: C03S06.convergesTo_unique
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
⊢ a = b
Tactic:
by_contra abne
Proof state after:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
⊢ False
Theorem: C03S06.convergesTo_unique
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
⊢ False
Tactic:
have : |a - b| > 0 := by sorry
Proof state after:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
⊢ False
Theorem: C03S06.convergesTo_unique
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
⊢ False
Tactic:
let ε := |a - b| / 2
Proof state after:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
⊢ False
Theorem: C03S06.convergesTo_unique
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
⊢ False
Tactic:
have εpos : ε > 0 := by
  change |a - b| / 2 > 0
  linarith
Proof state after:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
⊢ False
Theorem: C03S06.convergesTo_unique
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
⊢ False
Tactic:
rcases sa ε εpos with ⟨Na, hNa⟩
Proof state after:
case intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
⊢ False
Theorem: C03S06.convergesTo_unique
Proof state before:
case intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
⊢ False
Tactic:
rcases sb ε εpos with ⟨Nb, hNb⟩
Proof state after:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
⊢ False
Theorem: C03S06.convergesTo_unique
Proof state before:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
⊢ False
Tactic:
let N := max Na Nb
Proof state after:
case intro.intro
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
this : |a - b| > 0
ε : ℝ := |a - b| / 2
εpos : ε > 0
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
⊢ False