n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
⊢ MinFacHelper n (k + 2)
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
⊢ MinFacHelper n k'
rw [← e]
case refine_1
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
⊢ (k + 2) % 2 = 1

case refine_2
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
⊢ k + 2 ≤ minFac n
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
⊢ MinFacHelper n (k + 2)
refine ⟨Nat.lt_add_right _ _ _ h.1, ?_, ?_⟩
case refine_2.inl
n k' : ℕ
e : minFac n + 2 = k'
h : MinFacHelper n (minFac n)
np : minFac n ≠ minFac n
⊢ minFac n + 2 ≤ minFac n

case refine_2.inr
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2 : k < minFac n
⊢ k + 2 ≤ minFac n
case refine_2
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
⊢ k + 2 ≤ minFac n
rcases h.2.2.eq_or_lt with rfl|h2
case refine_2.inr.inl
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k = minFac n
⊢ k + 2 ≤ minFac n

case refine_2.inr.inr
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k < minFac n
⊢ k + 2 ≤ minFac n
case refine_2.inr
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2 : k < minFac n
⊢ k + 2 ≤ minFac n
rcases (succ_le_of_lt h2).eq_or_lt with h2|h2
no goals
case refine_2.inr.inr
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k < minFac n
⊢ k + 2 ≤ minFac n
exact h2
case refine_1
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
⊢ k % 2 = 1
case refine_1
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
⊢ (k + 2) % 2 = 1
rw [add_mod, mod_self, add_zero, mod_mod]
no goals
case refine_1
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
⊢ k % 2 = 1
exact h.2.1
no goals
case refine_2.inl
n k' : ℕ
e : minFac n + 2 = k'
h : MinFacHelper n (minFac n)
np : minFac n ≠ minFac n
⊢ minFac n + 2 ≤ minFac n
exact (np rfl).elim
case refine_2.inr.inl
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k = minFac n
⊢ 2 = minFac n
case refine_2.inr.inl
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k = minFac n
⊢ k + 2 ≤ minFac n
refine ((h.1.trans_le h.2.2).ne ?_).elim
case h3
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k = minFac n
⊢ 2 ∣ minFac n

case refine_2.inr.inl
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k = minFac n
h3 : 2 ∣ minFac n
⊢ 2 = minFac n
case refine_2.inr.inl
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k = minFac n
⊢ 2 = minFac n
have h3 : 2 ∣ minFac n
case refine_2.inr.inl
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k = minFac n
h3 : 2 = 1 ∨ 2 = minFac n
⊢ 2 = minFac n
case refine_2.inr.inl
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k = minFac n
h3 : 2 ∣ minFac n
⊢ 2 = minFac n
rw [dvd_prime <| minFac_prime h.one_lt.ne'] at h3
case refine_2.inr.inl
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k = minFac n
h3 : 2 = minFac n
⊢ 2 = minFac n
case refine_2.inr.inl
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k = minFac n
h3 : 2 = 1 ∨ 2 = minFac n
⊢ 2 = minFac n
norm_num at h3
no goals
case refine_2.inr.inl
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k = minFac n
h3 : 2 = minFac n
⊢ 2 = minFac n
exact h3
case h3
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k = minFac n
⊢ (1 + 1 % 2) % 2 = 0
case h3
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k = minFac n
⊢ 2 ∣ minFac n
rw [Nat.dvd_iff_mod_eq_zero, ← h2, succ_eq_add_one, add_mod, h.2.1]
no goals
case h3
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
h2✝ : k < minFac n
h2 : succ k = minFac n
⊢ (1 + 1 % 2) % 2 = 0
norm_num