Theorem: Nat.toDigitsCore_shift (One.lean)

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

State before:
b n : ℕ
P : b > 1
i : ℕ
igt : i > 0
⊢ List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) (i - 1) (Char.ofNat 48)
Tactic:
generalize h: i - 1 = p
State after:
b n : ℕ
P : b > 1
i : ℕ
igt : i > 0
p : ℕ
h : i - 1 = p
⊢ List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) p (Char.ofNat 48)

State before:
b n : ℕ
P : b > 1
i : ℕ
igt : i > 0
p : ℕ
h : i - 1 = p
⊢ List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) p (Char.ofNat 48)
Tactic:
have heq: i = p + 1 := by cases i with | zero => contradiction | succ n => simp at h; rw [h]
State after:
b n : ℕ
P : b > 1
i : ℕ
igt : i > 0
p : ℕ
h : i - 1 = p
heq : i = p + 1
⊢ List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) p (Char.ofNat 48)

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

State before:
b n : ℕ
P : b > 1
i : ℕ
igt : i > 0
p : ℕ
h : i - 1 = p
heq : i = p + 1
⊢ List.getD (List.reverse (toDigits b n)) (p + 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b))) p (Char.ofNat 48)
Tactic:
apply Nat.toDigitsCore_shift'
State after:
case P
b n : ℕ
P : b > 1
i : ℕ
igt : i > 0
p : ℕ
h : i - 1 = p
heq : i = p + 1
⊢ b > 1

State before:
case P
b n : ℕ
P : b > 1
i : ℕ
igt : i > 0
p : ℕ
h : i - 1 = p
heq : i = p + 1
⊢ b > 1
Tactic:
exact P
State after:
no goals

State before:
b n : ℕ
P : b > 1
i : ℕ
igt : i > 0
p : ℕ
h : i - 1 = p
⊢ i = p + 1
Tactic:
cases i with | zero => contradiction | succ n => simp at h; rw [h]
State after:
no goals

State before:
case zero
b n : ℕ
P : b > 1
p : ℕ
igt : zero > 0
h : zero - 1 = p
⊢ zero = p + 1
Tactic:
contradiction
State after:
no goals

State before:
case succ
b n✝ : ℕ
P : b > 1
p n : ℕ
igt : succ n > 0
h : succ n - 1 = p
⊢ succ n = p + 1
Tactic:
simp at h
State after:
case succ
b n✝ : ℕ
P : b > 1
p n : ℕ
igt : succ n > 0
h : n = p
⊢ succ n = p + 1

State before:
case succ
b n✝ : ℕ
P : b > 1
p n : ℕ
igt : succ n > 0
h : n = p
⊢ succ n = p + 1
Tactic:
rw [h]
State after:
no goals