internlm/Lean-Github huggingface dataset:
Theorem: chineseMap_surj
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
⊢ ∀ (i : ι), ∃ e, (mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → (mk (I j)) e = 0
Tactic:
intro i
Proof state after:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
i : ι
⊢ ∃ e, (mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → (mk (I j)) e = 0
Theorem: chineseMap_surj
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
i : ι
⊢ ∃ e, (mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → (mk (I j)) e = 0
Tactic:
have hI' : ∀ j ∈ ({i} : Finset ι)ᶜ, IsCoprime (I i) (I j) := by
  intros j hj
  exact hI _ _ (by simpa [ne_comm, isCoprime_iff_add] using hj)
Proof state after:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
⊢ ∃ e, (mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → (mk (I j)) e = 0
Theorem: chineseMap_surj
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
⊢ ∃ e, (mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → (mk (I j)) e = 0
Tactic:
rcases isCoprime_iff_exists.mp (isCoprime_Inf hI') with ⟨u, hu, e, he, hue⟩
Proof state after:
case intro.intro.intro.intro
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
he : e ∈ ⨅ j ∈ {i}ᶜ, I j
hue : u + e = 1
⊢ ∃ e, (mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → (mk (I j)) e = 0
Theorem: chineseMap_surj
Proof state before:
case intro.intro.intro.intro
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
he : e ∈ ⨅ j ∈ {i}ᶜ, I j
hue : u + e = 1
⊢ ∃ e, (mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → (mk (I j)) e = 0
Tactic:
replace he : ∀ j, j ≠ i → e ∈ I j := by simpa using he
Proof state after:
case intro.intro.intro.intro
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
hue : u + e = 1
he : ∀ (j : ι), j ≠ i → e ∈ I j
⊢ ∃ e, (mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → (mk (I j)) e = 0
Theorem: chineseMap_surj
Proof state before:
case intro.intro.intro.intro
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
hue : u + e = 1
he : ∀ (j : ι), j ≠ i → e ∈ I j
⊢ ∃ e, (mk (I i)) e = 1 ∧ ∀ (j : ι), j ≠ i → (mk (I j)) e = 0
Tactic:
refine ⟨e, ?_, ?_⟩
Proof state after:
case intro.intro.intro.intro.refine_1
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
hue : u + e = 1
he : ∀ (j : ι), j ≠ i → e ∈ I j
⊢ (mk (I i)) e = 1

case intro.intro.intro.intro.refine_2
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
hue : u + e = 1
he : ∀ (j : ι), j ≠ i → e ∈ I j
⊢ ∀ (j : ι), j ≠ i → (mk (I j)) e = 0
Theorem: chineseMap_surj
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
i : ι
⊢ ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
Tactic:
intros j hj
Proof state after:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
i j : ι
hj : j ∈ {i}ᶜ
⊢ IsCoprime (I i) (I j)
Theorem: chineseMap_surj
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
i j : ι
hj : j ∈ {i}ᶜ
⊢ IsCoprime (I i) (I j)
Tactic:
exact hI _ _ (by simpa [ne_comm, isCoprime_iff_add] using hj)
Proof state after:
no goals
Theorem: chineseMap_surj
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
i j : ι
hj : j ∈ {i}ᶜ
⊢ i ≠ j
Tactic:
simpa [ne_comm, isCoprime_iff_add] using hj
Proof state after:
no goals
Theorem: chineseMap_surj
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
he : e ∈ ⨅ j ∈ {i}ᶜ, I j
hue : u + e = 1
⊢ ∀ (j : ι), j ≠ i → e ∈ I j
Tactic:
simpa using he
Proof state after:
no goals
Theorem: chineseMap_surj
Proof state before:
case intro.intro.intro.intro.refine_1
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
hue : u + e = 1
he : ∀ (j : ι), j ≠ i → e ∈ I j
⊢ (mk (I i)) e = 1
Tactic:
simp [eq_sub_of_add_eq' hue, map_sub, eq_zero_iff_mem.mpr hu]
Proof state after:
no goals
Theorem: chineseMap_surj
Proof state before:
case intro.intro.intro.intro.refine_2
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
i : ι
hI' : ∀ j ∈ {i}ᶜ, IsCoprime (I i) (I j)
u : R
hu : u ∈ I i
e : R
hue : u + e = 1
he : ∀ (j : ι), j ≠ i → e ∈ I j
⊢ ∀ (j : ι), j ≠ i → (mk (I j)) e = 0
Tactic:
exact fun j hj ↦ eq_zero_iff_mem.mpr (he j hj)
Proof state after:
no goals
Theorem: chineseMap_surj
Proof state before:
case h.h
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), (mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (mk (I j)) (e i) = 0
i : ι
⊢ (mk (I i)) (f i * e i) = g i
Tactic:
simp [(he i).1, hf]
Proof state after:
no goals
Theorem: chineseMap_surj
Proof state before:
case h.h
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), (mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (mk (I j)) (e i) = 0
i : ι
⊢ ∀ (x : ι), x ≠ i → (mk (I i)) (f x * e x) = 0
Tactic:
intros j hj
Proof state after:
case h.h
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), (mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (mk (I j)) (e i) = 0
i j : ι
hj : j ≠ i
⊢ (mk (I i)) (f j * e j) = 0
Theorem: chineseMap_surj
Proof state before:
case h.h
ι : Type u_1
R : Type u_2
inst✝¹ : CommRing R
inst✝ : Fintype ι
I : ι → Ideal R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
g : Π (i : ι), R ⧸ I i
f : ι → R
hf : ∀ (i : ι), (mk (I i)) (f i) = g i
e : ι → R
he : ∀ (i : ι), (mk (I i)) (e i) = 1 ∧ ∀ (j : ι), j ≠ i → (mk (I j)) (e i) = 0
i j : ι
hj : j ≠ i
⊢ (mk (I i)) (f j * e j) = 0
Tactic:
simp [(he j).2 i hj.symm]
Proof state after:
no goals
Theorem: C06S01.Point.add_comm
Proof state before:
a b : Point
⊢ a.add b = b.add a
Tactic:
rw [add, add]
Proof state after:
a b : Point
⊢ { x := a.x + b.x, y := a.y + b.y, z := a.z + b.z } = { x := b.x + a.x, y := b.y + a.y, z := b.z + a.z }
Theorem: C06S01.Point.add_comm
Proof state before:
a b : Point
⊢ { x := a.x + b.x, y := a.y + b.y, z := a.z + b.z } = { x := b.x + a.x, y := b.y + a.y, z := b.z + a.z }
Tactic:
ext <;> dsimp
Proof state after:
case x
a b : Point
⊢ a.x + b.x = b.x + a.x

case y
a b : Point
⊢ a.y + b.y = b.y + a.y

case z
a b : Point
⊢ a.z + b.z = b.z + a.z
Theorem: C06S01.Point.add_comm
Proof state before:
case x
a b : Point
⊢ a.x + b.x = b.x + a.x

case y
a b : Point
⊢ a.y + b.y = b.y + a.y

case z
a b : Point
⊢ a.z + b.z = b.z + a.z
Tactic:
repeat' apply add_comm
Proof state after:
no goals
Theorem: C06S01.Point.add_comm
Proof state before:
case z
a b : Point
⊢ a.z + b.z = b.z + a.z
Tactic:
apply add_comm
Proof state after:
no goals
Theorem: C06S01.Point.addAlt_x
Proof state before:
a b : Point
⊢ (a.addAlt b).x = a.x + b.x
Tactic:
rfl
Proof state after:
no goals
Theorem: C06S01.Point.addAlt_comm
Proof state before:
a b : Point
⊢ a.addAlt b = b.addAlt a
Tactic:
rw [addAlt, addAlt]
Proof state after:
a b : Point
⊢ (match a, b with
    | { x := x₁, y := y₁, z := z₁ }, { x := x₂, y := y₂, z := z₂ } => { x := x₁ + x₂, y := y₁ + y₂, z := z₁ + z₂ }) =
    match b, a with
    | { x := x₁, y := y₁, z := z₁ }, { x := x₂, y := y₂, z := z₂ } => { x := x₁ + x₂, y := y₁ + y₂, z := z₁ + z₂ }
Theorem: C06S01.Point.addAlt_comm
Proof state before:
a b : Point
⊢ (match a, b with
    | { x := x₁, y := y₁, z := z₁ }, { x := x₂, y := y₂, z := z₂ } => { x := x₁ + x₂, y := y₁ + y₂, z := z₁ + z₂ }) =
    match b, a with
    | { x := x₁, y := y₁, z := z₁ }, { x := x₂, y := y₂, z := z₂ } => { x := x₁ + x₂, y := y₁ + y₂, z := z₁ + z₂ }
Tactic:
ext <;> dsimp
Proof state after:
case x
a b : Point
⊢ a.x + b.x = b.x + a.x

case y
a b : Point
⊢ a.y + b.y = b.y + a.y

case z
a b : Point
⊢ a.z + b.z = b.z + a.z
Theorem: C06S01.Point.addAlt_comm
Proof state before:
case x
a b : Point
⊢ a.x + b.x = b.x + a.x

case y
a b : Point
⊢ a.y + b.y = b.y + a.y

case z
a b : Point
⊢ a.z + b.z = b.z + a.z
Tactic:
repeat' apply add_comm
Proof state after:
no goals
Theorem: C06S01.Point.addAlt_comm
Proof state before:
case z
a b : Point
⊢ a.z + b.z = b.z + a.z
Tactic:
apply add_comm
Proof state after:
no goals
Theorem: C06S01.Point.add_assoc
Proof state before:
a b c : Point
⊢ (a.add b).add c = a.add (b.add c)
Tactic:
simp [add, add_assoc]
Proof state after:
no goals
Theorem: C06S01.Point.smul_distrib
Proof state before:
r : ℝ
a b : Point
⊢ (smul r a).add (smul r b) = smul r (a.add b)
Tactic:
simp [add, smul, mul_add]
Proof state after:
no goals
Theorem: C03S06.convergesTo_const
Proof state before:
a : ℝ
⊢ ConvergesTo (fun x => a) a
Tactic:
intro ε εpos
Proof state after:
a ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun x => a) n - a| < ε
Theorem: C03S06.convergesTo_const
Proof state before:
a ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun x => a) n - a| < ε
Tactic:
use 0
Proof state after:
case h
a ε : ℝ
εpos : ε > 0
⊢ ∀ n ≥ 0, |(fun x => a) n - a| < ε
Theorem: C03S06.convergesTo_const
Proof state before:
case h
a ε : ℝ
εpos : ε > 0
⊢ ∀ n ≥ 0, |(fun x => a) n - a| < ε
Tactic:
intro n nge
Proof state after:
case h
a ε : ℝ
εpos : ε > 0
n : ℕ
nge : n ≥ 0
⊢ |(fun x => a) n - a| < ε
Theorem: C03S06.convergesTo_const
Proof state before:
case h
a ε : ℝ
εpos : ε > 0
n : ℕ
nge : n ≥ 0
⊢ |(fun x => a) n - a| < ε
Tactic:
rw [sub_self, abs_zero]
Proof state after:
case h
a ε : ℝ
εpos : ε > 0
n : ℕ
nge : n ≥ 0
⊢ 0 < ε
Theorem: C03S06.convergesTo_const
Proof state before:
case h
a ε : ℝ
εpos : ε > 0
n : ℕ
nge : n ≥ 0
⊢ 0 < ε
Tactic:
apply εpos
Proof state after:
no goals
Theorem: C03S06.convergesTo_add
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:
intro ε εpos
Proof state after:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun n => s n + t n) n - (a + b)| < ε
Theorem: C03S06.convergesTo_add
Proof state before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun n => s n + t n) n - (a + b)| < ε
Tactic:
dsimp
Proof state after:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |s n + t n - (a + b)| < ε
Theorem: C03S06.convergesTo_add
Proof state before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |s n + t n - (a + b)| < ε
Tactic:
have ε2pos : 0 < ε / 2 := by linarith
Proof state after:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
⊢ ∃ N, ∀ n ≥ N, |s n + t n - (a + b)| < ε
Theorem: C03S06.convergesTo_add
Proof state before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
⊢ ∃ N, ∀ n ≥ N, |s n + t n - (a + b)| < ε
Tactic:
rcases cs (ε / 2) ε2pos with ⟨Ns, hs⟩
Proof state after:
case intro
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
⊢ ∃ N, ∀ n ≥ N, |s n + t n - (a + b)| < ε
Theorem: C03S06.convergesTo_add
Proof state before:
case intro
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
⊢ ∃ N, ∀ n ≥ N, |s n + t n - (a + b)| < ε
Tactic:
rcases ct (ε / 2) ε2pos with ⟨Nt, ht⟩
Proof state after:
case intro.intro
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, ∀ n ≥ N, |s n + t n - (a + b)| < ε
Theorem: C03S06.convergesTo_add
Proof state before:
case intro.intro
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, ∀ n ≥ N, |s n + t n - (a + b)| < ε
Tactic:
use max Ns Nt
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 ≥ 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 ≥ max Ns Nt, |s n + t n - (a + b)| < ε
Tactic:
sorry
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
⊢ 0 < ε / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: C03S06.convergesTo_addαα
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:
intro ε εpos
Proof state after:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun n => s n + t n) n - (a + b)| < ε
Theorem: C03S06.convergesTo_addαα
Proof state before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |(fun n => s n + t n) n - (a + b)| < ε
Tactic:
dsimp
Proof state after:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |s n + t n - (a + b)| < ε
Theorem: C03S06.convergesTo_addαα
Proof state before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ n ≥ N, |s n + t n - (a + b)| < ε
Tactic:
have ε2pos : 0 < ε / 2 := by linarith
Proof state after:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
⊢ ∃ N, ∀ n ≥ N, |s n + t n - (a + b)| < ε
Theorem: C03S06.convergesTo_addαα
Proof state before:
s t : ℕ → ℝ
a b : ℝ
cs : ConvergesTo s a
ct : ConvergesTo t b
ε : ℝ
εpos : ε > 0
ε2pos : 0 < ε / 2
⊢ ∃ N, ∀ n ≥ N, |s n + t n - (a + b)| < ε
Tactic:
rcases cs (ε / 2) ε2pos with ⟨Ns, hs⟩
Proof state after:
case intro
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
⊢ ∃ N, ∀ n ≥ N, |s n + t n - (a + b)| < ε
Theorem: C03S06.convergesTo_addαα
Proof state before:
case intro
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
⊢ ∃ N, ∀ n ≥ N, |s n + t n - (a + b)| < ε
Tactic:
rcases ct (ε / 2) ε2pos with ⟨Nt, ht⟩
Proof state after:
case intro.intro
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, ∀ n ≥ N, |s n + t n - (a + b)| < ε
Theorem: C03S06.convergesTo_addαα
Proof state before:
case intro.intro
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, ∀ n ≥ N, |s n + t n - (a + b)| < ε
Tactic:
use max Ns Nt
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 ≥ 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 ≥ 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
⊢ 0 < ε / 2
Tactic:
linarith
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:
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:
sorry
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