Analysis
B.2. The decimal representation of real numbers

Imports

import Mathlib.Tactic
import Analysis.Appendix_B_1

Analysis I, Appendix B.2: The decimal representation of real numbers

An implementation of the decimal representation of Mathlib's real numbers ℝ.

This is separate from the way decimal numerals are already represented in Mathlib. We also represent the integer part of the natural numbers just by ℕ, avoiding using the decimal representation from the previous section, although we still retain the AppendixB.Digit class.

namespace AppendixB

structure NNRealDecimal where
  intPart : ℕ
  fracPart : ℕ → Digit

open NNReal NNRealDecimalAppendixB.NNRealDecimal.mk (intPart : ℕ) (fracPart : ℕ → Digit) : NNRealDecimal#check mk

AppendixB.NNRealDecimal.mk (intPart : ℕ) (fracPart : ℕ → Digit) : NNRealDecimal

@[coe]
noncomputable def NNRealDecimal.toNNReal (d:NNRealDecimal) : NNReal :=
  d.intPart + ∑' i, (d.fracPart i) * (10:NNReal) ^ (-i-1:ℝ)

noncomputable instance NNRealDecimal.instCoeNNReal : Coe NNRealDecimal NNReal where
  coe := toNNReal

Exercise B.2.1

theorem declaration uses `sorry`NNRealDecimal.toNNReal_conv (d:NNRealDecimal) :
  Summable fun i ↦ (d.fracPart i) * (10:NNReal) ^ (-i-1:ℝ) := byd:NNRealDecimal⊢ Summable fun i ↦ ↑↑(d.fracPart i) * 10 ^ (-↑i - 1)
  sorryAll goals completed! 🐙

theorem NNRealDecimal.surj (x:NNReal) : ∃ d:NNRealDecimal, x = d := byx:ℝ≥0⊢ ∃ d, x = ↑d
  -- This proof is written to follow the structure of the original text.
  by_cases h : x = 0posx:ℝ≥0h:x = 0⊢ ∃ d, x = ↑dnegx:ℝ≥0h:¬x = 0⊢ ∃ d, x = ↑d
  .posx:ℝ≥0h:x = 0⊢ ∃ d, x = ↑d use mk 0 fun _ ↦ 0hx:ℝ≥0h:x = 0⊢ x = ↑{ intPart := 0, fracPart := fun x ↦ 0 }; simp [h, toNNReal]All goals completed! 🐙
  let s : ℕ → ℕ := fun n ↦ ⌊ x * 10^n ⌋₊negx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊⊢ ∃ d, x = ↑d
  have hs (n:ℕ) : s n ≤ x * 10^n := Nat.floor_le (byx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊n:ℕ⊢ 0 ≤ x * 10 ^ n positivityAll goals completed! 🐙)
  have hs' (n:ℕ) : x * 10^n < s n + 1 := Nat.lt_floor_add_one _negx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1⊢ ∃ d, x = ↑d
  have hdigit (n:ℕ) : ∃ a:Digit, s (n+1) = 10 * s n + (a:ℕ) := byx:ℝ≥0⊢ ∃ d, x = ↑d
    have hl : (10:NNReal) * s n < s (n+1) + 1 := calc
      _ ≤ 10 * (x * 10^n) := byx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1n:ℕ⊢ 10 * ↑(s n) ≤ 10 * (x * 10 ^ n) gcongrbcx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1n:ℕ⊢ ↑(s n) ≤ x * 10 ^ n; grindAll goals completed! 🐙
      _ = x * 10^(n+1) := byx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1n:ℕ⊢ 10 * (x * 10 ^ n) = x * 10 ^ (n + 1) ring_nfAll goals completed! 🐙
      _ < _ := hs' _
    have hu : s (n+1) < (10:NNReal) * s n + 10 := calc
      _ ≤ x * 10^(n+1) := hs (n+1)
      _ = 10 * (x * 10^n) := byx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1n:ℕhl:10 * ↑(s n) < ↑(s (n + 1)) + 1⊢ x * 10 ^ (n + 1) = 10 * (x * 10 ^ n) ring_nfAll goals completed! 🐙
      _ < 10 * (s n + 1) := byx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1n:ℕhl:10 * ↑(s n) < ↑(s (n + 1)) + 1⊢ 10 * (x * 10 ^ n) < 10 * (↑(s n) + 1) gcongrhbcx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1n:ℕhl:10 * ↑(s n) < ↑(s (n + 1)) + 1⊢ x * 10 ^ n < ↑(s n) + 1; grindAll goals completed! 🐙
      _ = _ := byx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1n:ℕhl:10 * ↑(s n) < ↑(s (n + 1)) + 1⊢ 10 * (↑(s n) + 1) = 10 * ↑(s n) + 10 ringAll goals completed! 🐙
    norm_cast at hl hux:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1n:ℕhl:10 * s n < s (n + 1) + 1hu:s (n + 1) < 10 * s n + 10⊢ ∃ a, s (n + 1) = 10 * s n + ↑a
    set d := s (n+1) - 10 * s nx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1n:ℕhl:10 * s n < s (n + 1) + 1hu:s (n + 1) < 10 * s n + 10d:ℕ := s (n + 1) - 10 * s n⊢ ∃ a, s (n + 1) = 10 * s n + ↑a
    have hd : d < 10 := byx:ℝ≥0⊢ ∃ d, x = ↑d omegaAll goals completed! 🐙
    have : s (n+1) = 10 * s n + d := byx:ℝ≥0⊢ ∃ d, x = ↑d omegaAll goals completed! 🐙
    use Digit.mk hdAll goals completed! 🐙
  choose a ha using hdigitnegx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)⊢ ∃ d, x = ↑d
  set d := mk (s 0) anegx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }⊢ ∃ d, x = ↑d; use dhx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }⊢ x = ↑d
  have hsum (n:ℕ) : s n * (10:NNReal)^(-n:ℝ) = s 0 + ∑ i ∈ .range n, a i * (10:NNReal)^(-i-1:ℝ) := byx:ℝ≥0⊢ ∃ d, x = ↑d
    induction' n with n hnzerox:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }⊢ ↑(s 0) * 10 ^ (-↑0) = ↑(s 0) + ∑ i ∈ Finset.range 0, ↑↑(a i) * 10 ^ (-↑i - 1)succx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }n:ℕhn:↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)⊢ ↑(s (n + 1)) * 10 ^ (-↑(n + 1)) = ↑(s 0) + ∑ i ∈ Finset.range (n + 1), ↑↑(a i) * 10 ^ (-↑i - 1); simpsuccx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }n:ℕhn:↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)⊢ ↑(s (n + 1)) * 10 ^ (-↑(n + 1)) = ↑(s 0) + ∑ i ∈ Finset.range (n + 1), ↑↑(a i) * 10 ^ (-↑i - 1)
    rw [ha n]succx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }n:ℕhn:↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)⊢ ↑(10 * s n + ↑(a n)) * 10 ^ (-↑(n + 1)) = ↑(s 0) + ∑ i ∈ Finset.range (n + 1), ↑↑(a i) * 10 ^ (-↑i - 1); calc
      _ = s n * (10:NNReal)^(-n:ℝ) + a n * 10^(-n-1:ℝ) := byx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }n:ℕhn:↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)⊢ ↑(10 * s n + ↑(a n)) * 10 ^ (-↑(n + 1)) = ↑(s n) * 10 ^ (-↑n) + ↑↑(a n) * 10 ^ (-↑n - 1)
        simp [add_mul]x:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }n:ℕhn:↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)⊢ 10 * ↑(s n) * 10 ^ (-1 + -↑n) + ↑↑(a n) * 10 ^ (-1 + -↑n) = ↑(s n) * 10 ^ (-↑n) + ↑↑(a n) * 10 ^ (-↑n - 1); ring_nfx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }n:ℕhn:↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)⊢ ↑(s n) * 10 ^ (-1 - ↑n) * 10 + 10 ^ (-1 - ↑n) * ↑↑(a n) = ↑(s n) * 10 ^ (-↑n) + 10 ^ (-1 - ↑n) * ↑↑(a n); congr 1e_ax:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }n:ℕhn:↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)⊢ ↑(s n) * 10 ^ (-1 - ↑n) * 10 = ↑(s n) * 10 ^ (-↑n)
        rw [mul_assoc, ←rpow_add_one]e_ax:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }n:ℕhn:↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)⊢ ↑(s n) * 10 ^ (-1 - ↑n + 1) = ↑(s n) * 10 ^ (-↑n)e_a.hxx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }n:ℕhn:↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)⊢ 10 ≠ 0; ring_nfe_a.hxx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }n:ℕhn:↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)⊢ 10 ≠ 0; norm_numAll goals completed! 🐙
      _ = s 0 + (∑ i ∈ .range n, a i * (10:NNReal)^(-i-1:ℝ) + a n * 10^(-n-1:ℝ)) := byx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }n:ℕhn:↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)⊢ ↑(s n) * 10 ^ (-↑n) + ↑↑(a n) * 10 ^ (-↑n - 1) =
  ↑(s 0) + (∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1) + ↑↑(a n) * 10 ^ (-↑n - 1)) grindAll goals completed! 🐙
      _ = _ := byx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }n:ℕhn:↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)⊢ ↑(s 0) + (∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1) + ↑↑(a n) * 10 ^ (-↑n - 1)) =
  ↑(s 0) + ∑ i ∈ Finset.range (n + 1), ↑↑(a i) * 10 ^ (-↑i - 1) congre_ax:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }n:ℕhn:↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)⊢ ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1) + ↑↑(a n) * 10 ^ (-↑n - 1) =
  ∑ i ∈ Finset.range (n + 1), ↑↑(a i) * 10 ^ (-↑i - 1); symme_ax:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }n:ℕhn:↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)⊢ ∑ i ∈ Finset.range (n + 1), ↑↑(a i) * 10 ^ (-↑i - 1) =
  ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1) + ↑↑(a n) * 10 ^ (-↑n - 1); apply Finset.sum_range_succAll goals completed! 🐙
  have := (d.toNNReal_conv.tendsto_sum_tsum_nat).const_add (s 0:NNReal)hx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun x ↦ ↑(s 0) + ∑ i ∈ Finset.range x, ↑↑(d.fracPart i) * 10 ^ (-↑i - 1)) Filter.atTop
  (nhds (↑(s 0) + ∑' (i : ℕ), ↑↑(d.fracPart i) * 10 ^ (-↑i - 1)))⊢ x = ↑d
  convert_to Filter.atTop.Tendsto (fun n ↦ s n * (10:NNReal)^(-n:ℝ)) (nhds (d:NNReal)) at thish.e'_3x:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun x ↦ ↑(s 0) + ∑ i ∈ Finset.range x, ↑↑(d.fracPart i) * 10 ^ (-↑i - 1)) Filter.atTop
  (nhds (↑(s 0) + ∑' (i : ℕ), ↑↑(d.fracPart i) * 10 ^ (-↑i - 1)))⊢ (fun x ↦ ↑(s 0) + ∑ i ∈ Finset.range x, ↑↑(d.fracPart i) * 10 ^ (-↑i - 1)) = fun n ↦ ↑(s n) * 10 ^ (-↑n)hx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)⊢ x = ↑d
  .h.e'_3x:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun x ↦ ↑(s 0) + ∑ i ∈ Finset.range x, ↑↑(d.fracPart i) * 10 ^ (-↑i - 1)) Filter.atTop
  (nhds (↑(s 0) + ∑' (i : ℕ), ↑↑(d.fracPart i) * 10 ^ (-↑i - 1)))⊢ (fun x ↦ ↑(s 0) + ∑ i ∈ Finset.range x, ↑↑(d.fracPart i) * 10 ^ (-↑i - 1)) = fun n ↦ ↑(s n) * 10 ^ (-↑n) ext nh.e'_3.h.ax:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun x ↦ ↑(s 0) + ∑ i ∈ Finset.range x, ↑↑(d.fracPart i) * 10 ^ (-↑i - 1)) Filter.atTop
  (nhds (↑(s 0) + ∑' (i : ℕ), ↑↑(d.fracPart i) * 10 ^ (-↑i - 1)))n:ℕ⊢ ↑(↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(d.fracPart i) * 10 ^ (-↑i - 1)) = ↑(↑(s n) * 10 ^ (-↑n)); rw [hsum n]All goals completed! 🐙
  apply tendsto_nhds_unique _ thisx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)⊢ Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds x)
  apply Filter.Tendsto.squeeze (g := fun n:ℕ ↦ x - (10:NNReal)^(-n:ℝ)) (h := fun _ ↦ x)hgx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)⊢ Filter.Tendsto (fun n ↦ x - 10 ^ (-↑n)) Filter.atTop (nhds x)hhx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)⊢ Filter.Tendsto (fun x_1 ↦ x) Filter.atTop (nhds x)hgfx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)⊢ (fun n ↦ x - 10 ^ (-↑n)) ≤ fun n ↦ ↑(s n) * 10 ^ (-↑n)hfhx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)⊢ (fun n ↦ ↑(s n) * 10 ^ (-↑n)) ≤ fun x_1 ↦ x
  .hgx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)⊢ Filter.Tendsto (fun n ↦ x - 10 ^ (-↑n)) Filter.atTop (nhds x) convert Filter.Tendsto.const_sub (c := 0) x _h.e'_1.h.e'_3x:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)⊢ x = x - 0hg.convert_4x:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)⊢ Filter.Tendsto (fun n ↦ 10 ^ (-↑n)) Filter.atTop (nhds 0)
    .h.e'_1.h.e'_3x:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)⊢ x = x - 0 simpAll goals completed! 🐙
    convert tendsto_pow_atTop_nhds_zero_of_lt_one (?_:(1/10:NNReal) < 1) with nh.e'_3.hx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)n:ℕ⊢ 10 ^ (-↑n) = (1 / 10) ^ nhg.convert_4x:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)⊢ 1 / 10 < 1
    .h.e'_3.hx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)n:ℕ⊢ 10 ^ (-↑n) = (1 / 10) ^ n rw [←rpow_natCast, one_div, inv_rpow, rpow_neg]All goals completed! 🐙
    apply div_lt_one_of_lthg.convert_4.hx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)⊢ 1 < 10; boundAll goals completed! 🐙
  .hhx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)⊢ Filter.Tendsto (fun x_1 ↦ x) Filter.atTop (nhds x) exact tendsto_const_nhdsAll goals completed! 🐙
  .hgfx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)⊢ (fun n ↦ x - 10 ^ (-↑n)) ≤ fun n ↦ ↑(s n) * 10 ^ (-↑n) intro nhgfx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)n:ℕ⊢ (fun n ↦ x - 10 ^ (-↑n)) n ≤ (fun n ↦ ↑(s n) * 10 ^ (-↑n)) n; simphgfx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)n:ℕ⊢ x ≤ ↑(s n) * 10 ^ (-↑n) + 10 ^ (-↑n); calc
    _ = (x * 10^n) * (10:NNReal)^(-n:ℝ) := byx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)n:ℕ⊢ x = x * 10 ^ n * 10 ^ (-↑n)
      rw [mul_assoc, ←rpow_natCast, ←rpow_add]x:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)n:ℕ⊢ x = x * 10 ^ (↑n + -↑n)hxx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)n:ℕ⊢ 10 ≠ 0; simphxx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)n:ℕ⊢ 10 ≠ 0; norm_numAll goals completed! 🐙
    _ ≤ ((s n:NNReal) + 1)*(10:NNReal)^(-n:ℝ) := byx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)n:ℕ⊢ x * 10 ^ n * 10 ^ (-↑n) ≤ (↑(s n) + 1) * 10 ^ (-↑n) gcongrbcx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)n:ℕ⊢ x * 10 ^ n ≤ ↑(s n) + 1; grind [le_of_lt]All goals completed! 🐙
    _ = _ := byx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)n:ℕ⊢ (↑(s n) + 1) * 10 ^ (-↑n) = ↑(s n) * 10 ^ (-↑n) + 10 ^ (-↑n) ringAll goals completed! 🐙
  intro nhfhx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)n:ℕ⊢ (fun n ↦ ↑(s n) * 10 ^ (-↑n)) n ≤ (fun x_1 ↦ x) n; simphfhx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)n:ℕ⊢ ↑(s n) * 10 ^ (-↑n) ≤ x; calc
    _ ≤ (x * 10^n) * (10:NNReal)^(-n:ℝ) := byx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)n:ℕ⊢ ↑(s n) * 10 ^ (-↑n) ≤ x * 10 ^ n * 10 ^ (-↑n) gcongrbcx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)n:ℕ⊢ ↑(s n) ≤ x * 10 ^ n; grindAll goals completed! 🐙
    _ = x := byx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)n:ℕ⊢ x * 10 ^ n * 10 ^ (-↑n) = x rw [mul_assoc, ←rpow_natCast, ←rpow_add]x:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)n:ℕ⊢ x * 10 ^ (↑n + -↑n) = xhxx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)n:ℕ⊢ 10 ≠ 0; simphxx:ℝ≥0h:¬x = 0s:ℕ → ℕ := fun n ↦ ⌊x * 10 ^ n⌋₊hs:∀ (n : ℕ), ↑(s n) ≤ x * 10 ^ nhs':∀ (n : ℕ), x * 10 ^ n < ↑(s n) + 1a:ℕ → Digitha:∀ (n : ℕ), s (n + 1) = 10 * s n + ↑(a n)d:NNRealDecimal := { intPart := s 0, fracPart := a }hsum:∀ (n : ℕ), ↑(s n) * 10 ^ (-↑n) = ↑(s 0) + ∑ i ∈ Finset.range n, ↑↑(a i) * 10 ^ (-↑i - 1)this:Filter.Tendsto (fun n ↦ ↑(s n) * 10 ^ (-↑n)) Filter.atTop (nhds ↑d)n:ℕ⊢ 10 ≠ 0; norm_numAll goals completed! 🐙

Proposition B.2.2

theorem NNRealDecimal.not_inj : (1:NNReal) = (mk 1 fun _ ↦ 0) ∧ (1:NNReal) = (mk 0 fun _ ↦ 9) := by⊢ 1 = ↑{ intPart := 1, fracPart := fun x ↦ 0 } ∧ 1 = ↑{ intPart := 0, fracPart := fun x ↦ 9 }
  -- This proof is written to follow the structure of the original text.
  simp [toNNReal]⊢ 1 = ∑' (i : ℕ), ↑↑9 * 10 ^ (-↑i - 1)
  have := (mk 0 fun _ ↦ 9).toNNReal_conv.tendsto_sum_tsum_natthis:Filter.Tendsto (fun n ↦ ∑ i ∈ Finset.range n, ↑↑({ intPart := 0, fracPart := fun x ↦ 9 }.fracPart i) * 10 ^ (-↑i - 1))
  Filter.atTop (nhds (∑' (i : ℕ), ↑↑({ intPart := 0, fracPart := fun x ↦ 9 }.fracPart i) * 10 ^ (-↑i - 1)))⊢ 1 = ∑' (i : ℕ), ↑↑9 * 10 ^ (-↑i - 1)
  simp at thisthis:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))⊢ 1 = ∑' (i : ℕ), ↑↑9 * 10 ^ (-↑i - 1)
  apply tendsto_nhds_unique _ thisthis:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))⊢ Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop (nhds 1)
  convert_to Filter.atTop.Tendsto (fun n:ℕ ↦ 1 - (10:NNReal)^(-n:ℝ)) (nhds 1) using 2 with nh.e'_3.hthis:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕ⊢ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)this:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))⊢ Filter.Tendsto (fun n ↦ 1 - 10 ^ (-↑n)) Filter.atTop (nhds 1)
  .h.e'_3.hthis:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕ⊢ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n) induction' n with n hnh.e'_3.h.zerothis:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))⊢ ∑ x ∈ Finset.range 0, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑0)h.e'_3.h.succthis:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)⊢ ∑ x ∈ Finset.range (n + 1), ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑(n + 1))
    .h.e'_3.h.zerothis:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))⊢ ∑ x ∈ Finset.range 0, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑0) simpAll goals completed! 🐙
    rw [Finset.sum_range_succ, hn, Nat.cast_add, Nat.cast_one, neg_add']h.e'_3.h.succthis:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)⊢ 1 - 10 ^ (-↑n) + ↑↑9 * 10 ^ (-↑n - 1) = 1 - 10 ^ (-↑n - 1)
    have : (10:NNReal)^(-n:ℝ) = 10^(-n-1:ℝ) * 10 := by⊢ 1 = ↑{ intPart := 1, fracPart := fun x ↦ 0 } ∧ 1 = ↑{ intPart := 0, fracPart := fun x ↦ 9 }
      rw [←rpow_add_one]this:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)⊢ 10 ^ (-↑n) = 10 ^ (-↑n - 1 + 1)hxthis:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)⊢ 10 ≠ 0; simphxthis:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)⊢ 10 ≠ 0; norm_numAll goals completed! 🐙
    simp [this, ←coe_inj]h.e'_3.h.succthis✝:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)this:10 ^ (-↑n) = 10 ^ (-↑n - 1) * 10⊢ ↑(1 - 10 ^ (-↑n - 1) * 10) + ↑↑9 * 10 ^ (-↑n - 1) = ↑(1 - 10 ^ (-↑n - 1))
    rw [NNReal.coe_sub, NNReal.coe_sub]h.e'_3.h.succthis✝:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)this:10 ^ (-↑n) = 10 ^ (-↑n - 1) * 10⊢ ↑1 - ↑(10 ^ (-↑n - 1) * 10) + ↑↑9 * 10 ^ (-↑n - 1) = ↑1 - ↑(10 ^ (-↑n - 1))h.e'_3.h.succthis✝:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)this:10 ^ (-↑n) = 10 ^ (-↑n - 1) * 10⊢ 10 ^ (-↑n - 1) ≤ 1h.e'_3.h.succthis✝:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)this:10 ^ (-↑n) = 10 ^ (-↑n - 1) * 10⊢ 10 ^ (-↑n - 1) * 10 ≤ 1
    .h.e'_3.h.succthis✝:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)this:10 ^ (-↑n) = 10 ^ (-↑n - 1) * 10⊢ ↑1 - ↑(10 ^ (-↑n - 1) * 10) + ↑↑9 * 10 ^ (-↑n - 1) = ↑1 - ↑(10 ^ (-↑n - 1)) suffices h : ∀ c a : ℝ, c = 9 → 1 - a * 10 + c * a = 1 - a bythis✝:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)this:10 ^ (-↑n) = 10 ^ (-↑n - 1) * 10h:∀ (c a : ℝ), c = 9 → 1 - a * 10 + c * a = 1 - a⊢ ↑1 - ↑(10 ^ (-↑n - 1) * 10) + ↑↑9 * 10 ^ (-↑n - 1) = ↑1 - ↑(10 ^ (-↑n - 1)) apply hathis✝:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)this:10 ^ (-↑n) = 10 ^ (-↑n - 1) * 10h:∀ (c a : ℝ), c = 9 → 1 - a * 10 + c * a = 1 - a⊢ ↑↑9 = 9; norm_castAll goals completed! 🐙
      grindAll goals completed! 🐙
    .h.e'_3.h.succthis✝:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)this:10 ^ (-↑n) = 10 ^ (-↑n - 1) * 10⊢ 10 ^ (-↑n - 1) ≤ 1 apply rpow_le_one_of_one_le_of_nonposh.e'_3.h.succ.hxthis✝:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)this:10 ^ (-↑n) = 10 ^ (-↑n - 1) * 10⊢ 1 ≤ 10h.e'_3.h.succ.hzthis✝:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)this:10 ^ (-↑n) = 10 ^ (-↑n - 1) * 10⊢ -↑n - 1 ≤ 0; norm_numh.e'_3.h.succ.hzthis✝:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)this:10 ^ (-↑n) = 10 ^ (-↑n - 1) * 10⊢ -↑n - 1 ≤ 0; linarithAll goals completed! 🐙
    rw [←rpow_add_one]h.e'_3.h.succthis✝:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)this:10 ^ (-↑n) = 10 ^ (-↑n - 1) * 10⊢ 10 ^ (-↑n - 1 + 1) ≤ 1h.e'_3.h.succ.hxthis✝:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)this:10 ^ (-↑n) = 10 ^ (-↑n - 1) * 10⊢ 10 ≠ 0
    apply rpow_le_one_of_one_le_of_nonposh.e'_3.h.succ.hxthis✝:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)this:10 ^ (-↑n) = 10 ^ (-↑n - 1) * 10⊢ 1 ≤ 10h.e'_3.h.succ.hzthis✝:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)this:10 ^ (-↑n) = 10 ^ (-↑n - 1) * 10⊢ -↑n - 1 + 1 ≤ 0h.e'_3.h.succ.hxthis✝:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)this:10 ^ (-↑n) = 10 ^ (-↑n - 1) * 10⊢ 10 ≠ 0; norm_numh.e'_3.h.succ.hzthis✝:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)this:10 ^ (-↑n) = 10 ^ (-↑n - 1) * 10⊢ -↑n - 1 + 1 ≤ 0h.e'_3.h.succ.hxthis✝:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)this:10 ^ (-↑n) = 10 ^ (-↑n - 1) * 10⊢ 10 ≠ 0; linarithh.e'_3.h.succ.hxthis✝:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))n:ℕhn:∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1) = 1 - 10 ^ (-↑n)this:10 ^ (-↑n) = 10 ^ (-↑n - 1) * 10⊢ 10 ≠ 0; norm_numAll goals completed! 🐙
  convert Filter.Tendsto.const_sub (f := fun n:ℕ ↦ (10:NNReal)^(-n:ℝ)) (c := 0) 1 _h.e'_5.h.e'_3this:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))⊢ 1 = 1 - 0convert_2this:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))⊢ Filter.Tendsto (fun n ↦ 10 ^ (-↑n)) Filter.atTop (nhds 0); simpconvert_2this:Filter.Tendsto (fun n ↦ ∑ x ∈ Finset.range n, ↑↑9 * 10 ^ (-↑x - 1)) Filter.atTop
  (nhds (∑' (x : ℕ), ↑↑9 * 10 ^ (-↑x - 1)))⊢ Filter.Tendsto (fun n ↦ 10 ^ (-↑n)) Filter.atTop (nhds 0)
  convert tendsto_pow_atTop_nhds_zero_of_lt_one (show (1/10:NNReal) < 1 by⊢ 1 = ↑{ intPart := 1, fracPart := fun x ↦ 0 } ∧ 1 = ↑{ intPart := 0, fracPart := fun x ↦ 9 } boundAll goals completed! 🐙) with n
  rw [←rpow_natCast, one_div, inv_rpow, rpow_neg]All goals completed! 🐙

              inductive RealDecimal where
  | pos : NNRealDecimal → RealDecimal
  | neg : NNRealDecimal → RealDecimalnoncomputable instance RealDecimal.instCoeReal : Coe RealDecimal ℝ where
  coe := fun d ↦ match d with
    | RealDecimal.pos d => d.toNNReal
    | RealDecimal.neg d => -(d.toNNReal:ℝ)theorem RealDecimal.surj (x:ℝ) : ∃ d:RealDecimal, x = d := byx:ℝ⊢ ∃ d,
  x =
    match d with
    | pos d => ↑↑d
    | neg d => -↑↑d
  obtain h | h := le_or_gt 0 xinlx:ℝh:0 ≤ x⊢ ∃ d,
  x =
    match d with
    | pos d => ↑↑d
    | neg d => -↑↑dinrx:ℝh:x < 0⊢ ∃ d,
  x =
    match d with
    | pos d => ↑↑d
    | neg d => -↑↑d
  .inlx:ℝh:0 ≤ x⊢ ∃ d,
  x =
    match d with
    | pos d => ↑↑d
    | neg d => -↑↑d choose d hd using NNRealDecimal.surj (x.toNNReal)inlx:ℝh:0 ≤ xd:NNRealDecimalhd:x.toNNReal = ↑d⊢ ∃ d,
  x =
    match d with
    | pos d => ↑↑d
    | neg d => -↑↑d; use pos dhx:ℝh:0 ≤ xd:NNRealDecimalhd:x.toNNReal = ↑d⊢ x =
  match pos d with
  | pos d => ↑↑d
  | neg d => -↑↑d; simp [←hd, h]All goals completed! 🐙
  .inrx:ℝh:x < 0⊢ ∃ d,
  x =
    match d with
    | pos d => ↑↑d
    | neg d => -↑↑d choose d hd using NNRealDecimal.surj ((-x).toNNReal)inrx:ℝh:x < 0d:NNRealDecimalhd:(-x).toNNReal = ↑d⊢ ∃ d,
  x =
    match d with
    | pos d => ↑↑d
    | neg d => -↑↑d; use neg dhx:ℝh:x < 0d:NNRealDecimalhd:(-x).toNNReal = ↑d⊢ x =
  match neg d with
  | pos d => ↑↑d
  | neg d => -↑↑d; simp [←hd, show 0 ≤ -x by linarith]All goals completed! 🐙

Exercise B.2.2

theorem declaration uses `sorry`RealDecimal.not_inj_one (d: RealDecimal) : (d:ℝ) = 1 ↔ (d = pos (mk 1 fun _ ↦ 0) ∨ d = pos (mk 0 fun _ ↦ 9)) := byd:RealDecimal⊢ (match d with
    | pos d => ↑↑d
    | neg d => -↑↑d) =
    1 ↔
  d = pos { intPart := 1, fracPart := fun x ↦ 0 } ∨ d = pos { intPart := 0, fracPart := fun x ↦ 9 }
  sorryAll goals completed! 🐙

Exercise B.2.3

abbrev TerminatingDecimal (x:ℝ) : Prop := ∃ (n:ℤ) (m:ℕ), x = n / (10:ℝ)^m

              theorem declaration uses `sorry`RealDecimal.not_inj_terminating {x:ℝ} (hx: TerminatingDecimal x) : ∃ d₁ d₂:RealDecimal, d₁ ≠ d₂ ∧ ∀ d: RealDecimal, d = x ↔ d = d₁ ∨ d = d₂ := byx:ℝhx:TerminatingDecimal x⊢ ∃ d₁ d₂,
  d₁ ≠ d₂ ∧
    ∀ (d : RealDecimal),
      (match d with
          | pos d => ↑↑d
          | neg d => -↑↑d) =
          x ↔
        d = d₁ ∨ d = d₂ sorryAll goals completed! 🐙theorem declaration uses `sorry`RealDecimal.inj_nonterminating {x:ℝ} (hx: ¬TerminatingDecimal x) : ∃! d:RealDecimal, d = x := byx:ℝhx:¬TerminatingDecimal x⊢ ∃! d,
  (match d with
    | pos d => ↑↑d
    | neg d => -↑↑d) =
    x sorryAll goals completed! 🐙/-- Exercise B.2.4.  This is Corollary 8.3.4, but the intent is to rewrite the proof using the decimal system. -/
declaration uses `sorry`example : Uncountable ℝ := by⊢ Uncountable ℝ sorryAll goals completed! 🐙end AppendixB