Theorem: String.toNatΔ_inv_NattoDigits (One.lean)

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
State after:
no goals

State before:
case h
n : ℕ
ih : ∀ (m : ℕ), m < n → toNatΔ (Nat.toDigits 10 m) = m
⊢ toNatΔ (Nat.toDigits 10 n) = n
Tactic:
cases n
State after:
case h.zero
ih : ∀ (m : ℕ), m < Nat.zero → toNatΔ (Nat.toDigits 10 m) = m
⊢ toNatΔ (Nat.toDigits 10 Nat.zero) = Nat.zero

case h.succ
n✝ : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n✝ → toNatΔ (Nat.toDigits 10 m) = m
⊢ toNatΔ (Nat.toDigits 10 (Nat.succ n✝)) = Nat.succ n✝

State before:
ih : ∀ (m : ℕ), m < Nat.zero → toNatΔ (Nat.toDigits 10 m) = m
⊢ toNatΔ (Nat.toDigits 10 Nat.zero) = Nat.zero
Tactic:
case zero => decide
State after:
no goals

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
State after:
no goals

State before:
ih : ∀ (m : ℕ), m < Nat.zero → toNatΔ (Nat.toDigits 10 m) = m
⊢ toNatΔ (Nat.toDigits 10 Nat.zero) = Nat.zero
Tactic:
decide
State after:
no goals

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:
unfold toNatΔ toNatAux
State after:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
⊢ (match Nat.toDigits 10 (Nat.succ n) with
    | [] => 0
    | head :: tail => toNatAux tail (0 * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48)))) =
    Nat.succ n

State before:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
⊢ (match Nat.toDigits 10 (Nat.succ n) with
    | [] => 0
    | head :: tail => toNatAux tail (0 * 10 + (Char.toNat head - Char.toNat (Char.ofNat 48)))) =
    Nat.succ n
Tactic:
simp only [zero_le, ge_iff_le, nonpos_iff_eq_zero, zero_mul, tsub_le_iff_right, zero_add]
State after:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
⊢ (match Nat.toDigits 10 (Nat.succ n) with
    | [] => 0
    | head :: tail => toNatAux tail (Char.toNat head - Char.toNat (Char.ofNat 48))) =
    Nat.succ n

State before:
n : ℕ
ih : ∀ (m : ℕ), m < Nat.succ n → toNatΔ (Nat.toDigits 10 m) = m
⊢ (match Nat.toDigits 10 (Nat.succ n) with
    | [] => 0
    | head :: tail => toNatAux tail (Char.toNat head - Char.toNat (Char.ofNat 48))) =
    Nat.succ n
Tactic:
split
State after:
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

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
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

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
State after:
no goals

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
State after:
no goals

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]
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

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
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

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
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

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Δ]
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

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]
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

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)
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

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]
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

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
State after:
no goals

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]
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))

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]
State after:
no goals

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
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

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?]
State after:
no goals

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]
State after:
no goals

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
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

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
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

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
State after:
no goals

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
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

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]
State after:
no goals