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 ^ (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
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, tsub_le_iff_right]
  apply Eq.symm
  rw [Nat.add_comm]
  apply Nat.eq_add_of_sub_eq
  . apply Nat.mod_le
  . conv => left; left; rw [← Nat.mod_add_div (Nat.succ n) (10^Nat.log 10 (Nat.succ n))]
    simp only [add_tsub_cancel_left, ge_iff_le, add_le_iff_nonpos_right, nonpos_iff_eq_zero, mul_eq_zero, zero_le,
      Nat.log_pos_iff, and_true, tsub_le_iff_right]
    have h₂: List.getD (Nat.toDigits 10 (Nat.succ n)) 0 '0' = hd := by
      unfold List.getD
      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?]
    rw [Nat.toDigits_eq_digit] at h₂
    have h₃: List.length tl = List.length (Nat.toDigits 10 (Nat.succ n)) -1 := by
      simp only [heq, List.length_cons, Nat.succ_sub_succ_eq_sub, tsub_zero, ge_iff_le, zero_le, nonpos_iff_eq_zero]
    rw [Nat.toDigits_length_eq_log] at h₃
    rw [← h₂, h₃, Nat.digitChar_sub_zero_eq_self, Nat.toDigits_length_eq_log, Nat.digit, Nat.mul_comm]
    simp only [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, tsub_zero, mul_eq_mul_right_iff, Nat.log_pos_iff, and_true]
    left
    apply Eq.symm (Nat.mod_eq_of_lt _)
    . apply (Nat.div_lt_iff_lt_mul _).2
      . rw [← pow_succ]
        apply Nat.lt_pow_of_log_lt
        . simp only
        . simp only [lt_add_iff_pos_right]
      . simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, gt_iff_lt, pow_pos]
    . simp only
    . simp only [tsub_le_iff_right, ge_iff_le, zero_le, nonpos_iff_eq_zero, tsub_zero, tsub_eq_zero_iff_le,
      gt_iff_lt, Nat.digit_lt_base]
    . simp only
    . simp only
    . apply Nat.pos_of_ne_zero
      intro hp
      apply Nat.toDigits_ne_nil (List.length_eq_zero.1 hp)
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)))
⊢ 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