n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime k
h : MinFacHelper n k
h2 : minFac n = k
⊢ False
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime k
h : MinFacHelper n k
⊢ MinFacHelper n k'
refine minFacHelper_1 e h λ h2 ↦ ?_
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime (minFac n)
h : MinFacHelper n k
h2 : minFac n = k
⊢ False
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime k
h : MinFacHelper n k
h2 : minFac n = k
⊢ False
rw [← h2] at nk
no goals
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime (minFac n)
h : MinFacHelper n k
h2 : minFac n = k
⊢ False
exact nk <| minFac_prime h.one_lt.ne'