have h2q : 2 ≤ q := by
  exact Prime.two_le <| minFac_prime <| Nat.ne_of_gt <| lt_of_succ_lt <|
      Nat.sub_le_sub_right ((pow_le_pow_of_le_right (succ_pos 1) (Prime.two_le hp))) 1
case h.right
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
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
h_piv_div_q_sub_one : p ∣ q - 1
⊢ p < q
case h.right
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
two : (ZMod q)ˣ := Units.mkOfMulEqOne 2 (2 ^ (p - 1)) this
two_desc : ↑two = 2
h_two : two ^ p = 1
two_ne_one : two ≠ 1
h_piv_div_q_sub_one : p ∣ q - 1
h2q : 2 ≤ q
⊢ p < q