Proof about sum of digits mod 9

Stream: new members

[Alex Gu]

I proved a theorem that n mod 9 is equal to the sum of the digits of n mod 9. However, I feel like the last step is probably provable in a more simple way. Is there a way to make it simpler? I am also wondering about the difference between Nat.digits 10 n and n.digits 10. It seems like they should be the same, but I couldn't figure out the tactic to show their equivalence. Thanks!

import Mathlib

theorem divisible_by_nine_iff_sum_digits_divisible_by_nine (n : ℕ) :
  9 ∣ n ↔ 9 ∣ ((Nat.digits 10 n).sum) := by

  have h : n ≡ (Nat.digits 10 n).sum [MOD 9] := by
    have h_aux : 10 % 9 = 1 := by exact rfl
    exact ((Nat.modEq_digits_sum 9 10 h_aux) n)

  rw [← Nat.modEq_zero_iff_dvd, ← Nat.modEq_zero_iff_dvd]
  constructor
  · exact fun a => Nat.ModEq.trans (id (Nat.ModEq.symm h)) a
  · exact fun a => Nat.ModEq.symm (Nat.ModEq.trans (id (Nat.ModEq.symm a)) (id (Nat.ModEq.symm h)))

[Mario Carneiro]

I am also wondering about the difference between Nat.digits 10 n and n.digits 10. It seems like they should be the same, but I couldn't figure out the tactic to show their equivalence.

They are literally the same thing after parsing, the tactic to show their equivalence is rfl

[Aaron Liu]

n.digits 10 is just syntax sugar for Nat.digits 10 n

[Matt Diamond]

it's not syntax sugar for Nat.digits n 10?

[Mario Carneiro]

ah, indeed the arguments are flipped, n.digits 10 is the digits of 10 in base n

[Mario Carneiro]

so probably not what you want

[Mario Carneiro]

10.digits n doesn't parse, but (10).digits n does and is equivalent to Nat.digits 10 n

[Alex Gu]

is this explicitly defined somewhere in the source code (and how can I find it)?

[Alex Gu]

and why in the world does 10.digits n not parse :laughter_tears:

[Mario Carneiro]

It's described in https://lean-lang.org/doc/reference/latest////Terms/Function-Application/#generalized-field-notation

[Mario Carneiro]

Alex Gu said:

and why in the world does 10.digits n not parse :laughter_tears:

gotta love float parser shenanigans

[Mario Carneiro]

:this: @Kyle Miller are you in the mood for another random parser issue to fix?

[Matt Diamond]

@Alex Gu re: cleaning up the proof, one small thing would be to remove the id function calls, as they don't accomplish anything

[Mario Carneiro]

you can significantly shorten the last two lines using "generalized field notation":

  constructor
  · exact fun a => h.symm.trans a
  · exact fun a => (a.symm.trans h.symm).symm

[Mario Carneiro]

also the double symm on the last line is redundant

  · exact fun a => h.trans a

[Jireh Loreaux]

and if you're feeling :chili_pepper: (h.trans ·)

[Aaron Liu]

or just h.trans