theorem String.Slice.toInt?_eq_some_iff {s : Slice} {a : Int} : s.toInt? = some a ↔ (∃ (b : Nat), s.toNat? = some b ∧ a = ↑b) ∨ ∃ (t : String), s.copy = "-" ++ t ∧ ∃ (b : Nat), t.toNat? = some b ∧ a = -↑b

@[simp]

theorem String.Slice.isSome_toInt? {s : Slice} : s.toInt?.isSome = s.isInt

theorem String.Slice.isInt_of_toInt?_eq_some {a : Int} {s : Slice} (h : s.toInt? = some a) : s.isInt = true

@[simp]

theorem String.Slice.toInt?_eq_none_iff {s : Slice} : s.toInt? = none ↔ s.isInt = false

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

theorem String.Slice.isInt_iff {s : Slice} : s.isInt = true ↔ s.isNat = true ∨ ∃ (t : String), s.copy = "-" ++ t ∧ t.isNat = true

theorem String.Slice.isInt_of_isNat {s : Slice} (h : s.isNat = true) : s.isInt = true

theorem String.Slice.toInt?_eq_toNat?_of_startsWith_eq_false {s : Slice} (h : s.startsWith '-' = false) : s.toInt? = Option.map (fun (n : Nat) => ↑n) s.toNat?

theorem String.Slice.toInt?_eq_of_eq_minus_append {s : Slice} {t : String} (h : s.copy = "-" ++ t) : s.toInt? = Option.map (fun (n : Nat) => -↑n) t.toNat?

theorem String.Slice.toInt?_eq_some_of_toNat?_eq_some {s : Slice} {a : Nat} (h : s.toNat? = some a) : s.toInt? = some ↑a

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

theorem String.Slice.isInt_congr {s t : Slice} (h : s.copy = t.copy) : s.isInt = t.isInt

@[simp]

theorem String.isInt_toSlice {s : String} : s.toSlice.isInt = s.isInt

@[simp]

theorem String.isInt_comp_toSlice : Slice.isInt ∘ toSlice = isInt

@[simp]

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

@[simp]

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

@[simp]

theorem String.Slice.isInt_copy {s : Slice} : s.copy.isInt = s.isInt

@[simp]

theorem String.Slice.isInt_comp_copy : String.isInt ∘ copy = isInt

@[simp]

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

@[simp]

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

theorem String.toInt?_eq_some_iff {s : String} {a : Int} : s.toInt? = some a ↔ (∃ (b : Nat), s.toNat? = some b ∧ a = ↑b) ∨ ∃ (t : String), s = "-" ++ t ∧ ∃ (b : Nat), t.toNat? = some b ∧ a = -↑b

@[simp]

theorem String.isSome_toInt? {s : String} : s.toInt?.isSome = s.isInt

theorem String.isInt_of_toInt?_eq_some {a : Int} {s : String} (h : s.toInt? = some a) : s.isInt = true

@[simp]

theorem String.toInt?_eq_none_iff {s : String} : s.toInt? = none ↔ s.isInt = false

theorem String.toInt?_eq_none {s : String} (h : s.isInt = false) : s.toInt? = none

theorem String.isInt_iff {s : String} : s.isInt = true ↔ s.isNat = true ∨ ∃ (t : String), s = "-" ++ t ∧ t.isNat = true

theorem String.isInt_of_isNat {s : String} (h : s.isNat = true) : s.isInt = true

theorem String.toInt?_eq_toNat?_of_startsWith_eq_false {s : String} (h : s.startsWith '-' = false) : s.toInt? = Option.map (fun (a : Nat) => ↑a) s.toNat?

@[simp]

theorem String.toInt?_minus_append {s : String} : ("-" ++ s).toInt? = Option.map (fun (n : Nat) => -↑n) s.toNat?

theorem String.toInt?_eq_some_of_toNat?_eq_some {s : String} {a : Nat} (h : s.toNat? = some a) : s.toInt? = some ↑a

@[simp]

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

@[simp]

theorem Nat.isInt_repr (n : Nat) : n.repr.isInt = true

@[simp]

theorem Int.toInt?_repr (a : Int) : a.repr.toInt? = some a

@[simp]

theorem Int.isInt_repr (a : Int) : a.repr.isInt = true

theorem Int.repr_injective {a b : Int} (h : a.repr = b.repr) : a = b

@[simp]

theorem Int.repr_inj {a b : Int} : a.repr = b.repr ↔ a = b