have h_mod_q : 2 ^ p  ≡ 1 [MOD q] := by
  have : (2^p - 1) % q = 0 :=  mod_eq_zero_of_dvd (minFac_dvd m)
  change (2^p - 1) ≡ 0 [MOD q] at this
  rw [modEq_iff_dvd, dvd_iff_exists_eq_mul_left] at *
  obtain ⟨c, hc⟩ := this
  use c
  simp only [CharP.cast_eq_zero, ge_iff_le, gt_iff_lt, pow_pos, cast_pred, cast_pow, cast_ofNat,
      zero_sub, neg_sub] at hc
  simp [cast_one, cast_pow, cast_ofNat, hc.symm]
p : ℕ
hp : p.Prime
this✝ : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : q.Prime
this : Fact q.Prime
⊢ ∃ 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
⊢ ∃ x, x.Prime ∧ p < x