internlm/Lean-Github huggingface dataset:
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
case h_1
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s✝ : List Char
heq✝ : Nat.toDigits 10 (Nat.succ n) = []
⊢ 0 = Nat.succ n

case h_2
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s✝ : List Char
head✝ : Char
tail✝ : List Char
heq✝ : Nat.toDigits 10 (Nat.succ n) = head✝ :: tail✝
⊢ toNatAux tail✝ (Char.toNat head✝ - Char.toNat (Char.ofNat 48)) = Nat.succ n
Tactic:
. next heq => simp only [Nat.toDigits_ne_nil] at heq
Proof state after:
case h_2
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s✝ : List Char
head✝ : Char
tail✝ : List Char
heq✝ : Nat.toDigits 10 (Nat.succ n) = head✝ :: tail✝
⊢ toNatAux tail✝ (Char.toNat head✝ - Char.toNat (Char.ofNat 48)) = Nat.succ n
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s✝ : List Char
heq : Nat.toDigits 10 (Nat.succ n) = []
⊢ 0 = Nat.succ n
Tactic:
simp only [Nat.toDigits_ne_nil] at heq
Proof state after:
no goals
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
⊢ toNatAux tl (Char.toNat hd - Char.toNat (Char.ofNat 48)) = Nat.succ n
Tactic:
have h: tl = List.lastN (List.length (Nat.toDigits 10 (Nat.succ n))  - 1) (Nat.toDigits 10 (Nat.succ n)) := by
  simp only [tsub_le_iff_right, ge_iff_le, List.lastN_eq_tail]
  simp only [heq, List.tail_cons]
Proof state after:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : tl = List.lastN (List.length (Nat.toDigits 10 (Nat.succ n)) - 1) (Nat.toDigits 10 (Nat.succ n))
⊢ toNatAux tl (Char.toNat hd - Char.toNat (Char.ofNat 48)) = Nat.succ n
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : tl = List.lastN (List.length (Nat.toDigits 10 (Nat.succ n)) - 1) (Nat.toDigits 10 (Nat.succ n))
⊢ toNatAux tl (Char.toNat hd - Char.toNat (Char.ofNat 48)) = Nat.succ n
Tactic:
apply_fun String.toNatΔ at h
Proof state after:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (List.lastN (List.length (Nat.toDigits 10 (Nat.succ n)) - 1) (Nat.toDigits 10 (Nat.succ n)))
⊢ toNatAux tl (Char.toNat hd - Char.toNat (Char.ofNat 48)) = Nat.succ n
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (List.lastN (List.length (Nat.toDigits 10 (Nat.succ n)) - 1) (Nat.toDigits 10 (Nat.succ n)))
⊢ toNatAux tl (Char.toNat hd - Char.toNat (Char.ofNat 48)) = Nat.succ n
Tactic:
rw [String.toNatΔ_inv_NattoDigits_tail] at h
Proof state after:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (Nat.toDigits 10 (Nat.succ n % 10 ^ (List.length (Nat.toDigits 10 (Nat.succ n)) - 1)))
⊢ toNatAux tl (Char.toNat hd - Char.toNat (Char.ofNat 48)) = Nat.succ n

case Q
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (List.lastN (List.length (Nat.toDigits 10 (Nat.succ n)) - 1) (Nat.toDigits 10 (Nat.succ n)))
⊢ 10 > 1
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (Nat.toDigits 10 (Nat.succ n % 10 ^ (List.length (Nat.toDigits 10 (Nat.succ n)) - 1)))
⊢ toNatAux tl (Char.toNat hd - Char.toNat (Char.ofNat 48)) = Nat.succ n

case Q
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (List.lastN (List.length (Nat.toDigits 10 (Nat.succ n)) - 1) (Nat.toDigits 10 (Nat.succ n)))
⊢ 10 > 1
Tactic:
rw [String.toNatAux_accumulates, ← String.toNatΔ]
Proof state after:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (Nat.toDigits 10 (Nat.succ n % 10 ^ (List.length (Nat.toDigits 10 (Nat.succ n)) - 1)))
⊢ toNatΔ tl + (Char.toNat hd - Char.toNat (Char.ofNat 48)) * 10 ^ List.length tl = Nat.succ n

case Q
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (List.lastN (List.length (Nat.toDigits 10 (Nat.succ n)) - 1) (Nat.toDigits 10 (Nat.succ n)))
⊢ 10 > 1
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (Nat.toDigits 10 (Nat.succ n % 10 ^ (List.length (Nat.toDigits 10 (Nat.succ n)) - 1)))
⊢ toNatΔ tl + (Char.toNat hd - Char.toNat (Char.ofNat 48)) * 10 ^ List.length tl = Nat.succ n

case Q
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (List.lastN (List.length (Nat.toDigits 10 (Nat.succ n)) - 1) (Nat.toDigits 10 (Nat.succ n)))
⊢ 10 > 1
Tactic:
rw [h, ih]
Proof state after:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (Nat.toDigits 10 (Nat.succ n % 10 ^ (List.length (Nat.toDigits 10 (Nat.succ n)) - 1)))
⊢ Nat.succ n % 10 ^ (List.length (Nat.toDigits 10 (Nat.succ n)) - 1) +
      (Char.toNat hd - Char.toNat (Char.ofNat 48)) * 10 ^ List.length tl =
    Nat.succ n

case a
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (Nat.toDigits 10 (Nat.succ n % 10 ^ (List.length (Nat.toDigits 10 (Nat.succ n)) - 1)))
⊢ Nat.succ n % 10 ^ (List.length (Nat.toDigits 10 (Nat.succ n)) - 1) < Nat.succ n

case Q
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (List.lastN (List.length (Nat.toDigits 10 (Nat.succ n)) - 1) (Nat.toDigits 10 (Nat.succ n)))
⊢ 10 > 1
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
case a
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (Nat.toDigits 10 (Nat.succ n % 10 ^ (List.length (Nat.toDigits 10 (Nat.succ n)) - 1)))
⊢ Nat.succ n % 10 ^ (List.length (Nat.toDigits 10 (Nat.succ n)) - 1) < Nat.succ n

case Q
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (List.lastN (List.length (Nat.toDigits 10 (Nat.succ n)) - 1) (Nat.toDigits 10 (Nat.succ n)))
⊢ 10 > 1
Tactic:
. simp only [gt_iff_lt, Nat.toDigits_length_eq_log, add_tsub_cancel_right, ge_iff_le, add_le_iff_nonpos_left,
    nonpos_iff_eq_zero, Nat.log_eq_zero_iff, or_false, zero_le]
  
  calc
    (Nat.succ n) % 10 ^ Nat.log 10 (Nat.succ n) < 10 ^ Nat.log 10 (Nat.succ n) :=  by apply Nat.mod_lt; apply Nat.pos_pow_of_pos; simp only
    _ ≤  n + 1  := by apply Nat.pow_log_le_self; simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, Nat.succ_ne_zero, not_false_iff]
Proof state after:
case Q
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (List.lastN (List.length (Nat.toDigits 10 (Nat.succ n)) - 1) (Nat.toDigits 10 (Nat.succ n)))
⊢ 10 > 1
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
case Q
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (List.lastN (List.length (Nat.toDigits 10 (Nat.succ n)) - 1) (Nat.toDigits 10 (Nat.succ n)))
⊢ 10 > 1
Tactic:
. simp only
Proof state after:
no goals
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
⊢ tl = List.lastN (List.length (Nat.toDigits 10 (Nat.succ n)) - 1) (Nat.toDigits 10 (Nat.succ n))
Tactic:
simp only [tsub_le_iff_right, ge_iff_le, List.lastN_eq_tail]
Proof state after:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
⊢ tl = List.tail (Nat.toDigits 10 (Nat.succ n))
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
⊢ tl = List.tail (Nat.toDigits 10 (Nat.succ n))
Tactic:
simp only [heq, List.tail_cons]
Proof state after:
no goals
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (Nat.toDigits 10 (Nat.succ n % 10 ^ (List.length (Nat.toDigits 10 (Nat.succ n)) - 1)))
⊢ List.getD (Nat.toDigits 10 (Nat.succ n)) 0 (Char.ofNat 48) = hd
Tactic:
unfold List.getD
Proof state after:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (Nat.toDigits 10 (Nat.succ n % 10 ^ (List.length (Nat.toDigits 10 (Nat.succ n)) - 1)))
⊢ Option.getD (List.get? (Nat.toDigits 10 (Nat.succ n)) 0) (Char.ofNat 48) = hd
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (Nat.toDigits 10 (Nat.succ n % 10 ^ (List.length (Nat.toDigits 10 (Nat.succ n)) - 1)))
⊢ Option.getD (List.get? (Nat.toDigits 10 (Nat.succ n)) 0) (Char.ofNat 48) = hd
Tactic:
simp only [heq, zero_le, ge_iff_le, nonpos_iff_eq_zero, List.cons.injEq, forall_true_left, and_imp,
  forall_apply_eq_imp_iff', forall_eq', Option.getD_some,  List.get?]
Proof state after:
no goals
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (Nat.toDigits 10 (Nat.succ n % 10 ^ (List.length (Nat.toDigits 10 (Nat.succ n)) - 1)))
h₂ : Nat.digitChar (Nat.digit 10 (Nat.succ n) (List.length (Nat.toDigits 10 (Nat.succ n)) - 1 - 0)) = hd
⊢ List.length tl = List.length (Nat.toDigits 10 (Nat.succ n)) - 1
Tactic:
simp only [heq, List.length_cons, Nat.succ_sub_succ_eq_sub, tsub_zero, ge_iff_le, zero_le, nonpos_iff_eq_zero]
Proof state after:
no goals
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (Nat.toDigits 10 (Nat.succ n % 10 ^ (List.length (Nat.toDigits 10 (Nat.succ n)) - 1)))
⊢ Nat.succ n % 10 ^ Nat.log 10 (Nat.succ n) < 10 ^ Nat.log 10 (Nat.succ n)
Tactic:
apply Nat.mod_lt
Proof state after:
case a
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (Nat.toDigits 10 (Nat.succ n % 10 ^ (List.length (Nat.toDigits 10 (Nat.succ n)) - 1)))
⊢ 10 ^ Nat.log 10 (Nat.succ n) > 0
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
case a
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (Nat.toDigits 10 (Nat.succ n % 10 ^ (List.length (Nat.toDigits 10 (Nat.succ n)) - 1)))
⊢ 10 ^ Nat.log 10 (Nat.succ n) > 0
Tactic:
apply Nat.pos_pow_of_pos
Proof state after:
case a.h
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (Nat.toDigits 10 (Nat.succ n % 10 ^ (List.length (Nat.toDigits 10 (Nat.succ n)) - 1)))
⊢ 0 < 10
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
case a.h
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (Nat.toDigits 10 (Nat.succ n % 10 ^ (List.length (Nat.toDigits 10 (Nat.succ n)) - 1)))
⊢ 0 < 10
Tactic:
simp only
Proof state after:
no goals
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (Nat.toDigits 10 (Nat.succ n % 10 ^ (List.length (Nat.toDigits 10 (Nat.succ n)) - 1)))
⊢ 10 ^ Nat.log 10 (Nat.succ n) ≤ n + 1
Tactic:
apply Nat.pow_log_le_self
Proof state after:
case hx
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (Nat.toDigits 10 (Nat.succ n % 10 ^ (List.length (Nat.toDigits 10 (Nat.succ n)) - 1)))
⊢ Nat.succ n ≠ 0
Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
case hx
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
s : List Char
hd : Char
tl : List Char
heq : Nat.toDigits 10 (Nat.succ n) = hd :: tl
h : toNatΔ tl = toNatΔ (Nat.toDigits 10 (Nat.succ n % 10 ^ (List.length (Nat.toDigits 10 (Nat.succ n)) - 1)))
⊢ Nat.succ n ≠ 0
Tactic:
simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, ne_eq, Nat.succ_ne_zero, not_false_iff]
Proof state after:
no goals
Theorem: String.toIntΔ_inv_IntreprΔ
Proof state before:
i : ℤ
⊢ toIntΔ (Int.reprΔ i) = i
Tactic:
unfold toIntΔ Int.reprΔ
Proof state after:
i : ℤ
⊢ (match
      match i with
      | Int.ofNat m => Nat.toDigits 10 m
      | Int.negSucc m => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m) with
    | [] => 0
    | h :: tail => if h = Char.ofNat 45 then -↑(toNatΔ tail) else ↑(toNatΔ (h :: tail))) =
    i
Theorem: String.toIntΔ_inv_IntreprΔ
Proof state before:
i : ℤ
⊢ (match
      match i with
      | Int.ofNat m => Nat.toDigits 10 m
      | Int.negSucc m => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m) with
    | [] => 0
    | h :: tail => if h = Char.ofNat 45 then -↑(toNatΔ tail) else ↑(toNatΔ (h :: tail))) =
    i
Tactic:
cases i with
| ofNat n =>
  simp only [Int.ofNat_eq_coe]
  split
  case h_1 s heq =>
    simp only [Nat.toDigits_ne_nil
  ] at heq
  case h_2 head tail heq =>
    split
    case inl h =>
      have h₂: (List.all (head::tail) Char.isDigit == true) = true := by
        rw [← heq]
        apply Nat.toDigits_digits <;> decide
      simp at h₂
      have ⟨ h₃, _⟩ :=h₂
      simp only [h] at h₃
    . simp only [← heq, toNatΔ_inv_NattoDigits]
| negSucc n =>
  simp only [List.singleton_append, toNatΔ_inv_NattoDigits, Nat.cast_succ, neg_add_rev, ite_true,
    Int.negSucc_eq]
Proof state after:
no goals
Theorem: String.toIntΔ_inv_IntreprΔ
Proof state before:
case ofNat
n : ℕ
⊢ (match
      match Int.ofNat n with
      | Int.ofNat m => Nat.toDigits 10 m
      | Int.negSucc m => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m) with
    | [] => 0
    | h :: tail => if h = Char.ofNat 45 then -↑(toNatΔ tail) else ↑(toNatΔ (h :: tail))) =
    Int.ofNat n
Tactic:
simp only [Int.ofNat_eq_coe]
Proof state after:
case ofNat
n : ℕ
⊢ (match Nat.toDigits 10 n with
    | [] => 0
    | h :: tail => if h = Char.ofNat 45 then -↑(toNatΔ tail) else ↑(toNatΔ (h :: tail))) =
    ↑n
Theorem: String.toIntΔ_inv_IntreprΔ
Proof state before:
case ofNat
n : ℕ
⊢ (match Nat.toDigits 10 n with
    | [] => 0
    | h :: tail => if h = Char.ofNat 45 then -↑(toNatΔ tail) else ↑(toNatΔ (h :: tail))) =
    ↑n
Tactic:
split
Proof state after:
case ofNat.h_1
n : ℕ
s✝ : List Char
heq✝ : Nat.toDigits 10 n = []
⊢ 0 = ↑n

case ofNat.h_2
n : ℕ
s✝ : List Char
head✝ : Char
tail✝ : List Char
heq✝ : Nat.toDigits 10 n = head✝ :: tail✝
⊢ (if head✝ = Char.ofNat 45 then -↑(toNatΔ tail✝) else ↑(toNatΔ (head✝ :: tail✝))) = ↑n
Theorem: String.toIntΔ_inv_IntreprΔ
Proof state before:
n : ℕ
s : List Char
heq : Nat.toDigits 10 n = []
⊢ 0 = ↑n
Tactic:
case h_1 s heq =>
  simp only [Nat.toDigits_ne_nil
] at heq
Proof state after:
no goals
Theorem: String.toIntΔ_inv_IntreprΔ
Proof state before:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
⊢ (if head = Char.ofNat 45 then -↑(toNatΔ tail) else ↑(toNatΔ (head :: tail))) = ↑n
Tactic:
case h_2 head tail heq =>
  split
  case inl h =>
    have h₂: (List.all (head::tail) Char.isDigit == true) = true := by
      rw [← heq]
      apply Nat.toDigits_digits <;> decide
    simp at h₂
    have ⟨ h₃, _⟩ :=h₂
    simp only [h] at h₃
  . simp only [← heq, toNatΔ_inv_NattoDigits]
Proof state after:
no goals
Theorem: String.toIntΔ_inv_IntreprΔ
Proof state before:
n : ℕ
s : List Char
heq : Nat.toDigits 10 n = []
⊢ 0 = ↑n
Tactic:
simp only [Nat.toDigits_ne_nil
] at heq
Proof state after:
no goals
Theorem: String.toIntΔ_inv_IntreprΔ
Proof state before:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
⊢ (if head = Char.ofNat 45 then -↑(toNatΔ tail) else ↑(toNatΔ (head :: tail))) = ↑n
Tactic:
split
Proof state after:
case inl
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h✝ : head = Char.ofNat 45
⊢ -↑(toNatΔ tail) = ↑n

case inr
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h✝ : ¬head = Char.ofNat 45
⊢ ↑(toNatΔ (head :: tail)) = ↑n
Theorem: String.toIntΔ_inv_IntreprΔ
Proof state before:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h : head = Char.ofNat 45
⊢ -↑(toNatΔ tail) = ↑n
Tactic:
case inl h =>
  have h₂: (List.all (head::tail) Char.isDigit == true) = true := by
    rw [← heq]
    apply Nat.toDigits_digits <;> decide
  simp at h₂
  have ⟨ h₃, _⟩ :=h₂
  simp only [h] at h₃
Proof state after:
no goals
Theorem: String.toIntΔ_inv_IntreprΔ
Proof state before:
case inr
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h✝ : ¬head = Char.ofNat 45
⊢ ↑(toNatΔ (head :: tail)) = ↑n
Tactic:
. simp only [← heq, toNatΔ_inv_NattoDigits]
Proof state after:
no goals
Theorem: String.toIntΔ_inv_IntreprΔ
Proof state before:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h : head = Char.ofNat 45
⊢ -↑(toNatΔ tail) = ↑n
Tactic:
have h₂: (List.all (head::tail) Char.isDigit == true) = true := by
  rw [← heq]
  apply Nat.toDigits_digits <;> decide
Proof state after:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h : head = Char.ofNat 45
h₂ : (List.all (head :: tail) Char.isDigit == true) = true
⊢ -↑(toNatΔ tail) = ↑n
Theorem: String.toIntΔ_inv_IntreprΔ
Proof state before:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h : head = Char.ofNat 45
h₂ : (List.all (head :: tail) Char.isDigit == true) = true
⊢ -↑(toNatΔ tail) = ↑n
Tactic:
simp at h₂
Proof state after:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h : head = Char.ofNat 45
h₂ : Char.isDigit head = true ∧ ∀ (x : Char), x ∈ tail → Char.isDigit x = true
⊢ -↑(toNatΔ tail) = ↑n
Theorem: String.toIntΔ_inv_IntreprΔ
Proof state before:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h : head = Char.ofNat 45
h₂ : Char.isDigit head = true ∧ ∀ (x : Char), x ∈ tail → Char.isDigit x = true
⊢ -↑(toNatΔ tail) = ↑n
Tactic:
have ⟨ h₃, _⟩ :=h₂
Proof state after:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h : head = Char.ofNat 45
h₂ : Char.isDigit head = true ∧ ∀ (x : Char), x ∈ tail → Char.isDigit x = true
h₃ : Char.isDigit head = true
right✝ : ∀ (x : Char), x ∈ tail → Char.isDigit x = true
⊢ -↑(toNatΔ tail) = ↑n
Theorem: String.toIntΔ_inv_IntreprΔ
Proof state before:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h : head = Char.ofNat 45
h₂ : Char.isDigit head = true ∧ ∀ (x : Char), x ∈ tail → Char.isDigit x = true
h₃ : Char.isDigit head = true
right✝ : ∀ (x : Char), x ∈ tail → Char.isDigit x = true
⊢ -↑(toNatΔ tail) = ↑n
Tactic:
simp only [h] at h₃
Proof state after:
no goals
Theorem: String.toIntΔ_inv_IntreprΔ
Proof state before:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h : head = Char.ofNat 45
⊢ (List.all (head :: tail) Char.isDigit == true) = true
Tactic:
rw [← heq]
Proof state after:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h : head = Char.ofNat 45
⊢ (List.all (Nat.toDigits 10 n) Char.isDigit == true) = true
Theorem: String.toIntΔ_inv_IntreprΔ
Proof state before:
n : ℕ
s✝ : List Char
head : Char
tail : List Char
heq : Nat.toDigits 10 n = head :: tail
h : head = Char.ofNat 45
⊢ (List.all (Nat.toDigits 10 n) Char.isDigit == true) = true
Tactic:
apply Nat.toDigits_digits <;> decide
Proof state after:
no goals
Theorem: String.toIntΔ_inv_IntreprΔ
Proof state before:
case negSucc
n : ℕ
⊢ (match
      match Int.negSucc n with
      | Int.ofNat m => Nat.toDigits 10 m
      | Int.negSucc m => [Char.ofNat 45] ++ Nat.toDigits 10 (Nat.succ m) with
    | [] => 0
    | h :: tail => if h = Char.ofNat 45 then -↑(toNatΔ tail) else ↑(toNatΔ (h :: tail))) =
    Int.negSucc n
Tactic:
simp only [List.singleton_append, toNatΔ_inv_NattoDigits, Nat.cast_succ, neg_add_rev, ite_true,
  Int.negSucc_eq]
Proof state after:
no goals
Theorem: List.eq_append_of_getRest
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
l l₁ l₂ : List α
P : getRest l l₁ = some l₂
⊢ l = l₁ ++ l₂
Tactic:
induction l₁ generalizing l l₂ with
| nil =>
  unfold getRest at P
  simp only [Option.some.injEq] at P
  simp only [P, nil_append]
| cons head tail ih =>
  unfold getRest at P
  split at P
  case h_1 heq => simp only at heq
  case h_2 => simp only at P
  case h_3 hd tl y l₁ heq =>
    split at P
    case inr heq₂ => contradiction
    case inl heq₂ =>
      injection heq
      subst hd y l₁
      simp only [cons_append, cons.injEq, true_and]
      apply ih
      apply P
Proof state after:
no goals
Theorem: List.eq_append_of_getRest
Proof state before:
case nil
α : Type u_1
inst✝ : DecidableEq α
l l₂ : List α
P : getRest l [] = some l₂
⊢ l = [] ++ l₂
Tactic:
unfold getRest at P
Proof state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
l l₂ : List α
P :
  (match l, [] with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l₂
⊢ l = [] ++ l₂
Theorem: List.eq_append_of_getRest
Proof state before:
case nil
α : Type u_1
inst✝ : DecidableEq α
l l₂ : List α
P :
  (match l, [] with
    | l, [] => some l
    | [], x => none
    | x :: l, y :: l₁ => if x = y then getRest l l₁ else none) =
    some l₂
⊢ l = [] ++ l₂
Tactic:
simp only [Option.some.injEq] at P
Proof state after:
case nil
α : Type u_1
inst✝ : DecidableEq α
l l₂ : List α
P : l = l₂
⊢ l = [] ++ l₂