uniqueness_of_limits.lean

-- Uniqueness of limits in a metric space.
-- https://www.codewars.com/kata/5ea1f341014f0c0001ec7c5e

import algebra.order
import algebra.ordered_field
import topology.metric_space.basic

def converges_to {X : Type*} [metric_space X] (s : ℕ → X) (x : X) :=
∀ (ε : ℝ) (hε : 0 < ε), ∃ N : ℕ, ∀ (n : ℕ) (hn : N ≤ n), dist x (s n) < ε

notation s ` ⟶ ` x := converges_to s x

theorem limit_unique {X : Type*} [metric_space X] {s : ℕ → X}
  (x₀ x₁ : X) (h₀ : s ⟶ x₀) (h₁ : s ⟶ x₁)
: x₀ = x₁ := begin
  apply eq_of_dist_eq_zero,
  by_contradiction hnz,
  let ε := dist x₀ x₁ / 2,
  have hgz: 0 < ε, by {
    dsimp [ε],
    apply half_pos,
    exact lt_of_le_of_ne dist_nonneg (ne.symm hnz)
  },
  cases h₀ ε hgz with N₀ hN₀,
  cases h₁ ε hgz with N₁ hN₁,
  let N := max N₀ N₁,
  have hc: dist x₀ x₁ < ε + ε, by {
    apply lt_of_le_of_lt,
    -- (dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z)
    { exact dist_triangle x₀ (s N) x₁ },
    apply add_lt_add_of_le_of_lt,
    { apply le_of_lt, apply hN₀, apply le_max_left },
    { rw dist_comm, apply hN₁, apply le_max_right },
  },
  dsimp [ε] at hc,
  rwa add_halves at hc,
  exact lt_irrefl _ hc,
end

uniqueness_show_term_output.lean

-- Uniqueness of limits in a metric space.
-- https://www.codewars.com/kata/5ea1f341014f0c0001ec7c5e

import algebra.order
import algebra.ordered_field
import topology.metric_space.basic

def converges_to {X : Type*} [metric_space X] (s : ℕ → X) (x : X) :=
∀ (ε : ℝ) (hε : 0 < ε), ∃ N : ℕ, ∀ (n : ℕ) (hn : N ≤ n), dist x (s n) < ε

notation s ` ⟶ ` x := converges_to s x

theorem limit_unique {X : Type*} [metric_space X] {s : ℕ → X}
  (x₀ x₁ : X) (h₀ : s ⟶ x₀) (h₁ : s ⟶ x₁)
: x₀ = x₁ :=
eq_of_dist_eq_zero
  (decidable.by_contradiction
     (λ (hnz : ¬dist x₀ x₁ = 0),
        let ε : ℝ := dist x₀ x₁ / 2
        in Exists.dcases_on (h₀ ε (id (half_pos (lt_of_le_of_ne dist_nonneg (ne.symm hnz)))))
             (λ (N₀ : ℕ) (hN₀ : ∀ (n : ℕ), N₀ ≤ n → dist x₀ (s n) < ε),
                Exists.dcases_on (h₁ ε (id (half_pos (lt_of_le_of_ne dist_nonneg (ne.symm hnz)))))
                  (λ (N₁ : ℕ) (hN₁ : ∀ (n : ℕ), N₁ ≤ n → dist x₁ (s n) < ε),
                     let N : ℕ := max N₀ N₁
                     in id
                          (λ (hc : dist x₀ x₁ < dist x₀ x₁ / 2 + dist x₀ x₁ / 2),
                             lt_irrefl (dist x₀ x₁)
                               (eq.mp
                                  -- 31:36: invalid 'eq.rec' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but expected type must not contain metavariables
                                  --  ?m_1 = (dist x₀ x₁ < dist x₀ x₁)
                                  (eq.rec (eq.refl (dist x₀ x₁ < dist x₀ x₁ / 2 + dist x₀ x₁ / 2))
                                     (add_halves (dist x₀ x₁)))
                                  hc))
                          (lt_of_le_of_lt (dist_triangle x₀ (s N) x₁)
                             (add_lt_add_of_le_of_lt (le_of_lt (hN₀ N (le_max_left N₀ N₁)))
                                      -- 38:39: invalid 'eq.rec' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but expected type must not contain metavariables
                                      --  ?m_1
                                ((id (eq.rec (eq.refl (dist (s N) x₁ < ε)) (dist_comm (s N) x₁))).mpr
                                   (hN₁ N (le_max_right N₀ N₁)))))))))