simp [h, s] at hi
p : ℕ
hpri : Fact p.Prime
hp5 : 5 ≤ p
a b : ℤ
k₁ k₂ : Fin p
h0 : 0 < p
h1 : 1 < p
s : Finset ℕ := {0, 1, ↑k₁, ↑k₂}
this : s.card < 5
hs : s ⊆ range p
i : ℕ
hi : i ∈ range p \ s
hi0 : i ≠ 0
hi1 : i ≠ 1
hik₁ : i ≠ ↑k₁
h : i = ↑k₂
⊢ False
no goals