Theorem: Nat.toDigits_modulo (One.lean)

State before:
b n p i : ℕ
P : i < p
Q : b > 1
⊢ List.getD (List.reverse (toDigits b (n % b ^ p))) i (Char.ofNat 48) =
    List.getD (List.reverse (toDigits b n)) i (Char.ofNat 48)
Tactic:
rw [Nat.toDigits_eq_digit_rev, Nat.toDigits_eq_digit_rev]
State after:
b n p i : ℕ
P : i < p
Q : b > 1
⊢ digitChar (digit b (n % b ^ p) i) = digitChar (digit b n i)

case P
b n p i : ℕ
P : i < p
Q : b > 1
⊢ b > 1

case P
b n p i : ℕ
P : i < p
Q : b > 1
⊢ b > 1

State before:
b n p i : ℕ
P : i < p
Q : b > 1
⊢ b > 1
Tactic:
case P => exact Q
State after:
no goals

State before:
b n p i : ℕ
P : i < p
Q : b > 1
⊢ digitChar (digit b (n % b ^ p) i) = digitChar (digit b n i)
Tactic:
congr 1
State after:
case e_n
b n p i : ℕ
P : i < p
Q : b > 1
⊢ digit b (n % b ^ p) i = digit b n i

State before:
case e_n
b n p i : ℕ
P : i < p
Q : b > 1
⊢ digit b (n % b ^ p) i = digit b n i
Tactic:
unfold digit
State after:
case e_n
b n p i : ℕ
P : i < p
Q : b > 1
⊢ n % b ^ p / b ^ i % b = n / b ^ i % b

State before:
case e_n
b n p i : ℕ
P : i < p
Q : b > 1
⊢ n % b ^ p / b ^ i % b = n / b ^ i % b
Tactic:
have hpeq := Nat.sub_add_cancel (le_of_lt P)
State after:
case e_n
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ n % b ^ p / b ^ i % b = n / b ^ i % b

State before:
case e_n
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ n % b ^ p / b ^ i % b = n / b ^ i % b
Tactic:
conv => left; left; left; rw [← hpeq, pow_add]
State after:
case e_n
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ n % (b ^ (p - i) * b ^ i) / b ^ i % b = n / b ^ i % b

State before:
case e_n
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ n % (b ^ (p - i) * b ^ i) / b ^ i % b = n / b ^ i % b
Tactic:
rw [Nat.mod_mul_left_div_self, Nat.mod_mod_of_dvd]
State after:
case e_n.h
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ b ∣ b ^ (p - i)

State before:
case e_n.h
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ b ∣ b ^ (p - i)
Tactic:
apply dvd_pow
State after:
case e_n.h.hxy
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ b ∣ b

case e_n.h.x
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ p - i ≠ 0

State before:
case e_n.h.hxy
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ b ∣ b

case e_n.h.x
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ p - i ≠ 0
Tactic:
. apply dvd_refl
State after:
case e_n.h.x
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ p - i ≠ 0

State before:
case e_n.h.x
b n p i : ℕ
P : i < p
Q : b > 1
hpeq : p - i + i = p
⊢ p - i ≠ 0
Tactic:
. simp only [min_le_iff, ge_iff_le, tsub_le_iff_right, le_min_iff, _root_.zero_le, nonpos_iff_eq_zero, ne_eq,
    tsub_eq_zero_iff_le, not_and, not_le, P, implies_true]
State after:
no goals

State before:
b n p i : ℕ
P : i < p
Q : b > 1
⊢ b > 1
Tactic:
exact Q
State after:
no goals