have : Fact (Nat.Prime q) := by exact { out := hq }
p : ℕ
hp : p.Prime
this : Fact p.Prime
m : ℕ := mersenne p
q : ℕ := m.minFac
hq : 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
⊢ ∃ x, x.Prime ∧ p < x