Theorem: Nat.toDigitsCore_shift' (One.lean)

State before:
b n : ℕ
P : b > 1
⊢ ∀ (i : ℕ),
    List.getD (List.reverse (toDigits b n)) (i + 1) (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Tactic:
intro i
State after:
b n : ℕ
P : b > 1
i : ℕ
⊢ List.getD (List.reverse (toDigits b n)) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)

State before:
b n : ℕ
P : b > 1
i : ℕ
⊢ List.getD (List.reverse (toDigits b n)) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Tactic:
rw [toDigits, toDigitsCore]
State after:
b n : ℕ
P : b > 1
i : ℕ
⊢ List.getD
      (List.reverse
        (let d := digitChar (n % b);
        let n' := n / b;
        if n' = 0 then [d] else toDigitsCore b n n' [d]))
      (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)

State before:
b n : ℕ
P : b > 1
i : ℕ
⊢ List.getD
      (List.reverse
        (let d := digitChar (n % b);
        let n' := n / b;
        if n' = 0 then [d] else toDigitsCore b n n' [d]))
      (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Tactic:
simp only [add_eq, add_zero]
State after:
b n : ℕ
P : b > 1
i : ℕ
⊢ List.getD (List.reverse (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b n (n / b) [digitChar (n % b)]))
      (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)

State before:
b n : ℕ
P : b > 1
i : ℕ
⊢ List.getD (List.reverse (if n / b = 0 then [digitChar (n % b)] else toDigitsCore b n (n / b) [digitChar (n % b)]))
      (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Tactic:
split
State after:
case inl
b n : ℕ
P : b > 1
i : ℕ
h✝ : n / b = 0
⊢ List.getD (List.reverse [digitChar (n % b)]) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)

case inr
b n : ℕ
P : b > 1
i : ℕ
h✝ : ¬n / b = 0
⊢ List.getD (List.reverse (toDigitsCore b n (n / b) [digitChar (n % b)])) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)

State before:
case inl
b n : ℕ
P : b > 1
i : ℕ
h✝ : n / b = 0
⊢ List.getD (List.reverse [digitChar (n % b)]) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)

case inr
b n : ℕ
P : b > 1
i : ℕ
h✝ : ¬n / b = 0
⊢ List.getD (List.reverse (toDigitsCore b n (n / b) [digitChar (n % b)])) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Tactic:
. next heq =>
  conv => left; unfold List.getD
  simp only [List.get?, Option.getD_none]
  rw [heq]
  unfold toDigits toDigitsCore digitChar
  simp only [Nat.zero_div, zero_mod, zero_ne_one, ite_false, ite_true, List.reverse_cons, List.reverse_nil,
List.nil_append, List.getD_singleton_default_eq]
State after:
case inr
b n : ℕ
P : b > 1
i : ℕ
h✝ : ¬n / b = 0
⊢ List.getD (List.reverse (toDigitsCore b n (n / b) [digitChar (n % b)])) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)

State before:
case inr
b n : ℕ
P : b > 1
i : ℕ
h✝ : ¬n / b = 0
⊢ List.getD (List.reverse (toDigitsCore b n (n / b) [digitChar (n % b)])) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Tactic:
. next heq =>
  rw [Nat.todigitsCore_accumulates_suffix]
  rw [List.getD, List.getD]
  congr 1
  simp only [List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append, List.singleton_append,
    List.cons.injEq, succ.injEq, and_imp, forall_apply_eq_imp_iff₂, forall_apply_eq_imp_iff', forall_eq', 
    List.get?, add_eq, add_zero]
  rw [Nat.toDigitsCore_fuel_irrelevant, ← Nat.toDigits]
  . simp only [ge_iff_le]
    have h: n ≠ 0 := by 
      simp only [ne_eq]
      intro h
      rw [h] at heq
      simp only [Nat.zero_div] at heq
    apply Nat.div_lt_self
    . simp only [ne_eq, h, not_false_iff, Nat.pos_of_ne_zero]
    . exact P
  . exact P
State after:
no goals

State before:
b n : ℕ
P : b > 1
i : ℕ
heq : n / b = 0
⊢ List.getD (List.reverse [digitChar (n % b)]) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Tactic:
conv => left; unfold List.getD
State after:
b n : ℕ
P : b > 1
i : ℕ
heq : n / b = 0
⊢ Option.getD (List.get? (List.reverse [digitChar (n % b)]) (i + 1)) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)

State before:
b n : ℕ
P : b > 1
i : ℕ
heq : n / b = 0
⊢ Option.getD (List.get? (List.reverse [digitChar (n % b)]) (i + 1)) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Tactic:
simp only [List.get?, Option.getD_none]
State after:
b n : ℕ
P : b > 1
i : ℕ
heq : n / b = 0
⊢ Char.ofNat 48 = List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)

State before:
b n : ℕ
P : b > 1
i : ℕ
heq : n / b = 0
⊢ Char.ofNat 48 = List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Tactic:
rw [heq]
State after:
b n : ℕ
P : b > 1
i : ℕ
heq : n / b = 0
⊢ Char.ofNat 48 = List.getD (List.reverse (toDigits b 0)) i (Char.ofNat 48)

State before:
b n : ℕ
P : b > 1
i : ℕ
heq : n / b = 0
⊢ Char.ofNat 48 = List.getD (List.reverse (toDigits b 0)) i (Char.ofNat 48)
Tactic:
unfold toDigits toDigitsCore digitChar
State after:
b n : ℕ
P : b > 1
i : ℕ
heq : n / b = 0
⊢ Char.ofNat 48 =
    List.getD
      (List.reverse
        (let d :=
          if 0 % b = 0 then Char.ofNat 48
          else
            if 0 % b = 1 then Char.ofNat 49
            else
              if 0 % b = 2 then Char.ofNat 50
              else
                if 0 % b = 3 then Char.ofNat 51
                else
                  if 0 % b = 4 then Char.ofNat 52
                  else
                    if 0 % b = 5 then Char.ofNat 53
                    else
                      if 0 % b = 6 then Char.ofNat 54
                      else
                        if 0 % b = 7 then Char.ofNat 55
                        else
                          if 0 % b = 8 then Char.ofNat 56
                          else
                            if 0 % b = 9 then Char.ofNat 57
                            else
                              if 0 % b = 10 then Char.ofNat 97
                              else
                                if 0 % b = 11 then Char.ofNat 98
                                else
                                  if 0 % b = 12 then Char.ofNat 99
                                  else
                                    if 0 % b = 13 then Char.ofNat 100
                                    else
                                      if 0 % b = 14 then Char.ofNat 101
                                      else if 0 % b = 15 then Char.ofNat 102 else Char.ofNat 42;
        let n' := 0 / b;
        if n' = 0 then [d] else toDigitsCore b 0 n' [d]))
      i (Char.ofNat 48)

State before:
b n : ℕ
P : b > 1
i : ℕ
heq : n / b = 0
⊢ Char.ofNat 48 =
    List.getD
      (List.reverse
        (let d :=
          if 0 % b = 0 then Char.ofNat 48
          else
            if 0 % b = 1 then Char.ofNat 49
            else
              if 0 % b = 2 then Char.ofNat 50
              else
                if 0 % b = 3 then Char.ofNat 51
                else
                  if 0 % b = 4 then Char.ofNat 52
                  else
                    if 0 % b = 5 then Char.ofNat 53
                    else
                      if 0 % b = 6 then Char.ofNat 54
                      else
                        if 0 % b = 7 then Char.ofNat 55
                        else
                          if 0 % b = 8 then Char.ofNat 56
                          else
                            if 0 % b = 9 then Char.ofNat 57
                            else
                              if 0 % b = 10 then Char.ofNat 97
                              else
                                if 0 % b = 11 then Char.ofNat 98
                                else
                                  if 0 % b = 12 then Char.ofNat 99
                                  else
                                    if 0 % b = 13 then Char.ofNat 100
                                    else
                                      if 0 % b = 14 then Char.ofNat 101
                                      else if 0 % b = 15 then Char.ofNat 102 else Char.ofNat 42;
        let n' := 0 / b;
        if n' = 0 then [d] else toDigitsCore b 0 n' [d]))
      i (Char.ofNat 48)
Tactic:
simp only [Nat.zero_div, zero_mod, zero_ne_one, ite_false, ite_true, List.reverse_cons, List.reverse_nil,
List.nil_append, List.getD_singleton_default_eq]
State after:
no goals

State before:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ List.getD (List.reverse (toDigitsCore b n (n / b) [digitChar (n % b)])) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Tactic:
rw [Nat.todigitsCore_accumulates_suffix]
State after:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ List.getD (List.reverse (toDigitsCore b n (n / b) [] ++ [digitChar (n % b)])) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)

State before:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ List.getD (List.reverse (toDigitsCore b n (n / b) [] ++ [digitChar (n % b)])) (i + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) i (Char.ofNat 48)
Tactic:
rw [List.getD, List.getD]
State after:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ Option.getD (List.get? (List.reverse (toDigitsCore b n (n / b) [] ++ [digitChar (n % b)])) (i + 1)) (Char.ofNat 48) =
    Option.getD (List.get? (List.reverse (toDigits b (n / b))) i) (Char.ofNat 48)

State before:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ Option.getD (List.get? (List.reverse (toDigitsCore b n (n / b) [] ++ [digitChar (n % b)])) (i + 1)) (Char.ofNat 48) =
    Option.getD (List.get? (List.reverse (toDigits b (n / b))) i) (Char.ofNat 48)
Tactic:
congr 1
State after:
case e_a
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ List.get? (List.reverse (toDigitsCore b n (n / b) [] ++ [digitChar (n % b)])) (i + 1) =
    List.get? (List.reverse (toDigits b (n / b))) i

State before:
case e_a
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ List.get? (List.reverse (toDigitsCore b n (n / b) [] ++ [digitChar (n % b)])) (i + 1) =
    List.get? (List.reverse (toDigits b (n / b))) i
Tactic:
simp only [List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append, List.singleton_append,
  List.cons.injEq, succ.injEq, and_imp, forall_apply_eq_imp_iff₂, forall_apply_eq_imp_iff', forall_eq', 
  List.get?, add_eq, add_zero]
State after:
case e_a
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ List.get? (List.reverse (toDigitsCore b n (n / b) [])) i = List.get? (List.reverse (toDigits b (n / b))) i

State before:
case e_a
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ List.get? (List.reverse (toDigitsCore b n (n / b) [])) i = List.get? (List.reverse (toDigits b (n / b))) i
Tactic:
rw [Nat.toDigitsCore_fuel_irrelevant, ← Nat.toDigits]
State after:
case e_a.P
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ n ≥ n / b + 1

case e_a.Q
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ b > 1

State before:
case e_a.P
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ n ≥ n / b + 1

case e_a.Q
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ b > 1
Tactic:
. simp only [ge_iff_le]
  have h: n ≠ 0 := by 
    simp only [ne_eq]
    intro h
    rw [h] at heq
    simp only [Nat.zero_div] at heq
  apply Nat.div_lt_self
  . simp only [ne_eq, h, not_false_iff, Nat.pos_of_ne_zero]
  . exact P
State after:
case e_a.Q
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ b > 1

State before:
case e_a.Q
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ b > 1
Tactic:
. exact P
State after:
no goals

State before:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ n ≠ 0
Tactic:
simp only [ne_eq]
State after:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ ¬n = 0

State before:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
⊢ ¬n = 0
Tactic:
intro h
State after:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
h : n = 0
⊢ False

State before:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b = 0
h : n = 0
⊢ False
Tactic:
rw [h] at heq
State after:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬0 / b = 0
h : n = 0
⊢ False

State before:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬0 / b = 0
h : n = 0
⊢ False
Tactic:
simp only [Nat.zero_div] at heq
State after:
no goals