-- Mathlib/Data/Nat/Digits.lean
theorem sub_one_mul_sum_log_div_pow_eq_sub_sum_digits {p : ℕ} (n : ℕ) :
    (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

Proof state:
case h.e'_3.h.e'_5
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ n = ofDigits p (p.digits n)

Tactic:
exact (ofDigits_digits p n).symm

Result:
no goals

Proof state:
case inl
p n : ℕ
h : 1 < p
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Result:
case inl.inl
p : ℕ
h : 1 < p
⊢ (p - 1) * ∑ i ∈ range (log p 0).succ, 0 / p ^ i.succ = 0 - (p.digits 0).sum

case inl.inr
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

Proof state:
case inr.inl
n : ℕ
⊢ (1 - 1) * ∑ i ∈ range (log 1 n).succ, n / 1 ^ i.succ = n - (digits 1 n).sum

Tactic:
simp

Result:
no goals

Proof state:
p n : ℕ
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

Tactic:
obtain h | rfl | h : 1 < p ∨ 1 = p ∨ p < 1 := trichotomous 1 p

Result:
case inl
p n : ℕ
h : 1 < p
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

case inr.inl
n : ℕ
⊢ (1 - 1) * ∑ i ∈ range (log 1 n).succ, n / 1 ^ i.succ = n - (digits 1 n).sum

case inr.inr
p n : ℕ
h : p < 1
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

Proof state:
case inl.inl
p : ℕ
h : 1 < p
⊢ (p - 1) * ∑ i ∈ range (log p 0).succ, 0 / p ^ i.succ = 0 - (p.digits 0).sum

Tactic:
simp

Result:
no goals

Proof state:
case inr.inr
p n : ℕ
h : p < 1
⊢ 0 = n - (digits 0 n).sum

Tactic:
cases n

Result:
case inr.inr.zero
p : ℕ
h : p < 1
⊢ 0 = 0 - (digits 0 0).sum

case inr.inr.succ
p : ℕ
h : p < 1
n✝ : ℕ
⊢ 0 = n✝ + 1 - (digits 0 (n✝ + 1)).sum

Proof state:
case h.e'_2.h.e'_6.a.h.e'_5
p n : ℕ
h : 1 < p
hn : n ≠ 0
x✝ : ℕ
a✝ : x✝ ∈ range (p.digits n).length
⊢ n = ofDigits p (p.digits n)

case h.e'_3.h.e'_5
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ n = ofDigits p (p.digits n)

Tactic:
all_goals exact (ofDigits_digits p n).symm

Result:
no goals

Proof state:
case inl.inr
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

Tactic:
convert sub_one_mul_sum_div_pow_eq_sub_sum_digits (p.digits n) (getLast_digit_ne_zero p hn) <|
    (fun l a ↦ digits_lt_base h a)

Result:
case h.e'_2.h.e'_6.h.h.e'_1
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ (log p n).succ = (p.digits n).length

case h.e'_2.h.e'_6.a.h.e'_5
p n : ℕ
h : 1 < p
hn : n ≠ 0
x✝ : ℕ
a✝ : x✝ ∈ range (p.digits n).length
⊢ n = ofDigits p (p.digits n)

case h.e'_3.h.e'_5
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ n = ofDigits p (p.digits n)

Proof state:
case inr.inr
p n : ℕ
h : p < 1
⊢ (p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum

Tactic:
simp [lt_one_iff.mp h]

Result:
case inr.inr
p n : ℕ
h : p < 1
⊢ 0 = n - (digits 0 n).sum

Proof state:
case h.e'_2.h.e'_6.h.h.e'_1
p n : ℕ
h : 1 < p
hn : n ≠ 0
⊢ (log p n).succ = (p.digits n).length

Tactic:
refine (digits_len p n h hn).symm

Result:
no goals

Proof state:
case inr.inr.succ
p : ℕ
h : p < 1
n✝ : ℕ
⊢ 0 = n✝ + 1 - (digits 0 (n✝ + 1)).sum

Tactic:
simp

Result:
no goals

Proof state:
case inr.inr.zero
p : ℕ
h : p < 1
⊢ 0 = 0 - (digits 0 0).sum

case inr.inr.succ
p : ℕ
h : p < 1
n✝ : ℕ
⊢ 0 = n✝ + 1 - (digits 0 (n✝ + 1)).sum

Tactic:
all_goals simp

Result:
no goals