Theorem: Nat.toDigits_eq_digit_rev (One.lean)

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

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

case P
b n : ℕ
P : b > 1
i : ℕ
⊢ b > 1

State before:
b n : ℕ
P : b > 1
i : ℕ
⊢ List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48) = digitChar (digit b n i)

case P
b n : ℕ
P : b > 1
i : ℕ
⊢ b > 1
Tactic:
. unfold toDigits toDigitsCore digit
  simp only [add_eq, add_zero]
  split
  . next heq =>
    simp only [List.reverse_cons, List.reverse_nil, List.nil_append, List.getD._eq_1, List.get?, Option.getD_some]
  . next heq =>
    rw [Nat.todigitsCore_accumulates_suffix]
    simp only [List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append, List.singleton_append,
List.getD._eq_1, List.get?, Option.getD_some]
State after:
case P
b n : ℕ
P : b > 1
i : ℕ
⊢ b > 1

State before:
case P
b n : ℕ
P : b > 1
i : ℕ
⊢ b > 1
Tactic:
. exact P
State after:
no goals

State before:
b n : ℕ
P : b > 1
i : ℕ
heq : n / b ^ i / b = 0
⊢ List.getD (List.reverse [digitChar (n / b ^ i % b)]) 0 (Char.ofNat 48) = digitChar (n / b ^ i % b)
Tactic:
simp only [List.reverse_cons, List.reverse_nil, List.nil_append, List.getD._eq_1, List.get?, Option.getD_some]
State after:
no goals

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

State before:
b n : ℕ
P : b > 1
i : ℕ
heq : ¬n / b ^ i / b = 0
⊢ List.getD (List.reverse (toDigitsCore b (n / b ^ i) (n / b ^ i / b) [] ++ [digitChar (n / b ^ i % b)])) 0
      (Char.ofNat 48) =
    digitChar (n / b ^ i % b)
Tactic:
simp only [List.reverse_append, List.reverse_cons, List.reverse_nil, List.nil_append, List.singleton_append,
List.getD._eq_1, List.get?, Option.getD_some]
State after:
no goals