have : (2 : (ZMod q)) * (2 ^ (p - 1)) = 1 := by
  convert h_mod_q'
  nth_rw 1 [← pow_one 2]
  rw [← pow_add 2 1 (p - 1)]
  congr
  exact add_sub_of_le <| Prime.pos hp
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
⊢ ∃ x, x.Prime ∧ p < x
p : ℕ
hp : p.Prime
this✝¹ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this✝ : Fact q.Prime
h_mod_q : q.ModEq (2 ^ p) 1
h_mod_q' : 2 ^ p = 1
this : 2 * 2 ^ (p - 1) = 1
⊢ ∃ x, x.Prime ∧ p < x