n k k' : ℕ
e : k + 2 = k'
nk : beq (n % k) 0 = false
h : MinFacHelper n k
h2 : minFac n = k
⊢ False
n k k' : ℕ
e : k + 2 = k'
nk : beq (n % k) 0 = false
h : MinFacHelper n k
⊢ MinFacHelper n k'
refine minFacHelper_1 e h λ h2 ↦ ?_
n k k' : ℕ
e : k + 2 = k'
nk✝ : beq (n % k) 0 = false
h : MinFacHelper n k
h2 : minFac n = k
nk : ¬n % k = 0
⊢ False
n k k' : ℕ
e : k + 2 = k'
nk : beq (n % k) 0 = false
h : MinFacHelper n k
h2 : minFac n = k
⊢ False
have nk := Nat.ne_of_beq_eq_false nk
n k k' : ℕ
e : k + 2 = k'
nk✝ : beq (n % k) 0 = false
h : MinFacHelper n k
h2 : minFac n = k
nk : ¬minFac n ∣ n
⊢ False
n k k' : ℕ
e : k + 2 = k'
nk✝ : beq (n % k) 0 = false
h : MinFacHelper n k
h2 : minFac n = k
nk : ¬n % k = 0
⊢ False
rw [← Nat.dvd_iff_mod_eq_zero, ← h2] at nk
no goals
n k k' : ℕ
e : k + 2 = k'
nk✝ : beq (n % k) 0 = false
h : MinFacHelper n k
h2 : minFac n = k
nk : ¬minFac n ∣ n
⊢ False
exact nk <| minFac_dvd n