case refine_1
p' : ℕ
⊢ 1 < p' + 2

case refine_2
p' : ℕ
⊢ minFac (mersenne (p' + 2)) ≠ 2
p' : ℕ
⊢ 2 < q (p' + 2)
refine (minFac_prime (one_lt_mersenne ?_).ne').two_le.lt_of_ne' ?_
no goals
case refine_1
p' : ℕ
⊢ 1 < p' + 2
exact le_add_left _ _
case refine_2
p' : ℕ
⊢ ¬2 ∣ 2 * 2 ^ (p' + 1) - 1
case refine_2
p' : ℕ
⊢ minFac (mersenne (p' + 2)) ≠ 2
rw [Ne.def, minFac_eq_two_iff, mersenne, Nat.pow_succ']
no goals
case refine_2
p' : ℕ
⊢ ¬2 ∣ 2 * 2 ^ (p' + 1) - 1
exact Nat.two_not_dvd_two_mul_sub_one (Nat.one_le_two_pow _)