calc
  6 * a (p - 2) = 3 * 2 ^ (p - 1) + 2 * 3 ^ (p - 1) + (2 * 3) ^ (p - 1) - 6 := by
    simp only [a, hp', pow_succ']; ring
  _ ≡ 3 * 1 + 2 * 1 + 1 - 6 [ZMOD p] := by
    gcongr <;> apply Int.ModEq.pow_card_sub_one_eq_one hp <;>
      rwa [Int.isCoprime_iff_gcd_eq_one, Int.gcd_comm]
  _ = 0 := rfl
p : ℕ
hp : p.Prime
hp2 : p.Coprime 2
hp3 : p.Coprime 3
this : (↑p).gcd 6 = 1
hp' : p - 1 = p - 2 + 1
⊢ 6 * a (p - 2) ≡ 6 * 0 [ZMOD ↑p]
no goals