have h_mod_q' : (2 : (ZMod q)) ^ p = 1 := by
  have := (ZMod.natCast_eq_natCast_iff _ _ _).mpr h_mod_q
  norm_cast at this
  rw [← this, cast_pow, cast_ofNat]
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
⊢ ∃ 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
⊢ ∃ x, x.Prime ∧ p < x