[GOAL]
n : ℕ
src✝ : Mul (Fin n) := inferInstanceAs (Mul (Fin n))
x✝² x✝¹ x✝ : Fin n
a : ℕ
ha : a < n
b : ℕ
hb : b < n
c : ℕ
hc : c < n
⊢ a * b * c ≡ a * (b * c) [MOD n]
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
n : ℕ
x✝² x✝¹ x✝ : Fin n
a : ℕ
ha : a < n
b : ℕ
hb : b < n
c : ℕ
hc : c < n
⊢ a * (b + c) ≡ a * b + a * c [MOD n]
[PROOFSTEP]
rw [mul_add]
[GOAL]
n : ℕ
src✝¹ : AddCommSemigroup (Fin n) := addCommSemigroup n
src✝ : CommSemigroup (Fin n) := instCommSemigroup n
a b c : Fin n
⊢ (a + b) * c = a * c + b * c
[PROOFSTEP]
rw [mul_comm, left_distrib_aux, mul_comm _ b, mul_comm]
[GOAL]
⊢ Repr (ZMod 0)
[PROOFSTEP]
dsimp [ZMod]
[GOAL]
⊢ Repr ℤ
[PROOFSTEP]
infer_instance
[GOAL]
n : ℕ
⊢ Repr (ZMod (n + 1))
[PROOFSTEP]
dsimp [ZMod]
[GOAL]
n : ℕ
⊢ Repr (Fin (n + 1))
[PROOFSTEP]
infer_instance
[GOAL]
n : ℕ
inst✝ : Fintype (ZMod n)
⊢ Fintype.card (ZMod n) = n
[PROOFSTEP]
cases n with
| zero => exact (not_finite (ZMod 0)).elim
| succ n => convert Fintype.card_fin (n + 1) using 2
[GOAL]
n : ℕ
inst✝ : Fintype (ZMod n)
⊢ Fintype.card (ZMod n) = n
[PROOFSTEP]
cases n with
| zero => exact (not_finite (ZMod 0)).elim
| succ n => convert Fintype.card_fin (n + 1) using 2
[GOAL]
case zero
inst✝ : Fintype (ZMod Nat.zero)
⊢ Fintype.card (ZMod Nat.zero) = Nat.zero
[PROOFSTEP]

| zero => exact (not_finite (ZMod 0)).elim
[GOAL]
case zero
inst✝ : Fintype (ZMod Nat.zero)
⊢ Fintype.card (ZMod Nat.zero) = Nat.zero
[PROOFSTEP]
exact (not_finite (ZMod 0)).elim
[GOAL]
case succ
n : ℕ
inst✝ : Fintype (ZMod (Nat.succ n))
⊢ Fintype.card (ZMod (Nat.succ n)) = Nat.succ n
[PROOFSTEP]

| succ n => convert Fintype.card_fin (n + 1) using 2
[GOAL]
case succ
n : ℕ
inst✝ : Fintype (ZMod (Nat.succ n))
⊢ Fintype.card (ZMod (Nat.succ n)) = Nat.succ n
[PROOFSTEP]
convert Fintype.card_fin (n + 1) using 2
