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

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

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ (↑i + m * ↑j) / m = ↑j
Tactic:
rewrite [Nat.add_mul_div_left _ _ i.pos, Nat.div_eq_of_lt i.2]
State after:
m n : Nat
i : Fin m
j : Fin n
⊢ 0 + ↑j = ↑j

State before:
m n : Nat
i : Fin m
j : Fin n
⊢ 0 + ↑j = ↑j
Tactic:
exact j.1.zero_add
State after:
no goals