internlm/Lean-Github huggingface dataset:
Theorem: Cauchy_formula
Proof state before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
z : ℂ
hz : z ∈ sphere c r
hzne : z ≠ c
⊢ ‖(z - c)⁻¹ • (f z - y)‖ ≤ r⁻¹ * (ε / (2 * π))
Tactic:
rw [mem_sphere, dist_eq_norm] at hz
Proof state after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
z : ℂ
hz : ‖z - c‖ = r
hzne : z ≠ c
⊢ ‖(z - c)⁻¹ • (f z - y)‖ ≤ r⁻¹ * (ε / (2 * π))
Theorem: Cauchy_formula
Proof state before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
z : ℂ
hz : ‖z - c‖ = r
hzne : z ≠ c
⊢ ‖(z - c)⁻¹ • (f z - y)‖ ≤ r⁻¹ * (ε / (2 * π))
Tactic:
rw [norm_smul, norm_inv, hz, ← dist_eq_norm]
Proof state after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
z : ℂ
hz : ‖z - c‖ = r
hzne : z ≠ c
⊢ r⁻¹ * dist (f z) y ≤ r⁻¹ * (ε / (2 * π))
Theorem: Cauchy_formula
Proof state before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
z : ℂ
hz : ‖z - c‖ = r
hzne : z ≠ c
⊢ r⁻¹ * dist (f z) y ≤ r⁻¹ * (ε / (2 * π))
Tactic:
refine' mul_le_mul_of_nonneg_left (le_of_lt <| hδ _ _) (inv_nonneg.2 hr0.le)
Proof state after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
z : ℂ
hz : ‖z - c‖ = r
hzne : z ≠ c
⊢ z ∈ closedBall c (α / 2)
Theorem: Cauchy_formula
Proof state before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
z : ℂ
hz : ‖z - c‖ = r
hzne : z ≠ c
⊢ z ∈ closedBall c (α / 2)
Tactic:
rwa [mem_closedBall_iff_norm, hz]
Proof state after:
no goals
Theorem: Cauchy_formula
Proof state before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ 2 * π * r * (r⁻¹ * (ε / (2 * π))) = ε
Tactic:
field_simp [hr0.ne', Real.two_pi_pos.ne']
Proof state after:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ 2 * π * r * ε = ε * (r * (2 * π))
Theorem: Cauchy_formula
Proof state before:
c : ℂ
R : ℝ
h0 : 0 < R
f : ℂ → ℂ
hf : ContinuousOn f (closedBall c R)
hdiff : ∀ z ∈ ball c R, DifferentiableAt ℂ f z
y : ℂ := f c
hy : Tendsto f (𝓝 c) (𝓝 y)
ε : ℝ
ε0 : 0 < ε
α : ℝ
α0 : 0 < α
hα : ∀ x ∈ ball c α, f x ∈ ball y (ε / (2 * π))
δ : ℝ := α / 2
δ0 : 0 < α / 2
hδ : ∀ z ∈ closedBall c (α / 2), f z ∈ ball y (ε / (2 * π))
r : ℝ
hr0 : 0 < r
hrδ : r ≤ δ
hrR : r ≤ R
hsub : closedBall c R \ ball c r ⊆ closedBall c R
hsub' : ball c R \ closedBall c r ⊆ ball c R \ {c}
hzne : ∀ z ∈ sphere c r, z ≠ c
⊢ 2 * π * r * ε = ε * (r * (2 * π))
Tactic:
ac_rfl
Proof state after:
no goals
Theorem: Odd_Odd_Even
Proof state before:
n m : ℕ
hn : Odd n
hm : Odd m
⊢ Even (n + m)
Tactic:
sorry
Proof state after:
no goals
Theorem: C03S06.convergesTo_add
Proof state before:
case h
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
⊢ ∀ n ≥ max Ns Nt, |s n + t n - (a + b)| < ε
Tactic:
intro n hn
Proof state after:
case h
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
n : ℕ
hn : n ≥ max Ns Nt
⊢ |s n + t n - (a + b)| < ε
Theorem: C03S06.convergesTo_add
Proof state before:
case h
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
n : ℕ
hn : n ≥ max Ns Nt
⊢ |s n + t n - (a + b)| < ε
Tactic:
have ngeNs : n ≥ Ns := le_of_max_le_left hn
Proof state after:
case h
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
n : ℕ
hn : n ≥ max Ns Nt
ngeNs : n ≥ Ns
⊢ |s n + t n - (a + b)| < ε
Theorem: C03S06.convergesTo_add
Proof state before:
case h
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
n : ℕ
hn : n ≥ max Ns Nt
ngeNs : n ≥ Ns
⊢ |s n + t n - (a + b)| < ε
Tactic:
have ngeNt : n ≥ Nt := le_of_max_le_right hn
Proof state after:
case h
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
n : ℕ
hn : n ≥ max Ns Nt
ngeNs : n ≥ Ns
ngeNt : n ≥ Nt
⊢ |s n + t n - (a + b)| < ε
Theorem: C03S06.convergesTo_add
Proof state before:
case h
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
n : ℕ
hn : n ≥ max Ns Nt
ngeNs : n ≥ Ns
ngeNt : n ≥ Nt
⊢ |s n + t n - (a + b)| < ε
Tactic:
calc
  |s n + t n - (a + b)| = |s n - a + (t n - b)| := by
    congr
    ring
  _ ≤ |s n - a| + |t n - b| := (abs_add _ _)
  _ < ε / 2 + ε / 2 := (add_lt_add (hs n ngeNs) (ht n ngeNt))
  _ = ε := by norm_num
Proof state after:
no goals
Theorem: C03S06.convergesTo_add
Proof state before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
n : ℕ
hn : n ≥ max Ns Nt
ngeNs : n ≥ Ns
ngeNt : n ≥ Nt
⊢ |s n + t n - (a + b)| = |s n - a + (t n - b)|
Tactic:
congr
Proof state after:
case e_a
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
n : ℕ
hn : n ≥ max Ns Nt
ngeNs : n ≥ Ns
ngeNt : n ≥ Nt
⊢ s n + t n - (a + b) = s n - a + (t n - b)
Theorem: C03S06.convergesTo_add
Proof state before:
case e_a
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
n : ℕ
hn : n ≥ max Ns Nt
ngeNs : n ≥ Ns
ngeNt : n ≥ Nt
⊢ s n + t n - (a + b) = s n - a + (t n - b)
Tactic:
ring
Proof state after:
no goals
Theorem: C03S06.convergesTo_add
Proof state before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
Ns : ℕ
hs : ∀ n ≥ Ns, |s n - a| < ε / 2
Nt : ℕ
ht : ∀ n ≥ Nt, |t n - b| < ε / 2
n : ℕ
hn : n ≥ max Ns Nt
ngeNs : n ≥ Ns
ngeNt : n ≥ Nt
⊢ ε / 2 + ε / 2 = ε
Tactic:
norm_num
Proof state after:
no goals
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:
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:
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:
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_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| < ε
N : ℕ := max Na Nb
⊢ False
Tactic:
have absa : |s N - a| < ε := by
  apply hNa
  apply le_max_left
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
absa : |s N - a| < ε
⊢ 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| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
⊢ False
Tactic:
have absb : |s N - b| < ε := by
  apply hNb
  apply le_max_right
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
absa : |s N - a| < ε
absb : |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| < ε
N : ℕ := max Na Nb
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ False
Tactic:
have : |a - b| < |a - b|
Proof state after:
case this
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
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ |a - b| < |a - b|

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
absa : |s N - a| < ε
absb : |s N - b| < ε
this : |a - b| < |a - b|
⊢ False
Theorem: C03S06.convergesTo_unique
Proof state before:
case this
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
absa : |s N - a| < ε
absb : |s N - b| < ε
⊢ |a - b| < |a - b|

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
absa : |s N - a| < ε
absb : |s N - b| < ε
this : |a - b| < |a - b|
⊢ False
Tactic:
calc
  |a - b| = |(-(s N - a)) + (s N - b)| := by
    congr
    ring
  _ ≤ |(-(s N - a))| + |s N - b| := (abs_add _ _)
  _ = |s N - a| + |s N - b| := by rw [abs_neg]
  _ < ε + ε := (add_lt_add absa absb)
  _ = |a - b| := by norm_num
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
absa : |s N - a| < ε
absb : |s N - b| < ε
this : |a - b| < |a - b|
⊢ False
Theorem: C03S06.convergesTo_unique
Proof state before:
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
⊢ |a - b| > 0
Tactic:
apply lt_of_le_of_ne
Proof state after:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
⊢ 0 ≤ |a - b|

case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
⊢ 0 ≠ |a - b|
Theorem: C03S06.convergesTo_unique
Proof state before:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
⊢ 0 ≠ |a - b|
Tactic:
intro h''
Proof state after:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
h'' : 0 = |a - b|
⊢ False
Theorem: C03S06.convergesTo_unique
Proof state before:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
h'' : 0 = |a - b|
⊢ False
Tactic:
apply abne
Proof state after:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
h'' : 0 = |a - b|
⊢ a = b
Theorem: C03S06.convergesTo_unique
Proof state before:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
h'' : 0 = |a - b|
⊢ a = b
Tactic:
apply eq_of_abs_sub_eq_zero h''.symm
Proof state after:
no goals
Theorem: C03S06.convergesTo_unique
Proof state before:
case a
s : ℕ → ℝ
a b : ℝ
sa : ConvergesTo s a
sb : ConvergesTo s b
abne : ¬a = b
⊢ 0 ≤ |a - b|
Tactic:
apply abs_nonneg
Proof state after:
no goals
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
Na : ℕ
hNa : ∀ n ≥ Na, |s n - a| < ε
Nb : ℕ
hNb : ∀ n ≥ Nb, |s n - b| < ε
N : ℕ := max Na Nb
⊢ |s N - a| < ε
Tactic:
apply hNa
Proof state after:
case a
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
⊢ N ≥ Na
Theorem: C03S06.convergesTo_unique
Proof state before:
case a
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
⊢ N ≥ Na
Tactic:
apply le_max_left
Proof state after:
no goals