num_3_dvd_of_mod_9_eq_3_or_6

Stream: Is there code for X?

[Patrick Johnson]

Any better way to prove this lemma?

import tactic

lemma num_3_dvd_of_mod_9_eq_3_or_6 {n : ℕ}
  (h : n % 9 = 3 ∨ n % 9 = 6) : 3 ∣ n :=
begin
  cases h;
  { induction n using nat.strong_induction_on with n ih, dsimp at ih,
    repeat { cases n, dec_trivial <|> cases h, try {
      change 3 ∣ n + 3 + 3 + 3, simp, apply ih,
      { change n < n + 9, exact lt_add_of_pos_right n dec_trivial },
      change (n + 9) % 9 = _ at h, simp at h, exact h }}},
end

[Kevin Buzzard]

Use div_add_mod

[Patrick Johnson]

I ended up using mod_mod_of_dvd, which seems fine enough:

lemma num_3_dvd_of_mod_9_eq_3_or_6 {n : ℕ}
  (h : n % 9 = 3 ∨ n % 9 = 6) : 3 ∣ n :=
begin
  have h₁ : n % 9 % 3 = 0, { cases h; rw h; dec_trivial },
  rw nat.mod_mod_of_dvd at h₁, swap, { dec_trivial },
  exact nat.dvd_of_mod_eq_zero h₁,
end