Theorem: LoVe.CauchySeq.Setoid_add (LoVe/Lectures/LoVe14_RationalAndRealNumbers_Demo.lean)

State before:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
⊢ f + g ≈ f' + g'
Tactic:
intro ε₀ hε₀
State after:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
⊢ ∃ N, ∀ (m : ℕ), m ≥ N → |seqOf (f + g) m - seqOf (f' + g') m| < ε₀

State before:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
⊢ ∃ N, ∀ (m : ℕ), m ≥ N → |seqOf (f + g) m - seqOf (f' + g') m| < ε₀
Tactic:
simp [Setoid_iff]
State after:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
⊢ ∃ N, ∀ (m : ℕ), N ≤ m → |seqOf (f + g) m - seqOf (f' + g') m| < ε₀

State before:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
⊢ ∃ N, ∀ (m : ℕ), N ≤ m → |seqOf (f + g) m - seqOf (f' + g') m| < ε₀
Tactic:
cases hf (ε₀ / 2) (half_pos hε₀) with
| intro Nf hNf =>
  cases hg (ε₀ / 2) (half_pos hε₀) with
  | intro Ng hNg =>
    apply Exists.intro (max Nf Ng)
    intro m hm
    calc
      abs (seqOf (f + g) m - seqOf (f' + g') m)
      = abs ((seqOf f m + seqOf g m)
        - (seqOf f' m + seqOf g' m)) :=
        by rfl
      _ = abs ((seqOf f m - seqOf f' m)
          + (seqOf g m - seqOf g' m)) :=
        by
          have arg_eq :
            seqOf f m + seqOf g m
              - (seqOf f' m + seqOf g' m) =
            seqOf f m - seqOf f' m
              + (seqOf g m - seqOf g' m) :=
            by linarith
          rw [arg_eq]
      _ ≤ abs (seqOf f m - seqOf f' m)
          + abs (seqOf g m - seqOf g' m) :=
        by apply abs_add
      _ < ε₀ / 2 + ε₀ / 2 :=
        add_lt_add (hNf m (le_of_max_le_left hm))
          (hNg m (le_of_max_le_right hm))
      _ = ε₀ :=
        by simp
State after:
no goals

State before:
case intro
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
⊢ ∃ N, ∀ (m : ℕ), N ≤ m → |seqOf (f + g) m - seqOf (f' + g') m| < ε₀
Tactic:
cases hg (ε₀ / 2) (half_pos hε₀) with
| intro Ng hNg =>
  apply Exists.intro (max Nf Ng)
  intro m hm
  calc
    abs (seqOf (f + g) m - seqOf (f' + g') m)
    = abs ((seqOf f m + seqOf g m)
      - (seqOf f' m + seqOf g' m)) :=
      by rfl
    _ = abs ((seqOf f m - seqOf f' m)
        + (seqOf g m - seqOf g' m)) :=
      by
        have arg_eq :
          seqOf f m + seqOf g m
            - (seqOf f' m + seqOf g' m) =
          seqOf f m - seqOf f' m
            + (seqOf g m - seqOf g' m) :=
          by linarith
        rw [arg_eq]
    _ ≤ abs (seqOf f m - seqOf f' m)
        + abs (seqOf g m - seqOf g' m) :=
      by apply abs_add
    _ < ε₀ / 2 + ε₀ / 2 :=
      add_lt_add (hNf m (le_of_max_le_left hm))
        (hNg m (le_of_max_le_right hm))
    _ = ε₀ :=
      by simp
State after:
no goals

State before:
case intro.intro
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
⊢ ∃ N, ∀ (m : ℕ), N ≤ m → |seqOf (f + g) m - seqOf (f' + g') m| < ε₀
Tactic:
apply Exists.intro (max Nf Ng)
State after:
case intro.intro
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
⊢ ∀ (m : ℕ), max Nf Ng ≤ m → |seqOf (f + g) m - seqOf (f' + g') m| < ε₀

State before:
case intro.intro
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
⊢ ∀ (m : ℕ), max Nf Ng ≤ m → |seqOf (f + g) m - seqOf (f' + g') m| < ε₀
Tactic:
intro m hm
State after:
case intro.intro
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
m : ℕ
hm : max Nf Ng ≤ m
⊢ |seqOf (f + g) m - seqOf (f' + g') m| < ε₀

State before:
case intro.intro
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
m : ℕ
hm : max Nf Ng ≤ m
⊢ |seqOf (f + g) m - seqOf (f' + g') m| < ε₀
Tactic:
calc
  abs (seqOf (f + g) m - seqOf (f' + g') m)
  = abs ((seqOf f m + seqOf g m)
    - (seqOf f' m + seqOf g' m)) :=
    by rfl
  _ = abs ((seqOf f m - seqOf f' m)
      + (seqOf g m - seqOf g' m)) :=
    by
      have arg_eq :
        seqOf f m + seqOf g m
          - (seqOf f' m + seqOf g' m) =
        seqOf f m - seqOf f' m
          + (seqOf g m - seqOf g' m) :=
        by linarith
      rw [arg_eq]
  _ ≤ abs (seqOf f m - seqOf f' m)
      + abs (seqOf g m - seqOf g' m) :=
    by apply abs_add
  _ < ε₀ / 2 + ε₀ / 2 :=
    add_lt_add (hNf m (le_of_max_le_left hm))
      (hNg m (le_of_max_le_right hm))
  _ = ε₀ :=
    by simp
State after:
no goals

State before:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
m : ℕ
hm : max Nf Ng ≤ m
⊢ |seqOf (f + g) m - seqOf (f' + g') m| = |seqOf f m + seqOf g m - (seqOf f' m + seqOf g' m)|
Tactic:
rfl
State after:
no goals

State before:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
m : ℕ
hm : max Nf Ng ≤ m
⊢ |seqOf f m + seqOf g m - (seqOf f' m + seqOf g' m)| = |seqOf f m - seqOf f' m + (seqOf g m - seqOf g' m)|
Tactic:
have arg_eq :
  seqOf f m + seqOf g m
    - (seqOf f' m + seqOf g' m) =
  seqOf f m - seqOf f' m
    + (seqOf g m - seqOf g' m) :=
  by linarith
State after:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
m : ℕ
hm : max Nf Ng ≤ m
arg_eq : seqOf f m + seqOf g m - (seqOf f' m + seqOf g' m) = seqOf f m - seqOf f' m + (seqOf g m - seqOf g' m)
⊢ |seqOf f m + seqOf g m - (seqOf f' m + seqOf g' m)| = |seqOf f m - seqOf f' m + (seqOf g m - seqOf g' m)|

State before:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
m : ℕ
hm : max Nf Ng ≤ m
arg_eq : seqOf f m + seqOf g m - (seqOf f' m + seqOf g' m) = seqOf f m - seqOf f' m + (seqOf g m - seqOf g' m)
⊢ |seqOf f m + seqOf g m - (seqOf f' m + seqOf g' m)| = |seqOf f m - seqOf f' m + (seqOf g m - seqOf g' m)|
Tactic:
rw [arg_eq]
State after:
no goals

State before:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
m : ℕ
hm : max Nf Ng ≤ m
⊢ seqOf f m + seqOf g m - (seqOf f' m + seqOf g' m) = seqOf f m - seqOf f' m + (seqOf g m - seqOf g' m)
Tactic:
linarith
State after:
no goals

State before:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
m : ℕ
hm : max Nf Ng ≤ m
⊢ |seqOf f m - seqOf f' m + (seqOf g m - seqOf g' m)| ≤ |seqOf f m - seqOf f' m| + |seqOf g m - seqOf g' m|
Tactic:
apply abs_add
State after:
no goals

State before:
f f' g g' : CauchySeq
hf : f ≈ f'
hg : g ≈ g'
ε₀ : ℚ
hε₀ : ε₀ > 0
Nf : ℕ
hNf : ∀ (m : ℕ), m ≥ Nf → |seqOf f m - seqOf f' m| < ε₀ / 2
Ng : ℕ
hNg : ∀ (m : ℕ), m ≥ Ng → |seqOf g m - seqOf g' m| < ε₀ / 2
m : ℕ
hm : max Nf Ng ≤ m
⊢ ε₀ / 2 + ε₀ / 2 = ε₀
Tactic:
simp
State after:
no goals