simp only [Int.cast_add, algebraMap.coe_one]
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
⊢ (↑(1 + 1)).val = 2
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
⊢ (↑1 + ↑1).val = 2