Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
n : ℕ
⊢ toNatΔ (Nat.toDigits 10 n) = n
Tactic:
induction n using Nat.strong_induction_on with
| h n ih =>
  cases n
  case zero => decide
  case succ n=>
    unfold toNatΔ toNatAux
    simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, zero_mul, tsub_le_iff_right, zero_add]
    split
    . next heq => simp only [Nat.toDigits_ne_nil] at heq
    . 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