theorem String.Slice.isNat_iff {s : Slice} : s.isNat = true ↔ s.isEmpty = false ∧ (∀ (c : Char), c ∈ s.copy.toList → c.isDigit = true ∨ c = '_') ∧ ¬['_', '_'] <:+: s.copy.toList ∧ s.copy.toList.head? ≠ some '_' ∧ s.copy.toList.getLast? ≠ some '_'

theorem String.Slice.isNat_of_isDigit {s : Slice} (hne : s.isEmpty = false) (hdigit : ∀ (c : Char), c ∈ s.copy.toList → c.isDigit = true) : s.isNat = true

@[simp]

theorem String.Slice.isSome_toNat? {s : Slice} : s.toNat?.isSome = s.isNat

theorem String.Slice.isNat_of_toNat?_eq_some {n : Nat} {s : Slice} (h : s.toNat? = some n) : s.isNat = true

@[simp]

theorem String.Slice.toNat?_eq_none_iff {s : Slice} : s.toNat? = none ↔ s.isNat = false

theorem String.Slice.toNat?_eq_none {s : Slice} (h : s.isNat = false) : s.toNat? = none

theorem String.Slice.toNat?_eq_some_ofDigitChars {s : Slice} (h : s.isNat = true) : s.toNat? = some (Nat.ofDigitChars 10 (List.filter (fun (x : Char) => x != '_') s.copy.toList) 0)

theorem String.Slice.isNat_congr {s t : Slice} (h : s.copy = t.copy) : s.isNat = t.isNat

theorem String.Slice.toNat?_congr {s t : Slice} (h : s.copy = t.copy) : s.toNat? = t.toNat?

@[simp]

theorem String.isNat_toSlice {s : String} : s.toSlice.isNat = s.isNat

@[simp]

theorem String.isNat_comp_toSlice : Slice.isNat ∘ toSlice = isNat

@[simp]

theorem String.toNat?_toSlice {s : String} : s.toSlice.toNat? = s.toNat?

@[simp]

theorem String.toNat?_comp_toSlice : Slice.toNat? ∘ toSlice = toNat?

@[simp]

theorem String.Slice.isNat_copy {s : Slice} : s.copy.isNat = s.isNat

@[simp]

theorem String.Slice.isNat_comp_copy : String.isNat ∘ copy = isNat

@[simp]

theorem String.Slice.toNat?_copy {s : Slice} : s.copy.toNat? = s.toNat?

@[simp]

theorem String.Slice.toNat?_comp_copy : String.toNat? ∘ copy = toNat?

theorem String.isNat_iff {s : String} : s.isNat = true ↔ s ≠ "" ∧ (∀ (c : Char), c ∈ s.toList → c.isDigit = true ∨ c = '_') ∧ ¬['_', '_'] <:+: s.toList ∧ s.toList.head? ≠ some '_' ∧ s.toList.getLast? ≠ some '_'

theorem String.isNat_of_isDigit {s : String} (hne : s ≠ "") (hdigit : ∀ (c : Char), c ∈ s.toList → c.isDigit = true) : s.isNat = true

@[simp]

theorem String.isSome_toNat? {s : String} : s.toNat?.isSome = s.isNat

theorem String.isNat_of_toNat?_eq_some {n : Nat} {s : String} (h : s.toNat? = some n) : s.isNat = true

@[simp]

theorem String.toNat?_eq_none_iff {s : String} : s.toNat? = none ↔ s.isNat = false

theorem String.toNat?_eq_none {s : String} (h : s.isNat = false) : s.toNat? = none

theorem String.toNat?_eq_some_ofDigitChars {s : String} (h : s.isNat = true) : s.toNat? = some (Nat.ofDigitChars 10 (List.filter (fun (x : Char) => x != '_') s.toList) 0)

theorem String.isNat_append_underscore_append {s t : String} (hs : s.isNat = true) (ht : t.isNat = true) : (s ++ "_" ++ t).isNat = true

theorem String.toNat?_append_underscore_append_eq_some {s t : String} {n m : Nat} (hs : s.toNat? = some n) (ht : t.toNat? = some m) : (s ++ "_" ++ t).toNat? = some (10 ^ (List.filter (fun (x : Char) => x != '_') t.toList).length * n + m)

@[simp]

theorem Nat.isNat_repr (n : Nat) : n.repr.isNat = true

@[simp]

theorem Nat.toNat?_repr (n : Nat) : n.repr.toNat? = some n

theorem Nat.repr_injective {m n : Nat} (h : m.repr = n.repr) : m = n

@[simp]

theorem Nat.repr_inj {m n : Nat} : m.repr = n.repr ↔ m = n