Analysis I, Appendix B.1: The decimal representation of natural numbers

Am implementation of the decimal representation of Mathlib's natural numbers ℕ : Typeℕ.

This is separate from the way decimal numerals are already represenated in Mathlib via the OfNat.{u} (α : Type u) : ℕ → Type uOfNat typeclass.

namespace AppendixB

/- The ten digits, together with the base 10 -/
example : 0 = Nat.zero := rfl

example : 1 = (0:Nat).succ := rflexample : 2 = (1:Nat).succ := rflexample : 3 = (2:Nat).succ := rflexample : 4 = (3:Nat).succ := rflexample : 5 = (4:Nat).succ := rflexample : 6 = (5:Nat).succ := rflexample : 7 = (6:Nat).succ := rflexample : 8 = (7:Nat).succ := rflexample : 9 = (8:Nat).succ := rflexample : 10 = (9:Nat).succ := rfl

Definition B.1.1

def Digit := Fin 10

instance Digit.instZero : Zero Digit := ⟨0, by⊢ 0 < 10 decideAll goals completed! 🐙⟩instance Digit.instOne : One Digit := ⟨1, by⊢ 1 < 10 decideAll goals completed! 🐙⟩instance Digit.instTwo : OfNat Digit 2 := ⟨2, by⊢ 2 < 10 decideAll goals completed! 🐙⟩instance Digit.instThree : OfNat Digit 3 := ⟨3, by⊢ 3 < 10 decideAll goals completed! 🐙⟩instance Digit.instFour : OfNat Digit 4 := ⟨4, by⊢ 4 < 10 decideAll goals completed! 🐙⟩instance Digit.instFive : OfNat Digit 5 := ⟨5, by⊢ 5 < 10 decideAll goals completed! 🐙⟩instance Digit.instSix : OfNat Digit 6 := ⟨6, by⊢ 6 < 10 decideAll goals completed! 🐙⟩instance Digit.instSeven : OfNat Digit 7 := ⟨7, by⊢ 7 < 10 decideAll goals completed! 🐙⟩instance Digit.instEight : OfNat Digit 8 := ⟨8, by⊢ 8 < 10 decideAll goals completed! 🐙⟩instance Digit.instNine : OfNat Digit 9 := ⟨9, by⊢ 9 < 10 decideAll goals completed! 🐙⟩instance Digit.instFintype : Fintype Digit := Fin.fintype 10instance Digit.instDecidableEq : DecidableEq Digit := instDecidableEqFin 10instance Digit.instInhabited : Inhabited Digit := ⟨ 0 ⟩

@[coe]
abbrev Digit.toNat (d:Digit) : ℕ := d.val

instance Digit.instCoeNat : Coe Digit Nat where
  coe := toNat

theorem Digit.lt (d:Digit) : (d:ℕ) < 10 := d.isLtabbrev Digit.mk {n:ℕ} (h: n < 10) : Digit := ⟨n, h⟩

@[simp]
theorem Digit.toNat_mk {n:ℕ} (h: n < 10) : (Digit.mk h:ℕ) = n := rfl

@[simp]
theorem Digit.inj (d d':Digit) : d = d' ↔ (d:ℕ) = d' := byd:Digitd':Digit⊢ d = d' ↔ ↑d = ↑d' grindAll goals completed! 🐙

theorem Digit.mk_eq_iff (d:Digit) {n:ℕ} (h: n < 10) : d = mk h ↔ (d:ℕ) = n := byd:Digitn:ℕh:n < 10⊢ d = mk h ↔ ↑d = n
  convert Digit.inj d (mk h)All goals completed! 🐙

0 : Digit

1 : Digit

2 : Digit

3 : Digit

4 : Digit

5 : Digit

6 : Digit

7 : Digit

8 : Digit

9 : Digit

theorem Digit.eq (n: Digit) : n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 3 ∨ n = 4 ∨ n = 5 ∨ n = 6 ∨ n = 7 ∨ n = 8 ∨ n = 9 := byn:Digit⊢ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 3 ∨ n = 4 ∨ n = 5 ∨ n = 6 ∨ n = 7 ∨ n = 8 ∨ n = 9
  fin_cases n«0»⊢ (fun i => i) ⟨0, ⋯⟩ = 0 ∨
  (fun i => i) ⟨0, ⋯⟩ = 1 ∨
    (fun i => i) ⟨0, ⋯⟩ = 2 ∨
      (fun i => i) ⟨0, ⋯⟩ = 3 ∨
        (fun i => i) ⟨0, ⋯⟩ = 4 ∨
          (fun i => i) ⟨0, ⋯⟩ = 5 ∨
            (fun i => i) ⟨0, ⋯⟩ = 6 ∨ (fun i => i) ⟨0, ⋯⟩ = 7 ∨ (fun i => i) ⟨0, ⋯⟩ = 8 ∨ (fun i => i) ⟨0, ⋯⟩ = 9«1»⊢ (fun i => i) ⟨1, ⋯⟩ = 0 ∨
  (fun i => i) ⟨1, ⋯⟩ = 1 ∨
    (fun i => i) ⟨1, ⋯⟩ = 2 ∨
      (fun i => i) ⟨1, ⋯⟩ = 3 ∨
        (fun i => i) ⟨1, ⋯⟩ = 4 ∨
          (fun i => i) ⟨1, ⋯⟩ = 5 ∨
            (fun i => i) ⟨1, ⋯⟩ = 6 ∨ (fun i => i) ⟨1, ⋯⟩ = 7 ∨ (fun i => i) ⟨1, ⋯⟩ = 8 ∨ (fun i => i) ⟨1, ⋯⟩ = 9«2»⊢ (fun i => i) ⟨2, ⋯⟩ = 0 ∨
  (fun i => i) ⟨2, ⋯⟩ = 1 ∨
    (fun i => i) ⟨2, ⋯⟩ = 2 ∨
      (fun i => i) ⟨2, ⋯⟩ = 3 ∨
        (fun i => i) ⟨2, ⋯⟩ = 4 ∨
          (fun i => i) ⟨2, ⋯⟩ = 5 ∨
            (fun i => i) ⟨2, ⋯⟩ = 6 ∨ (fun i => i) ⟨2, ⋯⟩ = 7 ∨ (fun i => i) ⟨2, ⋯⟩ = 8 ∨ (fun i => i) ⟨2, ⋯⟩ = 9«3»⊢ (fun i => i) ⟨3, ⋯⟩ = 0 ∨
  (fun i => i) ⟨3, ⋯⟩ = 1 ∨
    (fun i => i) ⟨3, ⋯⟩ = 2 ∨
      (fun i => i) ⟨3, ⋯⟩ = 3 ∨
        (fun i => i) ⟨3, ⋯⟩ = 4 ∨
          (fun i => i) ⟨3, ⋯⟩ = 5 ∨
            (fun i => i) ⟨3, ⋯⟩ = 6 ∨ (fun i => i) ⟨3, ⋯⟩ = 7 ∨ (fun i => i) ⟨3, ⋯⟩ = 8 ∨ (fun i => i) ⟨3, ⋯⟩ = 9«4»⊢ (fun i => i) ⟨4, ⋯⟩ = 0 ∨
  (fun i => i) ⟨4, ⋯⟩ = 1 ∨
    (fun i => i) ⟨4, ⋯⟩ = 2 ∨
      (fun i => i) ⟨4, ⋯⟩ = 3 ∨
        (fun i => i) ⟨4, ⋯⟩ = 4 ∨
          (fun i => i) ⟨4, ⋯⟩ = 5 ∨
            (fun i => i) ⟨4, ⋯⟩ = 6 ∨ (fun i => i) ⟨4, ⋯⟩ = 7 ∨ (fun i => i) ⟨4, ⋯⟩ = 8 ∨ (fun i => i) ⟨4, ⋯⟩ = 9«5»⊢ (fun i => i) ⟨5, ⋯⟩ = 0 ∨
  (fun i => i) ⟨5, ⋯⟩ = 1 ∨
    (fun i => i) ⟨5, ⋯⟩ = 2 ∨
      (fun i => i) ⟨5, ⋯⟩ = 3 ∨
        (fun i => i) ⟨5, ⋯⟩ = 4 ∨
          (fun i => i) ⟨5, ⋯⟩ = 5 ∨
            (fun i => i) ⟨5, ⋯⟩ = 6 ∨ (fun i => i) ⟨5, ⋯⟩ = 7 ∨ (fun i => i) ⟨5, ⋯⟩ = 8 ∨ (fun i => i) ⟨5, ⋯⟩ = 9«6»⊢ (fun i => i) ⟨6, ⋯⟩ = 0 ∨
  (fun i => i) ⟨6, ⋯⟩ = 1 ∨
    (fun i => i) ⟨6, ⋯⟩ = 2 ∨
      (fun i => i) ⟨6, ⋯⟩ = 3 ∨
        (fun i => i) ⟨6, ⋯⟩ = 4 ∨
          (fun i => i) ⟨6, ⋯⟩ = 5 ∨
            (fun i => i) ⟨6, ⋯⟩ = 6 ∨ (fun i => i) ⟨6, ⋯⟩ = 7 ∨ (fun i => i) ⟨6, ⋯⟩ = 8 ∨ (fun i => i) ⟨6, ⋯⟩ = 9«7»⊢ (fun i => i) ⟨7, ⋯⟩ = 0 ∨
  (fun i => i) ⟨7, ⋯⟩ = 1 ∨
    (fun i => i) ⟨7, ⋯⟩ = 2 ∨
      (fun i => i) ⟨7, ⋯⟩ = 3 ∨
        (fun i => i) ⟨7, ⋯⟩ = 4 ∨
          (fun i => i) ⟨7, ⋯⟩ = 5 ∨
            (fun i => i) ⟨7, ⋯⟩ = 6 ∨ (fun i => i) ⟨7, ⋯⟩ = 7 ∨ (fun i => i) ⟨7, ⋯⟩ = 8 ∨ (fun i => i) ⟨7, ⋯⟩ = 9«8»⊢ (fun i => i) ⟨8, ⋯⟩ = 0 ∨
  (fun i => i) ⟨8, ⋯⟩ = 1 ∨
    (fun i => i) ⟨8, ⋯⟩ = 2 ∨
      (fun i => i) ⟨8, ⋯⟩ = 3 ∨
        (fun i => i) ⟨8, ⋯⟩ = 4 ∨
          (fun i => i) ⟨8, ⋯⟩ = 5 ∨
            (fun i => i) ⟨8, ⋯⟩ = 6 ∨ (fun i => i) ⟨8, ⋯⟩ = 7 ∨ (fun i => i) ⟨8, ⋯⟩ = 8 ∨ (fun i => i) ⟨8, ⋯⟩ = 9«9»⊢ (fun i => i) ⟨9, ⋯⟩ = 0 ∨
  (fun i => i) ⟨9, ⋯⟩ = 1 ∨
    (fun i => i) ⟨9, ⋯⟩ = 2 ∨
      (fun i => i) ⟨9, ⋯⟩ = 3 ∨
        (fun i => i) ⟨9, ⋯⟩ = 4 ∨
          (fun i => i) ⟨9, ⋯⟩ = 5 ∨
            (fun i => i) ⟨9, ⋯⟩ = 6 ∨ (fun i => i) ⟨9, ⋯⟩ = 7 ∨ (fun i => i) ⟨9, ⋯⟩ = 8 ∨ (fun i => i) ⟨9, ⋯⟩ = 9 <;>«0»⊢ (fun i => i) ⟨0, ⋯⟩ = 0 ∨
  (fun i => i) ⟨0, ⋯⟩ = 1 ∨
    (fun i => i) ⟨0, ⋯⟩ = 2 ∨
      (fun i => i) ⟨0, ⋯⟩ = 3 ∨
        (fun i => i) ⟨0, ⋯⟩ = 4 ∨
          (fun i => i) ⟨0, ⋯⟩ = 5 ∨
            (fun i => i) ⟨0, ⋯⟩ = 6 ∨ (fun i => i) ⟨0, ⋯⟩ = 7 ∨ (fun i => i) ⟨0, ⋯⟩ = 8 ∨ (fun i => i) ⟨0, ⋯⟩ = 9«1»⊢ (fun i => i) ⟨1, ⋯⟩ = 0 ∨
  (fun i => i) ⟨1, ⋯⟩ = 1 ∨
    (fun i => i) ⟨1, ⋯⟩ = 2 ∨
      (fun i => i) ⟨1, ⋯⟩ = 3 ∨
        (fun i => i) ⟨1, ⋯⟩ = 4 ∨
          (fun i => i) ⟨1, ⋯⟩ = 5 ∨
            (fun i => i) ⟨1, ⋯⟩ = 6 ∨ (fun i => i) ⟨1, ⋯⟩ = 7 ∨ (fun i => i) ⟨1, ⋯⟩ = 8 ∨ (fun i => i) ⟨1, ⋯⟩ = 9«2»⊢ (fun i => i) ⟨2, ⋯⟩ = 0 ∨
  (fun i => i) ⟨2, ⋯⟩ = 1 ∨
    (fun i => i) ⟨2, ⋯⟩ = 2 ∨
      (fun i => i) ⟨2, ⋯⟩ = 3 ∨
        (fun i => i) ⟨2, ⋯⟩ = 4 ∨
          (fun i => i) ⟨2, ⋯⟩ = 5 ∨
            (fun i => i) ⟨2, ⋯⟩ = 6 ∨ (fun i => i) ⟨2, ⋯⟩ = 7 ∨ (fun i => i) ⟨2, ⋯⟩ = 8 ∨ (fun i => i) ⟨2, ⋯⟩ = 9«3»⊢ (fun i => i) ⟨3, ⋯⟩ = 0 ∨
  (fun i => i) ⟨3, ⋯⟩ = 1 ∨
    (fun i => i) ⟨3, ⋯⟩ = 2 ∨
      (fun i => i) ⟨3, ⋯⟩ = 3 ∨
        (fun i => i) ⟨3, ⋯⟩ = 4 ∨
          (fun i => i) ⟨3, ⋯⟩ = 5 ∨
            (fun i => i) ⟨3, ⋯⟩ = 6 ∨ (fun i => i) ⟨3, ⋯⟩ = 7 ∨ (fun i => i) ⟨3, ⋯⟩ = 8 ∨ (fun i => i) ⟨3, ⋯⟩ = 9«4»⊢ (fun i => i) ⟨4, ⋯⟩ = 0 ∨
  (fun i => i) ⟨4, ⋯⟩ = 1 ∨
    (fun i => i) ⟨4, ⋯⟩ = 2 ∨
      (fun i => i) ⟨4, ⋯⟩ = 3 ∨
        (fun i => i) ⟨4, ⋯⟩ = 4 ∨
          (fun i => i) ⟨4, ⋯⟩ = 5 ∨
            (fun i => i) ⟨4, ⋯⟩ = 6 ∨ (fun i => i) ⟨4, ⋯⟩ = 7 ∨ (fun i => i) ⟨4, ⋯⟩ = 8 ∨ (fun i => i) ⟨4, ⋯⟩ = 9«5»⊢ (fun i => i) ⟨5, ⋯⟩ = 0 ∨
  (fun i => i) ⟨5, ⋯⟩ = 1 ∨
    (fun i => i) ⟨5, ⋯⟩ = 2 ∨
      (fun i => i) ⟨5, ⋯⟩ = 3 ∨
        (fun i => i) ⟨5, ⋯⟩ = 4 ∨
          (fun i => i) ⟨5, ⋯⟩ = 5 ∨
            (fun i => i) ⟨5, ⋯⟩ = 6 ∨ (fun i => i) ⟨5, ⋯⟩ = 7 ∨ (fun i => i) ⟨5, ⋯⟩ = 8 ∨ (fun i => i) ⟨5, ⋯⟩ = 9«6»⊢ (fun i => i) ⟨6, ⋯⟩ = 0 ∨
  (fun i => i) ⟨6, ⋯⟩ = 1 ∨
    (fun i => i) ⟨6, ⋯⟩ = 2 ∨
      (fun i => i) ⟨6, ⋯⟩ = 3 ∨
        (fun i => i) ⟨6, ⋯⟩ = 4 ∨
          (fun i => i) ⟨6, ⋯⟩ = 5 ∨
            (fun i => i) ⟨6, ⋯⟩ = 6 ∨ (fun i => i) ⟨6, ⋯⟩ = 7 ∨ (fun i => i) ⟨6, ⋯⟩ = 8 ∨ (fun i => i) ⟨6, ⋯⟩ = 9«7»⊢ (fun i => i) ⟨7, ⋯⟩ = 0 ∨
  (fun i => i) ⟨7, ⋯⟩ = 1 ∨
    (fun i => i) ⟨7, ⋯⟩ = 2 ∨
      (fun i => i) ⟨7, ⋯⟩ = 3 ∨
        (fun i => i) ⟨7, ⋯⟩ = 4 ∨
          (fun i => i) ⟨7, ⋯⟩ = 5 ∨
            (fun i => i) ⟨7, ⋯⟩ = 6 ∨ (fun i => i) ⟨7, ⋯⟩ = 7 ∨ (fun i => i) ⟨7, ⋯⟩ = 8 ∨ (fun i => i) ⟨7, ⋯⟩ = 9«8»⊢ (fun i => i) ⟨8, ⋯⟩ = 0 ∨
  (fun i => i) ⟨8, ⋯⟩ = 1 ∨
    (fun i => i) ⟨8, ⋯⟩ = 2 ∨
      (fun i => i) ⟨8, ⋯⟩ = 3 ∨
        (fun i => i) ⟨8, ⋯⟩ = 4 ∨
          (fun i => i) ⟨8, ⋯⟩ = 5 ∨
            (fun i => i) ⟨8, ⋯⟩ = 6 ∨ (fun i => i) ⟨8, ⋯⟩ = 7 ∨ (fun i => i) ⟨8, ⋯⟩ = 8 ∨ (fun i => i) ⟨8, ⋯⟩ = 9«9»⊢ (fun i => i) ⟨9, ⋯⟩ = 0 ∨
  (fun i => i) ⟨9, ⋯⟩ = 1 ∨
    (fun i => i) ⟨9, ⋯⟩ = 2 ∨
      (fun i => i) ⟨9, ⋯⟩ = 3 ∨
        (fun i => i) ⟨9, ⋯⟩ = 4 ∨
          (fun i => i) ⟨9, ⋯⟩ = 5 ∨
            (fun i => i) ⟨9, ⋯⟩ = 6 ∨ (fun i => i) ⟨9, ⋯⟩ = 7 ∨ (fun i => i) ⟨9, ⋯⟩ = 8 ∨ (fun i => i) ⟨9, ⋯⟩ = 9 simp +decideAll goals completed! 🐙

Definition B.1.2

structure PosintDecimal where
  digits : List Digit
  nonempty : digits ≠ []
  nonzero : digits.head nonempty ≠ 0

theorem PosintDecimal.congr' {p q:PosintDecimal} (h: p.digits = q.digits) : p = q := byp:PosintDecimalq:PosintDecimalh:p.digits = q.digits⊢ p = q
  obtain ⟨ pd, _, _ ⟩ := pq:PosintDecimalpd:List Digitnonempty✝:pd ≠ []nonzero✝:pd.head nonempty✝ ≠ 0h:{ digits := pd, nonempty := nonempty✝, nonzero := nonzero✝ }.digits = q.digits⊢ { digits := pd, nonempty := nonempty✝, nonzero := nonzero✝ } = q
  obtain ⟨ qd, _, _ ⟩ := qpd:List Digitnonempty✝¹:pd ≠ []nonzero✝¹:pd.head nonempty✝ ≠ 0qd:List Digitnonempty✝:qd ≠ []nonzero✝:qd.head nonempty✝ ≠ 0h:{ digits := pd, nonempty := nonempty✝¹, nonzero := nonzero✝¹ }.digits =
  { digits := qd, nonempty := nonempty✝, nonzero := nonzero✝ }.digits⊢ { digits := pd, nonempty := nonempty✝¹, nonzero := nonzero✝¹ } =
  { digits := qd, nonempty := nonempty✝, nonzero := nonzero✝ }
  congrAll goals completed! 🐙

theorem PosintDecimal.congr {p q:PosintDecimal} (h: p.digits.length = q.digits.length)
  (h': ∀ (n:ℕ) (h₁ : n < p.digits.length) (h₂: n < q.digits.length), p.digits.get ⟨ n, h₁ ⟩ = q.digits.get ⟨ n, h₂ ⟩) : p = q := byp:PosintDecimalq:PosintDecimalh:p.digits.length = q.digits.lengthh':∀ (n : ℕ) (h₁ : n < p.digits.length) (h₂ : n < q.digits.length), p.digits.get ⟨n, h₁⟩ = q.digits.get ⟨n, h₂⟩⊢ p = q
  apply congr'hp:PosintDecimalq:PosintDecimalh:p.digits.length = q.digits.lengthh':∀ (n : ℕ) (h₁ : n < p.digits.length) (h₂ : n < q.digits.length), p.digits.get ⟨n, h₁⟩ = q.digits.get ⟨n, h₂⟩⊢ p.digits = q.digits
  simp_all [List.ext_get_iff]All goals completed! 🐙

abbrev PosintDecimal.head (p:PosintDecimal): Digit := p.digits.head p.nonemptytheorem PosintDecimal.head_ne_zero (p:PosintDecimal) : p.head ≠ 0 := p.nonzero

theorem PosintDecimal.head_ne_zero' (p:PosintDecimal) : (p.head:ℕ) ≠ 0 := byp:PosintDecimal⊢ ↑p.head ≠ 0
  by_contra!p:PosintDecimalthis:↑p.head = 0⊢ False
  apply head_ne_zero pp:PosintDecimalthis:↑p.head = 0⊢ p.head = 0
  simp_all [Digit.toNat, Digit.inj]p:PosintDecimalthis:p.head = 0⊢ 0 = ↑0; rflAll goals completed! 🐙

theorem PosintDecimal.length_pos (p:PosintDecimal) : 0 < p.digits.length := byp:PosintDecimal⊢ 0 < p.digits.length
  simp [List.length_pos_iff, p.nonempty]All goals completed! 🐙

A slightly clunky way of creating decimals.

def PosintDecimal.mk' (head:Digit) (tail:List Digit) (h: head ≠ 0) : PosintDecimal := {
  digits := head :: tail
  nonempty := byhead:Digittail:List Digith:head ≠ 0⊢ head :: tail ≠ [] aesopAll goals completed! 🐙
  nonzero := h
}

PosintDecimal.mk' 3 [1, 4] ⋯ : PosintDecimal

PosintDecimal.mk' 3 [] ⋯ : PosintDecimal

PosintDecimal.mk' 1 [0] ⋯ : PosintDecimal

We are indexing digits in a decimal from left to right rather than from right to left, thus necessitating a reversal here.

@[coe]
def PosintDecimal.toNat (p:PosintDecimal) : Nat :=
  ∑ i:Fin p.digits.length, p.digits[p.digits.length - 1 - ↑i].toNat * 10 ^ (i:ℕ)

instance PosintDecimal.instCoeNat : Coe PosintDecimal Nat where
  coe := toNat

example : (PosintDecimal.mk' 3 [1, 4] (by⊢ 3 ≠ 0 decideAll goals completed! 🐙):ℕ) = 314 := by⊢ ↑(PosintDecimal.mk' 3 [1, 4] ⋯) = 314 decideAll goals completed! 🐙

Remark B.1.3

@[simp]
theorem PosintDecimal.ten_eq_ten : (mk' 1 [0] (by⊢ 1 ≠ 0 decideAll goals completed! 🐙):ℕ) = 10 := by⊢ ↑(mk' 1 [0] ⋯) = 10
  decideAll goals completed! 🐙

theorem PosintDecimal.digit_eq {d:Digit} (h: d ≠ 0) : (mk' d [] h:ℕ) = d := byd:Digith:d ≠ 0⊢ ↑(mk' d [] h) = ↑d
  simp [toNat, mk']All goals completed! 🐙

theorem PosintDecimal.pos (p:PosintDecimal) : 0 < (p:ℕ) := byp:PosintDecimal⊢ 0 < ↑p
  simp [toNat]p:PosintDecimal⊢ 0 < ∑ i, ↑p.digits[p.digits.length - 1 - ↑i] * 10 ^ ↑i
  calc
    _ < (p.head:ℕ) * 10 ^ (p.digits.length - 1) := byp:PosintDecimal⊢ 0 < ↑p.head * 10 ^ (p.digits.length - 1)
      have := p.head_ne_zero'p:PosintDecimalthis:↑p.head ≠ 0 := head_ne_zero' p⊢ 0 < ↑p.head * 10 ^ (p.digits.length - 1)
      positivityAll goals completed! 🐙
    _ ≤ _ := byp:PosintDecimal⊢ ↑p.head * 10 ^ (p.digits.length - 1) ≤ ∑ i, ↑p.digits[p.digits.length - 1 - ↑i] * 10 ^ ↑i
      have := p.length_posp:PosintDecimalthis:0 < p.digits.length := length_pos p⊢ ↑p.head * 10 ^ (p.digits.length - 1) ≤ ∑ i, ↑p.digits[p.digits.length - 1 - ↑i] * 10 ^ ↑i
      set a : Fin p.digits.length := ⟨ p.digits.length - 1, byp:PosintDecimalthis:0 < p.digits.length := length_pos p⊢ p.digits.length - 1 < p.digits.length omegaAll goals completed! 🐙 ⟩
      convert Finset.single_le_sum _ (Finset.mem_univ a)h.e'_3p:PosintDecimalthis:0 < p.digits.length := length_pos pa:Fin p.digits.length := ⟨p.digits.length - 1, ⋯⟩⊢ ↑p.head * 10 ^ (p.digits.length - 1) = ↑p.digits[p.digits.length - 1 - ↑a] * 10 ^ ↑aconvert_5p:PosintDecimalthis:0 < p.digits.length := length_pos pa:Fin p.digits.length := ⟨p.digits.length - 1, ⋯⟩⊢ AddLeftMono ℕconvert_6p:PosintDecimalthis:0 < p.digits.length := length_pos pa:Fin p.digits.length := ⟨p.digits.length - 1, ⋯⟩⊢ ∀ i ∈ Finset.univ, 0 ≤ ↑p.digits[p.digits.length - 1 - ↑i] * 10 ^ ↑i
      .h.e'_3p:PosintDecimalthis:0 < p.digits.length := length_pos pa:Fin p.digits.length := ⟨p.digits.length - 1, ⋯⟩⊢ ↑p.head * 10 ^ (p.digits.length - 1) = ↑p.digits[p.digits.length - 1 - ↑a] * 10 ^ ↑a simp [a, head, List.head_eq_getElem]All goals completed! 🐙
      .convert_5p:PosintDecimalthis:0 < p.digits.length := length_pos pa:Fin p.digits.length := ⟨p.digits.length - 1, ⋯⟩⊢ AddLeftMono ℕ infer_instanceAll goals completed! 🐙
      grindAll goals completed! 🐙

An operation implicit in the proof of Theorem B.1.4:

abbrev PosintDecimal.append (p:PosintDecimal) (d:Digit) : PosintDecimal :=
  mk' p.head (p.digits.tail ++ [d]) p.head_ne_zero

Unknown identifier `toNat`toNat equals Horner (left-fold) evaluation of the digit list.

theorem PosintDecimal.toNat_eq_foldl (q : PosintDecimal) :
    q.toNat = q.digits.foldl (fun acc (d : Digit) => acc * 10 + d.toNat) 0 := byq:PosintDecimal⊢ ↑q = List.foldl (fun acc d => acc * 10 + ↑d) 0 q.digits
  suffices h : ∀ (L : List Digit) (acc : ℕ),
      L.foldl (fun a (d : Digit) => a * 10 + d.toNat) acc =
      acc * 10 ^ L.length + ∑ i : Fin L.length, (L[L.length - 1 - ↑i]).toNat * 10 ^ (↑i : ℕ)
    from byq:PosintDecimalh:∀ (L : List Digit) (acc : ℕ),
  List.foldl (fun a d => a * 10 + ↑d) acc L = acc * 10 ^ L.length + ∑ i, ↑L[L.length - 1 - ↑i] * 10 ^ ↑i := 
  ?m.94⊢ ↑q = List.foldl (fun acc d => acc * 10 + ↑d) 0 q.digits simp [toNat, h q.digits 0]All goals completed! 🐙
  intro Lq:PosintDecimalL:List Digit⊢ ∀ (acc : ℕ), List.foldl (fun a d => a * 10 + ↑d) acc L = acc * 10 ^ L.length + ∑ i, ↑L[L.length - 1 - ↑i] * 10 ^ ↑i; induction L with
  | nil =>nilq:PosintDecimal⊢ ∀ (acc : ℕ), List.foldl (fun a d => a * 10 + ↑d) acc [] = acc * 10 ^ [].length + ∑ i, ↑[][[].length - 1 - ↑i] * 10 ^ ↑i simpAll goals completed! 🐙
  | cons a t ih =>consq:PosintDecimala:Digitt:List Digitih:∀ (acc : ℕ), List.foldl (fun a d => a * 10 + ↑d) acc t = acc * 10 ^ t.length + ∑ i, ↑t[t.length - 1 - ↑i] * 10 ^ ↑i⊢ ∀ (acc : ℕ),
  List.foldl (fun a d => a * 10 + ↑d) acc (a :: t) =
    acc * 10 ^ (a :: t).length + ∑ i, ↑(a :: t)[(a :: t).length - 1 - ↑i] * 10 ^ ↑i
    intro accconsq:PosintDecimala:Digitt:List Digitih:∀ (acc : ℕ), List.foldl (fun a d => a * 10 + ↑d) acc t = acc * 10 ^ t.length + ∑ i, ↑t[t.length - 1 - ↑i] * 10 ^ ↑iacc:ℕ⊢ List.foldl (fun a d => a * 10 + ↑d) acc (a :: t) =
  acc * 10 ^ (a :: t).length + ∑ i, ↑(a :: t)[(a :: t).length - 1 - ↑i] * 10 ^ ↑i; simp only [List.foldl_cons, List.length_cons]consq:PosintDecimala:Digitt:List Digitih:∀ (acc : ℕ), List.foldl (fun a d => a * 10 + ↑d) acc t = acc * 10 ^ t.length + ∑ i, ↑t[t.length - 1 - ↑i] * 10 ^ ↑iacc:ℕ⊢ List.foldl (fun a d => a * 10 + ↑d) (acc * 10 + ↑a) t =
  acc * 10 ^ (t.length + 1) + ∑ x, ↑(a :: t)[t.length + 1 - 1 - ↑x] * 10 ^ ↑x
    -- Decompose the Fin (t.length+1) sum: last term is a*10^|t|, rest matches the Fin t.length sum
    have : ∑ x : Fin (t.length + 1), ((a :: t)[t.length - ↑x] : ℕ) * 10 ^ (↑x : ℕ) =
        (∑ x : Fin t.length, (t[t.length - 1 - ↑x] : ℕ) * 10 ^ (↑x : ℕ)) + a * 10 ^ t.length := byq:PosintDecimal⊢ ↑q = List.foldl (fun acc d => acc * 10 + ↑d) 0 q.digits
      refine (Fin.sum_univ_castSucc _).trans ?_q:PosintDecimala:Digitt:List Digitih:∀ (acc : ℕ), List.foldl (fun a d => a * 10 + ↑d) acc t = acc * 10 ^ t.length + ∑ i, ↑t[t.length - 1 - ↑i] * 10 ^ ↑iacc:ℕ⊢ ∑ i, ↑(a :: t)[t.length - ↑i.castSucc] * 10 ^ ↑i.castSucc +
    ↑(a :: t)[t.length - ↑(Fin.last t.length)] * 10 ^ ↑(Fin.last t.length) =
  ∑ x, ↑t[t.length - 1 - ↑x] * 10 ^ ↑x + ↑a * 10 ^ t.length
      congr 1e_aq:PosintDecimala:Digitt:List Digitih:∀ (acc : ℕ), List.foldl (fun a d => a * 10 + ↑d) acc t = acc * 10 ^ t.length + ∑ i, ↑t[t.length - 1 - ↑i] * 10 ^ ↑iacc:ℕ⊢ ∑ i, ↑(a :: t)[t.length - ↑i.castSucc] * 10 ^ ↑i.castSucc = ∑ x, ↑t[t.length - 1 - ↑x] * 10 ^ ↑xe_aq:PosintDecimala:Digitt:List Digitih:∀ (acc : ℕ), List.foldl (fun a d => a * 10 + ↑d) acc t = acc * 10 ^ t.length + ∑ i, ↑t[t.length - 1 - ↑i] * 10 ^ ↑iacc:ℕ⊢ ↑(a :: t)[t.length - ↑(Fin.last t.length)] * 10 ^ ↑(Fin.last t.length) = ↑a * 10 ^ t.length <;>e_aq:PosintDecimala:Digitt:List Digitih:∀ (acc : ℕ), List.foldl (fun a d => a * 10 + ↑d) acc t = acc * 10 ^ t.length + ∑ i, ↑t[t.length - 1 - ↑i] * 10 ^ ↑iacc:ℕ⊢ ∑ i, ↑(a :: t)[t.length - ↑i.castSucc] * 10 ^ ↑i.castSucc = ∑ x, ↑t[t.length - 1 - ↑x] * 10 ^ ↑xe_aq:PosintDecimala:Digitt:List Digitih:∀ (acc : ℕ), List.foldl (fun a d => a * 10 + ↑d) acc t = acc * 10 ^ t.length + ∑ i, ↑t[t.length - 1 - ↑i] * 10 ^ ↑iacc:ℕ⊢ ↑(a :: t)[t.length - ↑(Fin.last t.length)] * 10 ^ ↑(Fin.last t.length) = ↑a * 10 ^ t.length grindAll goals completed! 🐙
    grindAll goals completed! 🐙

@[simp]
theorem PosintDecimal.append_toNat (p:PosintDecimal) (d:Digit) :
  (p.append d:ℕ) = d.toNat + 10 * p.toNat  := byp:PosintDecimald:Digit⊢ ↑(p.append d) = ↑d + 10 * ↑p
  rw [toNat_eq_foldl, toNat_eq_foldl]p:PosintDecimald:Digit⊢ List.foldl (fun acc d => acc * 10 + ↑d) 0 (p.append d).digits =
  ↑d + 10 * List.foldl (fun acc d => acc * 10 + ↑d) 0 p.digits; simp only [append, mk']p:PosintDecimald:Digit⊢ List.foldl (fun acc d => acc * 10 + ↑d) 0 (p.head :: (p.digits.tail ++ [d])) =
  ↑d + 10 * List.foldl (fun acc d => acc * 10 + ↑d) 0 p.digits
  rw [show p.head :: (p.digits.tail ++ [d]) = p.digits ++ [d] from by
    simp [head, ← List.cons_append, List.cons_head_tail]]p:PosintDecimald:Digit⊢ List.foldl (fun acc d => acc * 10 + ↑d) 0 (p.digits ++ [d]) =
  ↑d + 10 * List.foldl (fun acc d => acc * 10 + ↑d) 0 p.digits
  rw [List.foldl_append]p:PosintDecimald:Digit⊢ List.foldl (fun acc d => acc * 10 + ↑d) (List.foldl (fun acc d => acc * 10 + ↑d) 0 p.digits) [d] =
  ↑d + 10 * List.foldl (fun acc d => acc * 10 + ↑d) 0 p.digits; simp [List.foldl]p:PosintDecimald:Digit⊢ List.foldl (fun acc d => acc * 10 + ↑d) 0 p.digits * 10 + ↑d =
  ↑d + 10 * List.foldl (fun acc d => acc * 10 + ↑d) 0 p.digits; ringAll goals completed! 🐙

theorem PosintDecimal.eq_append {p:PosintDecimal} (h: 2 ≤ p.digits.length) : ∃ (q:PosintDecimal) (d:Digit), p = q.append d := byp:PosintDecimalh:2 ≤ p.digits.length⊢ ∃ q d, p = q.append d
  use mk' p.head (p.digits.tail.dropLast) p.head_ne_zerohp:PosintDecimalh:2 ≤ p.digits.length⊢ ∃ d, p = (mk' p.head p.digits.tail.dropLast ⋯).append d
  set a := p.digits.getLast p.nonemptyhp:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := p.digits.getLast ⋯⊢ ∃ d, p = (mk' p.head p.digits.tail.dropLast ⋯).append d; use ahp:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := p.digits.getLast ⋯⊢ p = (mk' p.head p.digits.tail.dropLast ⋯).append a
  apply congr'h.hp:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := p.digits.getLast ⋯⊢ p.digits = ((mk' p.head p.digits.tail.dropLast ⋯).append a).digits
  simp [mk']h.hp:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := p.digits.getLast ⋯⊢ p.digits =
  { digits := p.head :: p.digits.tail.dropLast, nonempty := ⋯, nonzero := ⋯ }.head :: (p.digits.tail.dropLast ++ [a])
  rw [←p.digits.cons_head_tail p.nonempty]h.hp:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := p.digits.getLast ⋯⊢ p.digits.head ⋯ :: p.digits.tail =
  { digits := p.head :: (p.digits.head ⋯ :: p.digits.tail).tail.dropLast, nonempty := ⋯, nonzero := ⋯ }.head ::
    ((p.digits.head ⋯ :: p.digits.tail).tail.dropLast ++ [a])
  congr 1h.h.e_tailp:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := p.digits.getLast ⋯⊢ p.digits.tail = (p.digits.head ⋯ :: p.digits.tail).tail.dropLast ++ [a]
  convert (List.dropLast_append_getLast _).symm using 2h.e'_3.h.e'_6p:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := p.digits.getLast ⋯⊢ [a] = [p.digits.tail.getLast ?h.h.e_tail.convert_2]h.h.e_tail.convert_2p:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := p.digits.getLast ⋯⊢ p.digits.tail ≠ []; grindh.h.e_tail.convert_2p:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := p.digits.getLast ⋯⊢ p.digits.tail ≠ []
  simp [←List.length_pos_iff]h.h.e_tail.convert_2p:PosintDecimalh:2 ≤ p.digits.lengtha:Digit := p.digits.getLast ⋯⊢ 1 < p.digits.length; omegaAll goals completed! 🐙

Theorem B.1.4 (Uniqueness and existence of decimal representations)

theorem PosintDecimal.exists_unique (n:ℕ) : n > 0 → ∃! p:PosintDecimal, (p:ℕ) = n := byn:ℕ⊢ n > 0 → ∃! p, ↑p = n
  -- this proof is written to follow the structure of the original text.
  apply n.case_strong_induction_onhzn:ℕ⊢ 0 > 0 → ∃! p, ↑p = 0hin:ℕ⊢ ∀ (n : ℕ), (∀ m ≤ n, m > 0 → ∃! p, ↑p = m) → n + 1 > 0 → ∃! p, ↑p = n + 1
  .hzn:ℕ⊢ 0 > 0 → ∃! p, ↑p = 0 simpAll goals completed! 🐙
  -- note: the variable `m` in the text is referred to as `m+1` here.
  clear nhi⊢ ∀ (n : ℕ), (∀ m ≤ n, m > 0 → ∃! p, ↑p = m) → n + 1 > 0 → ∃! p, ↑p = n + 1; intro m hindhim:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1⊢ m + 1 > 0 → ∃! p, ↑p = m + 1 _him:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0⊢ ∃! p, ↑p = m + 1
  obtain hm | hm := lt_or_ge m 9hi.inlm:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9⊢ ∃! p, ↑p = m + 1hi.inrm:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:9 ≤ m⊢ ∃! p, ↑p = m + 1
  .hi.inlm:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9⊢ ∃! p, ↑p = m + 1 apply ExistsUnique.intro (mk' (.mk (show m+1 < 10 byn:ℕ⊢ n > 0 → ∃! p, ↑p = n omegaAll goals completed! 🐙)) [] (bym:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9⊢ Digit.mk ⋯ ≠ 0 simp [Digit.mk]All goals completed! 🐙))
    .hi.inl.h₁m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9⊢ ↑(mk' (Digit.mk ⋯) [] ⋯) = m + 1 simp [mk', Digit.mk, toNat, Digit.toNat]All goals completed! 🐙
    intro d hdhi.inl.h₂m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1⊢ d = mk' (Digit.mk ⋯) [] ⋯
    obtain hdl | hdl := lt_or_ge d.digits.length 2hi.inl.h₂.inlm:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:d.digits.length < 2⊢ d = mk' (Digit.mk ⋯) [] ⋯hi.inl.h₂.inrm:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.length⊢ d = mk' (Digit.mk ⋯) [] ⋯
    .hi.inl.h₂.inlm:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:d.digits.length < 2⊢ d = mk' (Digit.mk ⋯) [] ⋯ replace hdl : d.digits.length = 1 := byn:ℕ⊢ n > 0 → ∃! p, ↑p = n linarith [d.length_pos]All goals completed! 🐙
      have _subsing : Subsingleton (Fin d.digits.length) := byn:ℕ⊢ n > 0 → ∃! p, ↑p = n simp [Fin.subsingleton_iff_le_one, hdl]All goals completed! 🐙
      let zero : Fin d.digits.length := ⟨ 0, bym:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:d.digits.length = 1 := 
  Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt d.digits.length 1
    (Not.intro fun a =>
      Mathlib.Tactic.Linarith.lt_irrefl
        (Eq.mp
          (congrArg (fun _a => _a < 0)
            (Mathlib.Tactic.Ring.of_eq
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.add_congr
                  (Mathlib.Tactic.Ring.neg_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.neg_zero))
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                      (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                      (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1)))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                        (Mathlib.Meta.NormNum.IsInt.to_isNat
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                  (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 1).rawCast
                    (Mathlib.Tactic.Ring.add_pf_zero_add (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                (Mathlib.Tactic.Ring.sub_congr
                  (Mathlib.Tactic.Ring.add_congr
                    (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.add_pf_zero_add (Nat.rawCast 1 + 0)))
                  (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul (↑d.digits.length) (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1)
                      (Mathlib.Tactic.Ring.add_pf_zero_add
                        (↑d.digits.length ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                      (Eq.refl (Int.ofNat 0))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑d.digits.length) (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
              (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
          (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
            (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
              (Mathlib.Tactic.Linarith.sub_nonpos_of_le
                (Int.add_one_le_iff.mpr
                  (id
                    (Eq.mp
                      (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 d.digits.length 1)
                        (congrArg (LT.lt ↑d.digits.length) Nat.cast_one))
                      a)))))
            (Mathlib.Tactic.Linarith.sub_nonpos_of_le
              (Int.add_one_le_iff.mpr
                (id
                  (Eq.mp
                    (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 0 d.digits.length)
                      (congrFun' (congrArg LT.lt Nat.cast_zero) ↑d.digits.length))
                    (length_pos d))))))))
    (Not.intro fun a =>
      Mathlib.Tactic.Linarith.lt_irrefl
        (Eq.mp
          (congrArg (fun _a => _a < 0)
            (Mathlib.Tactic.Ring.of_eq
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.add_congr
                  (Mathlib.Tactic.Ring.neg_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.neg_zero))
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                      (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                      (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)))
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2))
                              (Eq.refl (Int.negOfNat 2)))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_add_overlap
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2)) (Eq.refl (Int.negOfNat 1))))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap
                    (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                      (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                (Mathlib.Tactic.Ring.sub_congr
                  (Mathlib.Tactic.Ring.add_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.add_pf_add_overlap
                      (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                        (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)
                          (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Eq.refl 2)))
                      (Mathlib.Tactic.Ring.add_pf_zero_add 0)))
                  (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul (↑d.digits.length) (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2)
                      (Mathlib.Tactic.Ring.add_pf_zero_add
                        (↑d.digits.length ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2))
                      (Eq.refl (Int.ofNat 0))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑d.digits.length) (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
              (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
          (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
            (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
              (Mathlib.Tactic.Linarith.sub_nonpos_of_le
                (Int.add_one_le_iff.mpr
                  (id (Eq.mp (Mathlib.Tactic.Zify.natCast_lt._simp_1 d.digits.length 2) _fvar.102828)))))
            (Mathlib.Tactic.Linarith.sub_nonpos_of_le
              (Int.add_one_le_iff.mpr
                (id
                  (Eq.mp
                    (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 1 d.digits.length)
                      (congrFun' (congrArg LT.lt Nat.cast_one) ↑d.digits.length))
                    a)))))))_subsing:Subsingleton (Fin d.digits.length) := 
  of_eq_true
    (Eq.trans (Eq.trans (congrArg Subsingleton (congrArg Fin hdl)) exists_unique._simp_1) (Std.le_refl._simp_1 1))⊢ 0 < d.digits.length omegaAll goals completed! 🐙 ⟩
      simp [toNat, hdl, Fintype.sum_subsingleton _ zero, zero, Digit.toNat] at hdhi.inl.h₂.inlm:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhdl:d.digits.length = 1 := 
  Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt d.digits.length 1
    (Not.intro fun a =>
      Mathlib.Tactic.Linarith.lt_irrefl
        (Eq.mp
          (congrArg (fun _a => _a < 0)
            (Mathlib.Tactic.Ring.of_eq
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.add_congr
                  (Mathlib.Tactic.Ring.neg_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.neg_zero))
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                      (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                      (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1)))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                        (Mathlib.Meta.NormNum.IsInt.to_isNat
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                  (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 1).rawCast
                    (Mathlib.Tactic.Ring.add_pf_zero_add (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                (Mathlib.Tactic.Ring.sub_congr
                  (Mathlib.Tactic.Ring.add_congr
                    (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.add_pf_zero_add (Nat.rawCast 1 + 0)))
                  (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul (↑d.digits.length) (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1)
                      (Mathlib.Tactic.Ring.add_pf_zero_add
                        (↑d.digits.length ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                      (Eq.refl (Int.ofNat 0))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑d.digits.length) (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
              (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
          (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
            (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
              (Mathlib.Tactic.Linarith.sub_nonpos_of_le
                (Int.add_one_le_iff.mpr
                  (id
                    (Eq.mp
                      (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 d.digits.length 1)
                        (congrArg (LT.lt ↑d.digits.length) Nat.cast_one))
                      a)))))
            (Mathlib.Tactic.Linarith.sub_nonpos_of_le
              (Int.add_one_le_iff.mpr
                (id
                  (Eq.mp
                    (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 0 d.digits.length)
                      (congrFun' (congrArg LT.lt Nat.cast_zero) ↑d.digits.length))
                    (length_pos d))))))))
    (Not.intro fun a =>
      Mathlib.Tactic.Linarith.lt_irrefl
        (Eq.mp
          (congrArg (fun _a => _a < 0)
            (Mathlib.Tactic.Ring.of_eq
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.add_congr
                  (Mathlib.Tactic.Ring.neg_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.neg_zero))
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                      (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                      (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)))
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2))
                              (Eq.refl (Int.negOfNat 2)))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_add_overlap
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2)) (Eq.refl (Int.negOfNat 1))))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap
                    (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                      (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                (Mathlib.Tactic.Ring.sub_congr
                  (Mathlib.Tactic.Ring.add_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.add_pf_add_overlap
                      (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                        (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)
                          (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Eq.refl 2)))
                      (Mathlib.Tactic.Ring.add_pf_zero_add 0)))
                  (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul (↑d.digits.length) (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2)
                      (Mathlib.Tactic.Ring.add_pf_zero_add
                        (↑d.digits.length ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2))
                      (Eq.refl (Int.ofNat 0))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑d.digits.length) (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
              (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
          (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
            (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
              (Mathlib.Tactic.Linarith.sub_nonpos_of_le
                (Int.add_one_le_iff.mpr
                  (id (Eq.mp (Mathlib.Tactic.Zify.natCast_lt._simp_1 d.digits.length 2) _fvar.102828)))))
            (Mathlib.Tactic.Linarith.sub_nonpos_of_le
              (Int.add_one_le_iff.mpr
                (id
                  (Eq.mp
                    (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 1 d.digits.length)
                      (congrFun' (congrArg LT.lt Nat.cast_one) ↑d.digits.length))
                    a)))))))_subsing:Subsingleton (Fin d.digits.length) := 
  of_eq_true
    (Eq.trans (Eq.trans (congrArg Subsingleton (congrArg Fin hdl)) exists_unique._simp_1) (Std.le_refl._simp_1 1))zero:Fin d.digits.length := ⟨0, ⋯⟩hd:↑d.digits[0] = m + 1⊢ d = mk' (Digit.mk ⋯) [] ⋯
      apply congrhi.inl.h₂.inl.hm:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhdl:d.digits.length = 1 := 
  Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt d.digits.length 1
    (Not.intro fun a =>
      Mathlib.Tactic.Linarith.lt_irrefl
        (Eq.mp
          (congrArg (fun _a => _a < 0)
            (Mathlib.Tactic.Ring.of_eq
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.add_congr
                  (Mathlib.Tactic.Ring.neg_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.neg_zero))
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                      (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                      (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1)))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                        (Mathlib.Meta.NormNum.IsInt.to_isNat
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                  (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 1).rawCast
                    (Mathlib.Tactic.Ring.add_pf_zero_add (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                (Mathlib.Tactic.Ring.sub_congr
                  (Mathlib.Tactic.Ring.add_congr
                    (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.add_pf_zero_add (Nat.rawCast 1 + 0)))
                  (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul (↑d.digits.length) (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1)
                      (Mathlib.Tactic.Ring.add_pf_zero_add
                        (↑d.digits.length ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                      (Eq.refl (Int.ofNat 0))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑d.digits.length) (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
              (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
          (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
            (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
              (Mathlib.Tactic.Linarith.sub_nonpos_of_le
                (Int.add_one_le_iff.mpr
                  (id
                    (Eq.mp
                      (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 d.digits.length 1)
                        (congrArg (LT.lt ↑d.digits.length) Nat.cast_one))
                      a)))))
            (Mathlib.Tactic.Linarith.sub_nonpos_of_le
              (Int.add_one_le_iff.mpr
                (id
                  (Eq.mp
                    (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 0 d.digits.length)
                      (congrFun' (congrArg LT.lt Nat.cast_zero) ↑d.digits.length))
                    (length_pos d))))))))
    (Not.intro fun a =>
      Mathlib.Tactic.Linarith.lt_irrefl
        (Eq.mp
          (congrArg (fun _a => _a < 0)
            (Mathlib.Tactic.Ring.of_eq
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.add_congr
                  (Mathlib.Tactic.Ring.neg_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.neg_zero))
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                      (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                      (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)))
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2))
                              (Eq.refl (Int.negOfNat 2)))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_add_overlap
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2)) (Eq.refl (Int.negOfNat 1))))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap
                    (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                      (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                (Mathlib.Tactic.Ring.sub_congr
                  (Mathlib.Tactic.Ring.add_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.add_pf_add_overlap
                      (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                        (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)
                          (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Eq.refl 2)))
                      (Mathlib.Tactic.Ring.add_pf_zero_add 0)))
                  (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul (↑d.digits.length) (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2)
                      (Mathlib.Tactic.Ring.add_pf_zero_add
                        (↑d.digits.length ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2))
                      (Eq.refl (Int.ofNat 0))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑d.digits.length) (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
              (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
          (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
            (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
              (Mathlib.Tactic.Linarith.sub_nonpos_of_le
                (Int.add_one_le_iff.mpr
                  (id (Eq.mp (Mathlib.Tactic.Zify.natCast_lt._simp_1 d.digits.length 2) _fvar.102828)))))
            (Mathlib.Tactic.Linarith.sub_nonpos_of_le
              (Int.add_one_le_iff.mpr
                (id
                  (Eq.mp
                    (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 1 d.digits.length)
                      (congrFun' (congrArg LT.lt Nat.cast_one) ↑d.digits.length))
                    a)))))))_subsing:Subsingleton (Fin d.digits.length) := 
  of_eq_true
    (Eq.trans (Eq.trans (congrArg Subsingleton (congrArg Fin hdl)) exists_unique._simp_1) (Std.le_refl._simp_1 1))zero:Fin d.digits.length := ⟨0, ⋯⟩hd:↑d.digits[0] = m + 1⊢ d.digits.length = (mk' (Digit.mk ⋯) [] ⋯).digits.lengthhi.inl.h₂.inl.h'm:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhdl:d.digits.length = 1 := 
  Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt d.digits.length 1
    (Not.intro fun a =>
      Mathlib.Tactic.Linarith.lt_irrefl
        (Eq.mp
          (congrArg (fun _a => _a < 0)
            (Mathlib.Tactic.Ring.of_eq
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.add_congr
                  (Mathlib.Tactic.Ring.neg_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.neg_zero))
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                      (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                      (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1)))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                        (Mathlib.Meta.NormNum.IsInt.to_isNat
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                  (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 1).rawCast
                    (Mathlib.Tactic.Ring.add_pf_zero_add (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                (Mathlib.Tactic.Ring.sub_congr
                  (Mathlib.Tactic.Ring.add_congr
                    (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.add_pf_zero_add (Nat.rawCast 1 + 0)))
                  (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul (↑d.digits.length) (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1)
                      (Mathlib.Tactic.Ring.add_pf_zero_add
                        (↑d.digits.length ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                      (Eq.refl (Int.ofNat 0))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑d.digits.length) (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
              (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
          (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
            (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
              (Mathlib.Tactic.Linarith.sub_nonpos_of_le
                (Int.add_one_le_iff.mpr
                  (id
                    (Eq.mp
                      (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 d.digits.length 1)
                        (congrArg (LT.lt ↑d.digits.length) Nat.cast_one))
                      a)))))
            (Mathlib.Tactic.Linarith.sub_nonpos_of_le
              (Int.add_one_le_iff.mpr
                (id
                  (Eq.mp
                    (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 0 d.digits.length)
                      (congrFun' (congrArg LT.lt Nat.cast_zero) ↑d.digits.length))
                    (length_pos d))))))))
    (Not.intro fun a =>
      Mathlib.Tactic.Linarith.lt_irrefl
        (Eq.mp
          (congrArg (fun _a => _a < 0)
            (Mathlib.Tactic.Ring.of_eq
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.add_congr
                  (Mathlib.Tactic.Ring.neg_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.neg_zero))
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                      (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                      (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)))
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2))
                              (Eq.refl (Int.negOfNat 2)))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_add_overlap
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2)) (Eq.refl (Int.negOfNat 1))))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap
                    (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                      (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                (Mathlib.Tactic.Ring.sub_congr
                  (Mathlib.Tactic.Ring.add_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.add_pf_add_overlap
                      (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                        (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)
                          (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Eq.refl 2)))
                      (Mathlib.Tactic.Ring.add_pf_zero_add 0)))
                  (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul (↑d.digits.length) (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2)
                      (Mathlib.Tactic.Ring.add_pf_zero_add
                        (↑d.digits.length ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2))
                      (Eq.refl (Int.ofNat 0))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑d.digits.length) (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
              (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
          (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
            (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
              (Mathlib.Tactic.Linarith.sub_nonpos_of_le
                (Int.add_one_le_iff.mpr
                  (id (Eq.mp (Mathlib.Tactic.Zify.natCast_lt._simp_1 d.digits.length 2) _fvar.102828)))))
            (Mathlib.Tactic.Linarith.sub_nonpos_of_le
              (Int.add_one_le_iff.mpr
                (id
                  (Eq.mp
                    (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 1 d.digits.length)
                      (congrFun' (congrArg LT.lt Nat.cast_one) ↑d.digits.length))
                    a)))))))_subsing:Subsingleton (Fin d.digits.length) := 
  of_eq_true
    (Eq.trans (Eq.trans (congrArg Subsingleton (congrArg Fin hdl)) exists_unique._simp_1) (Std.le_refl._simp_1 1))zero:Fin d.digits.length := ⟨0, ⋯⟩hd:↑d.digits[0] = m + 1⊢ ∀ (n : ℕ) (h₁ : n < d.digits.length) (h₂ : n < (mk' (Digit.mk ⋯) [] ⋯).digits.length),
  d.digits.get ⟨n, h₁⟩ = (mk' (Digit.mk ⋯) [] ⋯).digits.get ⟨n, h₂⟩
      .hi.inl.h₂.inl.hm:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhdl:d.digits.length = 1 := 
  Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt d.digits.length 1
    (Not.intro fun a =>
      Mathlib.Tactic.Linarith.lt_irrefl
        (Eq.mp
          (congrArg (fun _a => _a < 0)
            (Mathlib.Tactic.Ring.of_eq
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.add_congr
                  (Mathlib.Tactic.Ring.neg_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.neg_zero))
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                      (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                      (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1)))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                        (Mathlib.Meta.NormNum.IsInt.to_isNat
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                  (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 1).rawCast
                    (Mathlib.Tactic.Ring.add_pf_zero_add (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                (Mathlib.Tactic.Ring.sub_congr
                  (Mathlib.Tactic.Ring.add_congr
                    (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.add_pf_zero_add (Nat.rawCast 1 + 0)))
                  (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul (↑d.digits.length) (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1)
                      (Mathlib.Tactic.Ring.add_pf_zero_add
                        (↑d.digits.length ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                      (Eq.refl (Int.ofNat 0))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑d.digits.length) (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
              (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
          (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
            (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
              (Mathlib.Tactic.Linarith.sub_nonpos_of_le
                (Int.add_one_le_iff.mpr
                  (id
                    (Eq.mp
                      (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 d.digits.length 1)
                        (congrArg (LT.lt ↑d.digits.length) Nat.cast_one))
                      a)))))
            (Mathlib.Tactic.Linarith.sub_nonpos_of_le
              (Int.add_one_le_iff.mpr
                (id
                  (Eq.mp
                    (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 0 d.digits.length)
                      (congrFun' (congrArg LT.lt Nat.cast_zero) ↑d.digits.length))
                    (length_pos d))))))))
    (Not.intro fun a =>
      Mathlib.Tactic.Linarith.lt_irrefl
        (Eq.mp
          (congrArg (fun _a => _a < 0)
            (Mathlib.Tactic.Ring.of_eq
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.add_congr
                  (Mathlib.Tactic.Ring.neg_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.neg_zero))
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                      (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                      (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)))
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2))
                              (Eq.refl (Int.negOfNat 2)))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_add_overlap
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2)) (Eq.refl (Int.negOfNat 1))))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap
                    (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                      (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                (Mathlib.Tactic.Ring.sub_congr
                  (Mathlib.Tactic.Ring.add_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.add_pf_add_overlap
                      (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                        (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)
                          (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Eq.refl 2)))
                      (Mathlib.Tactic.Ring.add_pf_zero_add 0)))
                  (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul (↑d.digits.length) (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2)
                      (Mathlib.Tactic.Ring.add_pf_zero_add
                        (↑d.digits.length ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2))
                      (Eq.refl (Int.ofNat 0))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑d.digits.length) (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
              (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
          (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
            (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
              (Mathlib.Tactic.Linarith.sub_nonpos_of_le
                (Int.add_one_le_iff.mpr
                  (id (Eq.mp (Mathlib.Tactic.Zify.natCast_lt._simp_1 d.digits.length 2) _fvar.102828)))))
            (Mathlib.Tactic.Linarith.sub_nonpos_of_le
              (Int.add_one_le_iff.mpr
                (id
                  (Eq.mp
                    (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 1 d.digits.length)
                      (congrFun' (congrArg LT.lt Nat.cast_one) ↑d.digits.length))
                    a)))))))_subsing:Subsingleton (Fin d.digits.length) := 
  of_eq_true
    (Eq.trans (Eq.trans (congrArg Subsingleton (congrArg Fin hdl)) exists_unique._simp_1) (Std.le_refl._simp_1 1))zero:Fin d.digits.length := ⟨0, ⋯⟩hd:↑d.digits[0] = m + 1⊢ d.digits.length = (mk' (Digit.mk ⋯) [] ⋯).digits.length simp [hdl, mk']All goals completed! 🐙
      intro i hi₁hi.inl.h₂.inl.h'm:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhdl:d.digits.length = 1 := 
  Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt d.digits.length 1
    (Not.intro fun a =>
      Mathlib.Tactic.Linarith.lt_irrefl
        (Eq.mp
          (congrArg (fun _a => _a < 0)
            (Mathlib.Tactic.Ring.of_eq
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.add_congr
                  (Mathlib.Tactic.Ring.neg_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.neg_zero))
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                      (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                      (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1)))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                        (Mathlib.Meta.NormNum.IsInt.to_isNat
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                  (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 1).rawCast
                    (Mathlib.Tactic.Ring.add_pf_zero_add (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                (Mathlib.Tactic.Ring.sub_congr
                  (Mathlib.Tactic.Ring.add_congr
                    (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.add_pf_zero_add (Nat.rawCast 1 + 0)))
                  (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul (↑d.digits.length) (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1)
                      (Mathlib.Tactic.Ring.add_pf_zero_add
                        (↑d.digits.length ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                      (Eq.refl (Int.ofNat 0))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑d.digits.length) (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
              (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
          (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
            (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
              (Mathlib.Tactic.Linarith.sub_nonpos_of_le
                (Int.add_one_le_iff.mpr
                  (id
                    (Eq.mp
                      (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 d.digits.length 1)
                        (congrArg (LT.lt ↑d.digits.length) Nat.cast_one))
                      a)))))
            (Mathlib.Tactic.Linarith.sub_nonpos_of_le
              (Int.add_one_le_iff.mpr
                (id
                  (Eq.mp
                    (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 0 d.digits.length)
                      (congrFun' (congrArg LT.lt Nat.cast_zero) ↑d.digits.length))
                    (length_pos d))))))))
    (Not.intro fun a =>
      Mathlib.Tactic.Linarith.lt_irrefl
        (Eq.mp
          (congrArg (fun _a => _a < 0)
            (Mathlib.Tactic.Ring.of_eq
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.add_congr
                  (Mathlib.Tactic.Ring.neg_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.neg_zero))
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                      (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                      (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)))
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2))
                              (Eq.refl (Int.negOfNat 2)))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_add_overlap
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2)) (Eq.refl (Int.negOfNat 1))))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap
                    (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                      (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                (Mathlib.Tactic.Ring.sub_congr
                  (Mathlib.Tactic.Ring.add_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.add_pf_add_overlap
                      (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                        (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)
                          (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Eq.refl 2)))
                      (Mathlib.Tactic.Ring.add_pf_zero_add 0)))
                  (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul (↑d.digits.length) (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2)
                      (Mathlib.Tactic.Ring.add_pf_zero_add
                        (↑d.digits.length ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2))
                      (Eq.refl (Int.ofNat 0))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑d.digits.length) (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
              (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
          (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
            (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
              (Mathlib.Tactic.Linarith.sub_nonpos_of_le
                (Int.add_one_le_iff.mpr
                  (id (Eq.mp (Mathlib.Tactic.Zify.natCast_lt._simp_1 d.digits.length 2) _fvar.102828)))))
            (Mathlib.Tactic.Linarith.sub_nonpos_of_le
              (Int.add_one_le_iff.mpr
                (id
                  (Eq.mp
                    (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 1 d.digits.length)
                      (congrFun' (congrArg LT.lt Nat.cast_one) ↑d.digits.length))
                    a)))))))_subsing:Subsingleton (Fin d.digits.length) := 
  of_eq_true
    (Eq.trans (Eq.trans (congrArg Subsingleton (congrArg Fin hdl)) exists_unique._simp_1) (Std.le_refl._simp_1 1))zero:Fin d.digits.length := ⟨0, ⋯⟩hd:↑d.digits[0] = m + 1i:ℕhi₁:i < d.digits.length⊢ ∀ (h₂ : i < (mk' (Digit.mk ⋯) [] ⋯).digits.length), d.digits.get ⟨i, hi₁⟩ = (mk' (Digit.mk ⋯) [] ⋯).digits.get ⟨i, h₂⟩ hi₂hi.inl.h₂.inl.h'm:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhdl:d.digits.length = 1 := 
  Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt d.digits.length 1
    (Not.intro fun a =>
      Mathlib.Tactic.Linarith.lt_irrefl
        (Eq.mp
          (congrArg (fun _a => _a < 0)
            (Mathlib.Tactic.Ring.of_eq
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.add_congr
                  (Mathlib.Tactic.Ring.neg_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.neg_zero))
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                      (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                      (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1)))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                        (Mathlib.Meta.NormNum.IsInt.to_isNat
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                  (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 1).rawCast
                    (Mathlib.Tactic.Ring.add_pf_zero_add (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                (Mathlib.Tactic.Ring.sub_congr
                  (Mathlib.Tactic.Ring.add_congr
                    (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.add_pf_zero_add (Nat.rawCast 1 + 0)))
                  (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul (↑d.digits.length) (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1)
                      (Mathlib.Tactic.Ring.add_pf_zero_add
                        (↑d.digits.length ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                      (Eq.refl (Int.ofNat 0))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑d.digits.length) (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
              (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
          (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
            (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
              (Mathlib.Tactic.Linarith.sub_nonpos_of_le
                (Int.add_one_le_iff.mpr
                  (id
                    (Eq.mp
                      (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 d.digits.length 1)
                        (congrArg (LT.lt ↑d.digits.length) Nat.cast_one))
                      a)))))
            (Mathlib.Tactic.Linarith.sub_nonpos_of_le
              (Int.add_one_le_iff.mpr
                (id
                  (Eq.mp
                    (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 0 d.digits.length)
                      (congrFun' (congrArg LT.lt Nat.cast_zero) ↑d.digits.length))
                    (length_pos d))))))))
    (Not.intro fun a =>
      Mathlib.Tactic.Linarith.lt_irrefl
        (Eq.mp
          (congrArg (fun _a => _a < 0)
            (Mathlib.Tactic.Ring.of_eq
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.add_congr
                  (Mathlib.Tactic.Ring.neg_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.neg_zero))
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                      (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                      (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)))
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2))
                              (Eq.refl (Int.negOfNat 2)))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_add_overlap
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2)) (Eq.refl (Int.negOfNat 1))))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap
                    (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                      (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add (↑d.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                (Mathlib.Tactic.Ring.sub_congr
                  (Mathlib.Tactic.Ring.add_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.add_pf_add_overlap
                      (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                        (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)
                          (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Eq.refl 2)))
                      (Mathlib.Tactic.Ring.add_pf_zero_add 0)))
                  (Mathlib.Tactic.Ring.atom_pf ↑d.digits.length)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul (↑d.digits.length) (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2)
                      (Mathlib.Tactic.Ring.add_pf_zero_add
                        (↑d.digits.length ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2))
                      (Eq.refl (Int.ofNat 0))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑d.digits.length) (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
              (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
          (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
            (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
              (Mathlib.Tactic.Linarith.sub_nonpos_of_le
                (Int.add_one_le_iff.mpr
                  (id (Eq.mp (Mathlib.Tactic.Zify.natCast_lt._simp_1 d.digits.length 2) _fvar.102828)))))
            (Mathlib.Tactic.Linarith.sub_nonpos_of_le
              (Int.add_one_le_iff.mpr
                (id
                  (Eq.mp
                    (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 1 d.digits.length)
                      (congrFun' (congrArg LT.lt Nat.cast_one) ↑d.digits.length))
                    a)))))))_subsing:Subsingleton (Fin d.digits.length) := 
  of_eq_true
    (Eq.trans (Eq.trans (congrArg Subsingleton (congrArg Fin hdl)) exists_unique._simp_1) (Std.le_refl._simp_1 1))zero:Fin d.digits.length := ⟨0, ⋯⟩hd:↑d.digits[0] = m + 1i:ℕhi₁:i < d.digits.lengthhi₂:i < (mk' (Digit.mk ⋯) [] ⋯).digits.length⊢ d.digits.get ⟨i, hi₁⟩ = (mk' (Digit.mk ⋯) [] ⋯).digits.get ⟨i, hi₂⟩
      replace hi₁ : i = 0 := byn:ℕ⊢ n > 0 → ∃! p, ↑p = n omegaAll goals completed! 🐙
      simp [hi₁, mk', Digit.mk, hd]All goals completed! 🐙
    have : d.toNat ≥ 10 := calc
      _ ≥ (d.head:ℕ) * 10^(d.digits.length-1) := bym:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.length⊢ ↑d ≥ ↑d.head * 10 ^ (d.digits.length - 1)
        set a : Fin d.digits.length := ⟨ d.digits.length - 1, bym:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.length⊢ d.digits.length - 1 < d.digits.length omegaAll goals completed! 🐙 ⟩
        convert Finset.single_le_sum _ (Finset.mem_univ a)h.e'_4.h.e'_5.h.e'_1m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.lengtha:Fin d.digits.length := ⟨d.digits.length - 1, ⋯⟩⊢ d.head = d.digits[d.digits.length - 1 - ↑a]convert_5m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.lengtha:Fin d.digits.length := ⟨d.digits.length - 1, ⋯⟩⊢ AddLeftMono ℕconvert_6m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.lengtha:Fin d.digits.length := ⟨d.digits.length - 1, ⋯⟩⊢ ∀ i ∈ Finset.univ, 0 ≤ ↑d.digits[d.digits.length - 1 - ↑i] * 10 ^ ↑i
        .h.e'_4.h.e'_5.h.e'_1m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.lengtha:Fin d.digits.length := ⟨d.digits.length - 1, ⋯⟩⊢ d.head = d.digits[d.digits.length - 1 - ↑a] simp [a, head, List.head_eq_getElem]All goals completed! 🐙
        .convert_5m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.lengtha:Fin d.digits.length := ⟨d.digits.length - 1, ⋯⟩⊢ AddLeftMono ℕ infer_instanceAll goals completed! 🐙
        introsconvert_6m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝¹:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.lengtha:Fin d.digits.length := ⟨d.digits.length - 1, ⋯⟩i✝:Fin d.digits.lengtha✝:i✝ ∈ Finset.univ⊢ 0 ≤ ↑d.digits[d.digits.length - 1 - ↑i✝] * 10 ^ ↑i✝; positivityAll goals completed! 🐙
      _ ≥ 1 * 10^(2-1) := bym:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.length⊢ ↑d.head * 10 ^ (d.digits.length - 1) ≥ 1 * 10 ^ (2 - 1)
        gcongrh₁m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.length⊢ 1 ≤ ↑d.headh₂.ham:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.length⊢ 1 ≤ 10
        .h₁m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.length⊢ 1 ≤ ↑d.head have := d.head_ne_zero'h₁m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.lengththis:↑d.head ≠ 0 := head_ne_zero' d⊢ 1 ≤ ↑d.head; omegaAll goals completed! 🐙
        norm_numAll goals completed! 🐙
      _ = 10 := bym:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:m < 9d:PosintDecimalhd:↑d = m + 1hdl:2 ≤ d.digits.length⊢ 1 * 10 ^ (2 - 1) = 10 norm_numAll goals completed! 🐙
    linarithAll goals completed! 🐙
  have := (m+1).mod_add_div 10hi.inrm:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:9 ≤ mthis:(m + 1) % 10 + 10 * ((m + 1) / 10) = m + 1 := Nat.mod_add_div (m + 1) 10⊢ ∃! p, ↑p = m + 1
  set s := (m+1)/10hi.inrm:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10this:(m + 1) % 10 + 10 * s = m + 1⊢ ∃! p, ↑p = m + 1
  set r := (m+1) % 10hi.inrm:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1⊢ ∃! p, ↑p = m + 1
  have hr : r < 10 := byn:ℕ⊢ n > 0 → ∃! p, ↑p = n grindAll goals completed! 🐙
  specialize hind s _ _hi.inr.specialize_1m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 m⊢ s ≤ mhi.inr.specialize_2m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 m⊢ s > 0hi.inrm:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 mhind:∃! p, ↑p = s⊢ ∃! p, ↑p = m + 1 <;>hi.inr.specialize_1m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 m⊢ s ≤ mhi.inr.specialize_2m:ℕhind:∀ m_1 ≤ m, m_1 > 0 → ∃! p, ↑p = m_1a✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 m⊢ s > 0hi.inrm:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 mhind:∃! p, ↑p = s⊢ ∃! p, ↑p = m + 1 try linarithhi.inrm:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 mhind:∃! p, ↑p = s⊢ ∃! p, ↑p = m + 1
  choose b hb huniq using hindhi.inrm:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 mb:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), (fun p => ↑p = s) y → y = b⊢ ∃! p, ↑p = m + 1; simp at huniqhi.inrm:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 mb:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = b⊢ ∃! p, ↑p = m + 1
  apply ExistsUnique.intro (b.append (.mk hr))hi.inr.h₁m:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 mb:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = b⊢ ↑(b.append (Digit.mk hr)) = m + 1hi.inr.h₂m:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 mb:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = b⊢ ∀ (y : PosintDecimal), ↑y = m + 1 → y = b.append (Digit.mk hr)
  .hi.inr.h₁m:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 mb:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = b⊢ ↑(b.append (Digit.mk hr)) = m + 1 simp [←this, hb]All goals completed! 🐙
  intro a hahi.inr.h₂m:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 mb:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = ba:PosintDecimalha:↑a = m + 1⊢ a = b.append (Digit.mk hr)
  obtain hal | hal := lt_or_ge a.digits.length 2hi.inr.h₂.inlm:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 mb:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = ba:PosintDecimalha:↑a = m + 1hal:a.digits.length < 2⊢ a = b.append (Digit.mk hr)hi.inr.h₂.inrm:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 mb:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = ba:PosintDecimalha:↑a = m + 1hal:2 ≤ a.digits.length⊢ a = b.append (Digit.mk hr)
  .hi.inr.h₂.inlm:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 mb:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = ba:PosintDecimalha:↑a = m + 1hal:a.digits.length < 2⊢ a = b.append (Digit.mk hr) replace hal : a.digits.length = 1 := byn:ℕ⊢ n > 0 → ∃! p, ↑p = n linarith [a.length_pos]All goals completed! 🐙
    have _subsing : Subsingleton (Fin a.digits.length) := byn:ℕ⊢ n > 0 → ∃! p, ↑p = n simp [Fin.subsingleton_iff_le_one, hal]All goals completed! 🐙
    let zero : Fin a.digits.length := ⟨ 0, bym:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 mb:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = ba:PosintDecimalha:↑a = m + 1hal:a.digits.length = 1 := 
  Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt a.digits.length 1
    (Not.intro fun a_1 =>
      Mathlib.Tactic.Linarith.lt_irrefl
        (Eq.mp
          (congrArg (fun _a => _a < 0)
            (Mathlib.Tactic.Ring.of_eq
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.add_congr
                  (Mathlib.Tactic.Ring.neg_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.neg_zero))
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑a.digits.length)
                      (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                      (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑a.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1)))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                        (Mathlib.Meta.NormNum.IsInt.to_isNat
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑a.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                  (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 1).rawCast
                    (Mathlib.Tactic.Ring.add_pf_zero_add (↑a.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                (Mathlib.Tactic.Ring.sub_congr
                  (Mathlib.Tactic.Ring.add_congr
                    (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.add_pf_zero_add (Nat.rawCast 1 + 0)))
                  (Mathlib.Tactic.Ring.atom_pf ↑a.digits.length)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul (↑a.digits.length) (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1)
                      (Mathlib.Tactic.Ring.add_pf_zero_add
                        (↑a.digits.length ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                      (Eq.refl (Int.ofNat 0))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑a.digits.length) (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
              (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
          (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
            (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
              (Mathlib.Tactic.Linarith.sub_nonpos_of_le
                (Int.add_one_le_iff.mpr
                  (id
                    (Eq.mp
                      (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 a.digits.length 1)
                        (congrArg (LT.lt ↑a.digits.length) Nat.cast_one))
                      a_1)))))
            (Mathlib.Tactic.Linarith.sub_nonpos_of_le
              (Int.add_one_le_iff.mpr
                (id
                  (Eq.mp
                    (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 0 a.digits.length)
                      (congrFun' (congrArg LT.lt Nat.cast_zero) ↑a.digits.length))
                    (length_pos a))))))))
    (Not.intro fun a_1 =>
      Mathlib.Tactic.Linarith.lt_irrefl
        (Eq.mp
          (congrArg (fun _a => _a < 0)
            (Mathlib.Tactic.Ring.of_eq
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.add_congr
                  (Mathlib.Tactic.Ring.neg_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.neg_zero))
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑a.digits.length)
                      (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                      (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑a.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)))
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2))
                              (Eq.refl (Int.negOfNat 2)))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_add_overlap
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2)) (Eq.refl (Int.negOfNat 1))))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑a.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap
                    (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                      (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add (↑a.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                (Mathlib.Tactic.Ring.sub_congr
                  (Mathlib.Tactic.Ring.add_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.add_pf_add_overlap
                      (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                        (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)
                          (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Eq.refl 2)))
                      (Mathlib.Tactic.Ring.add_pf_zero_add 0)))
                  (Mathlib.Tactic.Ring.atom_pf ↑a.digits.length)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul (↑a.digits.length) (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2)
                      (Mathlib.Tactic.Ring.add_pf_zero_add
                        (↑a.digits.length ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2))
                      (Eq.refl (Int.ofNat 0))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑a.digits.length) (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
              (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
          (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
            (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
              (Mathlib.Tactic.Linarith.sub_nonpos_of_le
                (Int.add_one_le_iff.mpr
                  (id (Eq.mp (Mathlib.Tactic.Zify.natCast_lt._simp_1 a.digits.length 2) _fvar.154273)))))
            (Mathlib.Tactic.Linarith.sub_nonpos_of_le
              (Int.add_one_le_iff.mpr
                (id
                  (Eq.mp
                    (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 1 a.digits.length)
                      (congrFun' (congrArg LT.lt Nat.cast_one) ↑a.digits.length))
                    a_1)))))))_subsing:Subsingleton (Fin a.digits.length) := 
  of_eq_true
    (Eq.trans (Eq.trans (congrArg Subsingleton (congrArg Fin hal)) exists_unique._simp_1) (Std.le_refl._simp_1 1))⊢ 0 < a.digits.length linarithAll goals completed! 🐙 ⟩
    simp [toNat, hal, Fintype.sum_subsingleton _ zero, zero, Digit.toNat] at hahi.inr.h₂.inlm:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 mb:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = ba:PosintDecimalhal:a.digits.length = 1 := 
  Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt a.digits.length 1
    (Not.intro fun a_1 =>
      Mathlib.Tactic.Linarith.lt_irrefl
        (Eq.mp
          (congrArg (fun _a => _a < 0)
            (Mathlib.Tactic.Ring.of_eq
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.add_congr
                  (Mathlib.Tactic.Ring.neg_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.neg_zero))
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑a.digits.length)
                      (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                      (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑a.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1)))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                        (Mathlib.Meta.NormNum.IsInt.to_isNat
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑a.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                  (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 1).rawCast
                    (Mathlib.Tactic.Ring.add_pf_zero_add (↑a.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                (Mathlib.Tactic.Ring.sub_congr
                  (Mathlib.Tactic.Ring.add_congr
                    (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.add_pf_zero_add (Nat.rawCast 1 + 0)))
                  (Mathlib.Tactic.Ring.atom_pf ↑a.digits.length)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul (↑a.digits.length) (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1)
                      (Mathlib.Tactic.Ring.add_pf_zero_add
                        (↑a.digits.length ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                      (Eq.refl (Int.ofNat 0))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑a.digits.length) (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
              (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
          (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
            (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
              (Mathlib.Tactic.Linarith.sub_nonpos_of_le
                (Int.add_one_le_iff.mpr
                  (id
                    (Eq.mp
                      (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 a.digits.length 1)
                        (congrArg (LT.lt ↑a.digits.length) Nat.cast_one))
                      a_1)))))
            (Mathlib.Tactic.Linarith.sub_nonpos_of_le
              (Int.add_one_le_iff.mpr
                (id
                  (Eq.mp
                    (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 0 a.digits.length)
                      (congrFun' (congrArg LT.lt Nat.cast_zero) ↑a.digits.length))
                    (length_pos a))))))))
    (Not.intro fun a_1 =>
      Mathlib.Tactic.Linarith.lt_irrefl
        (Eq.mp
          (congrArg (fun _a => _a < 0)
            (Mathlib.Tactic.Ring.of_eq
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.add_congr
                  (Mathlib.Tactic.Ring.neg_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.neg_zero))
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑a.digits.length)
                      (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                      (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑a.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)))
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2))
                              (Eq.refl (Int.negOfNat 2)))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_add_overlap
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2)) (Eq.refl (Int.negOfNat 1))))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑a.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap
                    (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                      (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add (↑a.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                (Mathlib.Tactic.Ring.sub_congr
                  (Mathlib.Tactic.Ring.add_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.add_pf_add_overlap
                      (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                        (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)
                          (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Eq.refl 2)))
                      (Mathlib.Tactic.Ring.add_pf_zero_add 0)))
                  (Mathlib.Tactic.Ring.atom_pf ↑a.digits.length)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul (↑a.digits.length) (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2)
                      (Mathlib.Tactic.Ring.add_pf_zero_add
                        (↑a.digits.length ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2))
                      (Eq.refl (Int.ofNat 0))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑a.digits.length) (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
              (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
          (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
            (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
              (Mathlib.Tactic.Linarith.sub_nonpos_of_le
                (Int.add_one_le_iff.mpr
                  (id (Eq.mp (Mathlib.Tactic.Zify.natCast_lt._simp_1 a.digits.length 2) _fvar.154273)))))
            (Mathlib.Tactic.Linarith.sub_nonpos_of_le
              (Int.add_one_le_iff.mpr
                (id
                  (Eq.mp
                    (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 1 a.digits.length)
                      (congrFun' (congrArg LT.lt Nat.cast_one) ↑a.digits.length))
                    a_1)))))))_subsing:Subsingleton (Fin a.digits.length) := 
  of_eq_true
    (Eq.trans (Eq.trans (congrArg Subsingleton (congrArg Fin hal)) exists_unique._simp_1) (Std.le_refl._simp_1 1))zero:Fin a.digits.length := ⟨0, ⋯⟩ha:↑a.digits[0] = m + 1⊢ a = b.append (Digit.mk hr)
    observe : a.digits[0].val < 10hi.inr.h₂.inlm:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this✝:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 mb:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = ba:PosintDecimalhal:a.digits.length = 1 := 
  Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt a.digits.length 1
    (Not.intro fun a_1 =>
      Mathlib.Tactic.Linarith.lt_irrefl
        (Eq.mp
          (congrArg (fun _a => _a < 0)
            (Mathlib.Tactic.Ring.of_eq
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.add_congr
                  (Mathlib.Tactic.Ring.neg_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.neg_zero))
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑a.digits.length)
                      (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                      (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑a.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1)))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                        (Mathlib.Meta.NormNum.IsInt.to_isNat
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0))))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑a.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                  (Mathlib.Tactic.Ring.add_pf_add_lt (Int.negOfNat 1).rawCast
                    (Mathlib.Tactic.Ring.add_pf_zero_add (↑a.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                (Mathlib.Tactic.Ring.sub_congr
                  (Mathlib.Tactic.Ring.add_congr
                    (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.add_pf_zero_add (Nat.rawCast 1 + 0)))
                  (Mathlib.Tactic.Ring.atom_pf ↑a.digits.length)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul (↑a.digits.length) (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 1)
                      (Mathlib.Tactic.Ring.add_pf_zero_add
                        (↑a.digits.length ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                      (Eq.refl (Int.ofNat 0))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑a.digits.length) (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
              (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
          (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
            (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
              (Mathlib.Tactic.Linarith.sub_nonpos_of_le
                (Int.add_one_le_iff.mpr
                  (id
                    (Eq.mp
                      (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 a.digits.length 1)
                        (congrArg (LT.lt ↑a.digits.length) Nat.cast_one))
                      a_1)))))
            (Mathlib.Tactic.Linarith.sub_nonpos_of_le
              (Int.add_one_le_iff.mpr
                (id
                  (Eq.mp
                    (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 0 a.digits.length)
                      (congrFun' (congrArg LT.lt Nat.cast_zero) ↑a.digits.length))
                    (length_pos a))))))))
    (Not.intro fun a_1 =>
      Mathlib.Tactic.Linarith.lt_irrefl
        (Eq.mp
          (congrArg (fun _a => _a < 0)
            (Mathlib.Tactic.Ring.of_eq
              (Mathlib.Tactic.Ring.add_congr
                (Mathlib.Tactic.Ring.add_congr
                  (Mathlib.Tactic.Ring.neg_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_one_mul
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Eq.refl (Int.negOfNat 1)))))
                      Mathlib.Tactic.Ring.neg_zero))
                  (Mathlib.Tactic.Ring.sub_congr
                    (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf ↑a.digits.length)
                      (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                      (Mathlib.Tactic.Ring.add_pf_add_gt (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑a.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 2)))
                    (Mathlib.Tactic.Ring.sub_pf
                      (Mathlib.Tactic.Ring.neg_add
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2))
                              (Eq.refl (Int.negOfNat 2)))))
                        Mathlib.Tactic.Ring.neg_zero)
                      (Mathlib.Tactic.Ring.add_pf_add_overlap
                        (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                          (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                            (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                            (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2)) (Eq.refl (Int.negOfNat 1))))
                        (Mathlib.Tactic.Ring.add_pf_add_zero (↑a.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap
                    (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                      (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                        (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.negOfNat 2))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add (↑a.digits.length ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
                (Mathlib.Tactic.Ring.sub_congr
                  (Mathlib.Tactic.Ring.add_congr
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 1)))
                    (Mathlib.Tactic.Ring.add_pf_add_overlap
                      (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                        (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1)
                          (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1) (Eq.refl 2)))
                      (Mathlib.Tactic.Ring.add_pf_zero_add 0)))
                  (Mathlib.Tactic.Ring.atom_pf ↑a.digits.length)
                  (Mathlib.Tactic.Ring.sub_pf
                    (Mathlib.Tactic.Ring.neg_add
                      (Mathlib.Tactic.Ring.neg_mul (↑a.digits.length) (Nat.rawCast 1)
                        (Mathlib.Tactic.Ring.neg_one_mul
                          (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                            (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                              (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1))
                              (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                              (Eq.refl (Int.negOfNat 1))))))
                      Mathlib.Tactic.Ring.neg_zero)
                    (Mathlib.Tactic.Ring.add_pf_add_lt (Nat.rawCast 2)
                      (Mathlib.Tactic.Ring.add_pf_zero_add
                        (↑a.digits.length ^ Nat.rawCast 1 * (Int.negOfNat 1).rawCast + 0)))))
                (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                  (Mathlib.Meta.NormNum.IsInt.to_isNat
                    (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                      (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 2))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 2))
                      (Eq.refl (Int.ofNat 0))))
                  (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
                    (Mathlib.Tactic.Ring.add_overlap_pf_zero (↑a.digits.length) (Nat.rawCast 1)
                      (Mathlib.Meta.NormNum.IsInt.to_isNat
                        (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                          (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw ℤ 1))
                          (Mathlib.Meta.NormNum.IsInt.of_raw ℤ (Int.negOfNat 1)) (Eq.refl (Int.ofNat 0)))))
                    (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
              (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat ℤ (Eq.refl 0)))))
          (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le
            (Mathlib.Tactic.Linarith.add_lt_of_neg_of_le (neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one)
              (Mathlib.Tactic.Linarith.sub_nonpos_of_le
                (Int.add_one_le_iff.mpr
                  (id (Eq.mp (Mathlib.Tactic.Zify.natCast_lt._simp_1 a.digits.length 2) _fvar.154273)))))
            (Mathlib.Tactic.Linarith.sub_nonpos_of_le
              (Int.add_one_le_iff.mpr
                (id
                  (Eq.mp
                    (Eq.trans (Mathlib.Tactic.Zify.natCast_lt._simp_1 1 a.digits.length)
                      (congrFun' (congrArg LT.lt Nat.cast_one) ↑a.digits.length))
                    a_1)))))))_subsing:Subsingleton (Fin a.digits.length) := 
  of_eq_true
    (Eq.trans (Eq.trans (congrArg Subsingleton (congrArg Fin hal)) exists_unique._simp_1) (Std.le_refl._simp_1 1))zero:Fin a.digits.length := ⟨0, ⋯⟩ha:↑a.digits[0] = m + 1this:↑a.digits[0] < 10⊢ a = b.append (Digit.mk hr)
    linarithAll goals completed! 🐙
  obtain ⟨ b', b'₀, rfl ⟩ := eq_append halhi.inr.h₂.inrm:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 mb:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = bb':PosintDecimalb'₀:Digitha:↑(b'.append b'₀) = m + 1hal:2 ≤ (b'.append b'₀).digits.length⊢ b'.append b'₀ = b.append (Digit.mk hr)
  simp [←this] at hahi.inr.h₂.inrm:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 mb:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = bb':PosintDecimalb'₀:Digithal:2 ≤ (b'.append b'₀).digits.lengthha:↑b'₀ + 10 * ↑b' = r + 10 * s⊢ b'.append b'₀ = b.append (Digit.mk hr)
  observe : (b'₀:ℕ) < 10hi.inr.h₂.inrm:ℕa✝:m + 1 > 0hm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this✝:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 mb:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = bb':PosintDecimalb'₀:Digithal:2 ≤ (b'.append b'₀).digits.lengthha:↑b'₀ + 10 * ↑b' = r + 10 * sthis:↑b'₀ < 10⊢ b'.append b'₀ = b.append (Digit.mk hr)
  replace : (s:ℤ) = (b':ℕ) := byn:ℕ⊢ n > 0 → ∃! p, ↑p = n omegaAll goals completed! 🐙
  have hb'₀r: (b'₀:ℕ) = (r:ℤ) := byn:ℕ⊢ n > 0 → ∃! p, ↑p = n omegaAll goals completed! 🐙
  simp at *hi.inr.h₂.inrm:ℕhm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this✝:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 mb:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = bb':PosintDecimalb'₀:Digithal:2 ≤ (b'.append b'₀).digits.lengthha:↑b'₀ + 10 * ↑b' = r + 10 * sa✝:Truethis:s = ↑b'hb'₀r:↑b'₀ = r⊢ b'.append b'₀ = b.append (Digit.mk hr)
  rw [←b'₀.mk_eq_iff hr] at hb'₀rhi.inr.h₂.inrm:ℕhm:9 ≤ ms:ℕ := (m + 1) / 10r:ℕ := (m + 1) % 10this✝:r + 10 * s = m + 1hr:r < 10 := exists_unique._proof_6 mb:PosintDecimalhb:↑b = shuniq:∀ (y : PosintDecimal), ↑y = s → y = bb':PosintDecimalb'₀:Digithal:2 ≤ (b'.append b'₀).digits.lengthha:↑b'₀ + 10 * ↑b' = r + 10 * sa✝:Truethis:s = ↑b'hb'₀r:b'₀ = Digit.mk hr⊢ b'.append b'₀ = b.append (Digit.mk hr)
  rw [huniq b' this.symm, hb'₀r]All goals completed! 🐙

@[simp]
theorem PosintDecimal.coe_inj (p q:PosintDecimal) : (p:ℕ) = (q:ℕ) ↔ p = q := byp:PosintDecimalq:PosintDecimal⊢ ↑p = ↑q ↔ p = q
  constructormpp:PosintDecimalq:PosintDecimal⊢ ↑p = ↑q → p = qmprp:PosintDecimalq:PosintDecimal⊢ p = q → ↑p = ↑q <;>mpp:PosintDecimalq:PosintDecimal⊢ ↑p = ↑q → p = qmprp:PosintDecimalq:PosintDecimal⊢ p = q → ↑p = ↑q intro hmprp:PosintDecimalq:PosintDecimalh:p = q⊢ ↑p = ↑q
  .mpp:PosintDecimalq:PosintDecimalh:↑p = ↑q⊢ p = q exact (exists_unique _ q.pos).unique h rflAll goals completed! 🐙
  rw [h]All goals completed! 🐙

inductive IntDecimal where
  | zero : IntDecimal
  | pos : PosintDecimal → IntDecimal
  | neg : PosintDecimal → IntDecimal

def IntDecimal.toInt : IntDecimal → Int
  | zero => 0
  | pos p => p.toNat
  | neg p => -p.toNat

instance IntDecimal.instCoeInt : Coe IntDecimal Int where
  coe := toInt

example : (IntDecimal.neg (PosintDecimal.mk' 3 [1, 4] (by⊢ 3 ≠ 0 decideAll goals completed! 🐙)):ℤ) = -314 := by⊢ (IntDecimal.neg (PosintDecimal.mk' 3 [1, 4] ⋯)).toInt = -314 decideAll goals completed! 🐙

theorem IntDecimal.Int_bij : Function.Bijective IntDecimal.toInt := by⊢ Function.Bijective toInt
  constructorleft⊢ Function.Injective toIntright⊢ Function.Surjective toInt
  .left⊢ Function.Injective toInt intro p qleftp:IntDecimalq:IntDecimal⊢ p.toInt = q.toInt → p = q hpqleftp:IntDecimalq:IntDecimalhpq:p.toInt = q.toInt⊢ p = q
    cases p with
    | zero =>left.zeroq:IntDecimalhpq:zero.toInt = q.toInt⊢ zero = q cases q with
      | zero =>left.zero.zerohpq:zero.toInt = zero.toInt⊢ zero = zero rflAll goals completed! 🐙
      | pos q =>left.zero.posq:PosintDecimalhpq:zero.toInt = (pos q).toInt⊢ zero = pos q simp [toInt] at hpqleft.zero.posq:PosintDecimalhpq:0 = ↑↑q⊢ zero = pos q; linarith [q.pos]All goals completed! 🐙
      | neg q =>left.zero.negq:PosintDecimalhpq:zero.toInt = (neg q).toInt⊢ zero = neg q simp [toInt] at hpqleft.zero.negq:PosintDecimalhpq:↑q = 0⊢ zero = neg q; linarith [q.pos]All goals completed! 🐙
    | pos p =>left.posq:IntDecimalp:PosintDecimalhpq:(pos p).toInt = q.toInt⊢ pos p = q cases q with
      | zero =>left.pos.zerop:PosintDecimalhpq:(pos p).toInt = zero.toInt⊢ pos p = zero simp [toInt] at hpqleft.pos.zerop:PosintDecimalhpq:↑p = 0⊢ pos p = zero; linarith [p.pos]All goals completed! 🐙
      | pos q =>left.pos.posp:PosintDecimalq:PosintDecimalhpq:(pos p).toInt = (pos q).toInt⊢ pos p = pos q simpa [toInt] using hpqAll goals completed! 🐙
      | neg q =>left.pos.negp:PosintDecimalq:PosintDecimalhpq:(pos p).toInt = (neg q).toInt⊢ pos p = neg q simp [toInt] at hpqleft.pos.negp:PosintDecimalq:PosintDecimalhpq:↑p = 0 ∧ ↑q = 0⊢ pos p = neg q; linarith [q.pos]All goals completed! 🐙
    | neg p =>left.negq:IntDecimalp:PosintDecimalhpq:(neg p).toInt = q.toInt⊢ neg p = q cases q with
      | zero =>left.neg.zerop:PosintDecimalhpq:(neg p).toInt = zero.toInt⊢ neg p = zero simp [toInt] at hpqleft.neg.zerop:PosintDecimalhpq:↑p = 0⊢ neg p = zero; linarith [p.pos]All goals completed! 🐙
      | pos q =>left.neg.posp:PosintDecimalq:PosintDecimalhpq:(neg p).toInt = (pos q).toInt⊢ neg p = pos q simp [toInt] at hpqleft.neg.posp:PosintDecimalq:PosintDecimalhpq:↑p = 0 ∧ ↑q = 0⊢ neg p = pos q; linarith [q.pos]All goals completed! 🐙
      | neg q =>left.neg.negp:PosintDecimalq:PosintDecimalhpq:(neg p).toInt = (neg q).toInt⊢ neg p = neg q simpa [toInt] using hpqAll goals completed! 🐙
  intro nrightn:ℤ⊢ ∃ a, a.toInt = n
  obtain h | rfl | h := lt_trichotomy n 0right.inln:ℤh:n < 0⊢ ∃ a, a.toInt = nright.inr.inl⊢ ∃ a, a.toInt = 0right.inr.inrn:ℤh:0 < n⊢ ∃ a, a.toInt = n
  .right.inln:ℤh:n < 0⊢ ∃ a, a.toInt = n generalize e: -n = mright.inln:ℤh:n < 0m:ℤe:-n = m⊢ ∃ a, a.toInt = n
    lift m to Nat using (byn:ℤh:n < 0m:ℤe:-n = m⊢ 0 ≤ m omegaAll goals completed! 🐙)
    choose p hp _ using PosintDecimal.exists_unique _ (show 0 < m by⊢ Function.Bijective toInt omegaAll goals completed! 🐙)
    use neg phn:ℤh:n < 0m:ℕe:-n = ↑mp:PosintDecimalhp:↑p = ma✝:∀ (y : PosintDecimal), (fun p => ↑p = m) y → y = p⊢ (neg p).toInt = n
    simp [toInt, hp, ←e]All goals completed! 🐙
  .right.inr.inl⊢ ∃ a, a.toInt = 0 use zeroh⊢ zero.toInt = 0; simp [toInt]All goals completed! 🐙
  lift n to Nat using (byn:ℤh:0 < n⊢ 0 ≤ n omegaAll goals completed! 🐙); simp at hright.inr.inrn:ℕh:0 < n⊢ ∃ a, a.toInt = ↑n
  choose p hp _ using PosintDecimal.exists_unique _ hright.inr.inrn:ℕh:0 < np:PosintDecimalhp:↑p = na✝:∀ (y : PosintDecimal), (fun p => ↑p = n) y → y = p⊢ ∃ a, a.toInt = ↑n
  use pos phn:ℕh:0 < np:PosintDecimalhp:↑p = na✝:∀ (y : PosintDecimal), (fun p => ↑p = n) y → y = p⊢ (pos p).toInt = ↑n
  simp [toInt, hp]All goals completed! 🐙

abbrev PosintDecimal.digit (p:PosintDecimal) (i:ℕ) : Digit :=
  if h: i < p.digits.length then p.digits[p.digits.length - i - 1] else 0

abbrev PosintDecimal.carry (p q:PosintDecimal) : ℕ → ℕ := Nat.rec 0 (fun i ε ↦ if ((p.digit i:ℕ) + (q.digit i:ℕ) + ε) < 10 then 0 else 1)

theorem PosintDecimal.carry_zero (p q:PosintDecimal) : p.carry q 0 = 0 := byp:PosintDecimalq:PosintDecimal⊢ p.carry q 0 = 0 convert Nat.rec_zero _ _All goals completed! 🐙

theorem PosintDecimal.carry_succ (p q:PosintDecimal) (i:ℕ) : p.carry q (i+1) = if ((p.digit i:ℕ) + (q.digit i:ℕ) + p.carry q i < 10) then 0 else 1 :=
  Nat.rec_add_one 0 (fun i ε ↦ if ((p.digit i:ℕ) + (q.digit i:ℕ) + ε) < 10 then 0 else 1) i

abbrev PosintDecimal.sum_digit (p q:PosintDecimal) (i:ℕ) : ℕ :=
  if (p.digit i + q.digit i + (p.carry q) i < 10) then
    p.digit i + q.digit i + (p.carry q) i
  else
    p.digit i + q.digit i + (p.carry q) i - 10

Exercise B.1.1

theorem declaration uses `sorry`PosintDecimal.sum_digit_lt (p q:PosintDecimal) (i:ℕ) :
  p.sum_digit q i < 10 := byp:PosintDecimalq:PosintDecimali:ℕ⊢ p.sum_digit q i < 10 sorryAll goals completed! 🐙

Define this number such that it satisfies the two following theorems.

def declaration uses `sorry`PosintDecimal.sum_digit_top (p q:PosintDecimal) : ℕ := byp:PosintDecimalq:PosintDecimal⊢ ℕ sorryAll goals completed! 🐙

theorem declaration uses `sorry`PosintDecimal.leading_nonzero (p q:PosintDecimal) :
    p.sum_digit q (p.sum_digit_top q) ≠ 0 := sorry

theorem declaration uses `sorry`PosintDecimal.out_of_range_eq_zero (p q:PosintDecimal) :
    ∀ i > ↑(p.sum_digit_top q), p.sum_digit q i = 0 := sorry

def declaration uses `sorry`declaration uses `sorry`declaration uses `sorry`PosintDecimal.longAddition (p q : PosintDecimal) : PosintDecimal where
  digits := sorry
  nonempty := sorry
  nonzero := sorry

theorem declaration uses `sorry`PosintDecimal.sum_eq (p q:PosintDecimal) (i:ℕ) :
    (((p.longAddition q).digit i):ℕ) = p.sum_digit q i ∧ (p.longAddition q:ℕ) = p + q := byp:PosintDecimalq:PosintDecimali:ℕ⊢ ↑((p.longAddition q).digit i) = p.sum_digit q i ∧ ↑(p.longAddition q) = ↑p + ↑q sorryAll goals completed! 🐙