rw [succ_pred_prime hpri] at this
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
this✝ : Fact p.Prime
this : p.pred.pred.succ.succ = p.pred.succ
⊢ (↑1 + ↑1).val = 2
p : ℕ
hpri✝ : p.Prime
k : Fin p
hpri : p.Prime
hp5 : 5 ≤ p
hcong : ↑↑↑k = ↑(1 + 1)
this✝ : Fact p.Prime
this : p.pred.pred.succ.succ = p
⊢ (↑1 + ↑1).val = 2