Theorem: Fin.rlexProd_val_mod (Fifteen/Data/Fin/Basic.lean)

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ ↑(rlexProd i j) % m = ↑i
Tactic:
dsimp [rlexProd]
State after:
m n : Nat
i : Fin m
j : Fin n
⊢ (↑i + m * ↑j) % m = ↑i

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ (↑i + m * ↑j) % m = ↑i
Tactic:
rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt i.2]
State after:
no goals