Theorem: String.toNatΔ_inv_NattoDigits
Proof state before:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
⊢ toNatΔ (Nat.toDigits 10 (Nat.succ n)) = Nat.succ n
Tactic:
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