Theorem: Nat.toDigitsCore_shift_full (One.lean)

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

State before:
b n : ℕ
P : b > 1
i : ℕ
⊢ List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
Tactic:
induction i generalizing n with
| zero =>
  simp only [zero_eq, pow_zero, Nat.div_one]
| succ i ih =>
  rw [Nat.toDigitsCore_shift]
  . simp
    rw [ih]
    congr 3
    rw [Nat.div_div_eq_div_mul]
    congr 1
    rw [Nat.pow_succ']
  . exact P
  . simp
State after:
no goals

State before:
case zero
b : ℕ
P : b > 1
n : ℕ
⊢ List.getD (List.reverse (toDigits b n)) zero (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b ^ zero))) 0 (Char.ofNat 48)
Tactic:
simp only [zero_eq, pow_zero, Nat.div_one]
State after:
no goals

State before:
case succ
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ List.getD (List.reverse (toDigits b n)) (succ i) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b ^ succ i))) 0 (Char.ofNat 48)
Tactic:
rw [Nat.toDigitsCore_shift]
State after:
case succ
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ List.getD (List.reverse (toDigits b (n / b))) (succ i - 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b ^ succ i))) 0 (Char.ofNat 48)

case succ.P
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ b > 1

case succ.a
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ succ i > 0

State before:
case succ
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ List.getD (List.reverse (toDigits b (n / b))) (succ i - 1) (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b (n / b ^ succ i))) 0 (Char.ofNat 48)

case succ.P
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ b > 1

case succ.a
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ succ i > 0
Tactic:
. simp
  rw [ih]
  congr 3
  rw [Nat.div_div_eq_div_mul]
  congr 1
  rw [Nat.pow_succ']
State after:
case succ.P
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ b > 1

case succ.a
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ succ i > 0

State before:
case succ.P
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ b > 1

case succ.a
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ succ i > 0
Tactic:
. exact P
State after:
case succ.a
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ succ i > 0

State before:
case succ.a
b : ℕ
P : b > 1
i : ℕ
ih :
  ∀ (n : ℕ),
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48) =
      List.getD (List.reverse (toDigits b (n / b ^ i))) 0 (Char.ofNat 48)
n : ℕ
⊢ succ i > 0
Tactic:
. simp
State after:
no goals