Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
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 s hd tl heq =>
  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]
  apply_fun String.toNatΔ at h
  rw [String.toNatΔ_inv_NattoDigits_tail] at h
  rw [String.toNatAux_accumulates, ← String.toNatΔ]
  rw [h, ih]
  . 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)
      
  . 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]
    
  . simp only
Proof state after:
no goals