rw [Fin.val_mk, ← ZMod.val_cast_of_lt (Fin.is_lt k)]
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 1 [ZMOD ↑p]
⊢ ↑k = ↑⟨1, ⋯⟩
p : ℕ
hpri : p.Prime
k : Fin p
hcong : ↑↑k ≡ 1 [ZMOD ↑p]
⊢ (↑↑k).val = ↑⟨1, ⋯⟩