Values of n (mod 3)

Stream: new members

[Harry Pacitti]

I'm working on the proof below but am stuck on the lines including sorry. Any help would be appreciated.

import algebra.field.basic
import number_theory.pythagorean_triples
import ring_theory.int.basic
import algebra.group_with_zero.power
import tactic.ring
import tactic.ring_exp
import tactic.field_simp
import data.zmod.basic

lemma mod_three_eq_zero_or_one_or_two (n : ℤ) : n % 3 = 0 ∨ n % 3 = 1 ∨ n % 3 = 2 :=
have h : n % 3 < 3 := abs_of_nonneg (show 0 ≤ (2 : ℤ), from dec_trivial) ▸ int.mod_lt _ dec_trivial,
have h₁ : 0 ≤ n % 3 := int.mod_nonneg _ dec_trivial,
match (n % 3), h, h₁ with
| (0:ℕ) := λ _ _, or.inl rfl
| (1 : ℕ) := λ _ _, sorry
| (2 : ℕ) := λ _ _, sorry
| (k + 3 : ℕ) := λ h _, absurd h dec_trivial
| -[1+ a] := λ _ h₁, absurd h₁ dec_trivial
end

[Marcus Rossel]

Do or.inr (or.inl rfl) and or.inr (or.inr rfl) work?