[GOAL]
n k : ℕ
h : MinFacHelper n k
⊢ 1 < n
[PROOFSTEP]
have : 2 < minFac n := h.1.trans_le h.2.2
[GOAL]
n k : ℕ
h : MinFacHelper n k
this : 2 < minFac n
⊢ 1 < n
[PROOFSTEP]
rcases eq_zero_or_pos n with rfl | h
[GOAL]
case inl
k : ℕ
h : MinFacHelper 0 k
this : 2 < minFac 0
⊢ 1 < 0
[PROOFSTEP]
contradiction
[GOAL]
case inr
n k : ℕ
h✝ : MinFacHelper n k
this : 2 < minFac n
h : n > 0
⊢ 1 < n
[PROOFSTEP]
rcases(succ_le_of_lt h).eq_or_lt with rfl | h
[GOAL]
case inr.inl
k : ℕ
h✝ : MinFacHelper (succ 0) k
this : 2 < minFac (succ 0)
h : succ 0 > 0
⊢ 1 < succ 0
[PROOFSTEP]
contradiction
[GOAL]
case inr.inr
n k : ℕ
h✝¹ : MinFacHelper n k
this : 2 < minFac n
h✝ : n > 0
h : succ 0 < n
⊢ 1 < n
[PROOFSTEP]
exact h
[GOAL]
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ MinFacHelper n 3
[PROOFSTEP]
refine ⟨by norm_num, by norm_num, ?_⟩
[GOAL]
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ 2 < 3
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ 3 % 2 = 1
[PROOFSTEP]
norm_num
[GOAL]
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
⊢ 3 ≤ minFac n
[PROOFSTEP]
refine (le_minFac'.mpr λ p hp hpn ↦ ?_).resolve_left (Nat.ne_of_gt (Nat.le_of_ble_eq_true h1))
[GOAL]
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
p : ℕ
hp : 2 ≤ p
hpn : p ∣ n
⊢ 3 ≤ p
[PROOFSTEP]
rcases hp.eq_or_lt with rfl | h
[GOAL]
case inl
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
hp : 2 ≤ 2
hpn : 2 ∣ n
⊢ 3 ≤ 2
[PROOFSTEP]
simp [(Nat.dvd_iff_mod_eq_zero ..).1 hpn] at h2 
[GOAL]
case inr
n : ℕ
h1 : ble 2 n = true
h2 : 1 = n % 2
p : ℕ
hp : 2 ≤ p
hpn : p ∣ n
h : 2 < p
⊢ 3 ≤ p
[PROOFSTEP]
exact h
[GOAL]
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
⊢ MinFacHelper n k'
[PROOFSTEP]
rw [← e]
[GOAL]
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
⊢ MinFacHelper n (k + 2)
[PROOFSTEP]
refine ⟨Nat.lt_add_right _ _ _ h.1, ?_, ?_⟩
[GOAL]
case refine_1
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
⊢ (k + 2) % 2 = 1
[PROOFSTEP]
rw [add_mod, mod_self, add_zero, mod_mod]
[GOAL]
case refine_1
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
⊢ k % 2 = 1
[PROOFSTEP]
exact h.2.1
[GOAL]
case refine_2
n k k' : ℕ
e : k + 2 = k'
h : MinFacHelper n k
np : minFac n ≠ k
⊢ k + 2 ≤ minFac n
[PROOFSTEP]
rcases h.2.2.eq_or_lt with rfl | h2
[GOAL]
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
[PROOFSTEP]
exact (np rfl).elim
[GOAL]
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
[PROOFSTEP]
rcases(succ_le_of_lt h2).eq_or_lt with h2 | h2
[GOAL]
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
[PROOFSTEP]
refine ((h.1.trans_le h.2.2).ne ?_).elim
[GOAL]
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
[PROOFSTEP]
have h3 : 2 ∣ minFac n
[GOAL]
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
[PROOFSTEP]
rw [Nat.dvd_iff_mod_eq_zero, ← h2, succ_eq_add_one, add_mod, h.2.1]
[GOAL]
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
[PROOFSTEP]
norm_num
[GOAL]
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
[PROOFSTEP]
rw [dvd_prime <| minFac_prime h.one_lt.ne'] at h3 
[GOAL]
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
[PROOFSTEP]
norm_num at h3 
[GOAL]
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
[PROOFSTEP]
exact h3
[GOAL]
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
[PROOFSTEP]
exact h2
[GOAL]
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime k
h : MinFacHelper n k
⊢ MinFacHelper n k'
[PROOFSTEP]
refine minFacHelper_1 e h λ h2 ↦ ?_
[GOAL]
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime k
h : MinFacHelper n k
h2 : minFac n = k
⊢ False
[PROOFSTEP]
rw [← h2] at nk 
[GOAL]
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime (minFac n)
h : MinFacHelper n k
h2 : minFac n = k
⊢ False
[PROOFSTEP]
exact nk <| minFac_prime h.one_lt.ne'
[GOAL]
n k k' : ℕ
e : k + 2 = k'
nk : beq (n % k) 0 = false
h : MinFacHelper n k
⊢ MinFacHelper n k'
[PROOFSTEP]
refine minFacHelper_1 e h λ h2 ↦ ?_
[GOAL]
n k k' : ℕ
e : k + 2 = k'
nk : beq (n % k) 0 = false
h : MinFacHelper n k
h2 : minFac n = k
⊢ False
[PROOFSTEP]
have nk := Nat.ne_of_beq_eq_false nk
[GOAL]
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
[PROOFSTEP]
rw [← Nat.dvd_iff_mod_eq_zero, ← h2] at nk 
[GOAL]
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
[PROOFSTEP]
exact nk <| minFac_dvd n
[GOAL]
a : ℕ
h : a % 2 = 0
⊢ minFac a = ↑2
[PROOFSTEP]
rw [cast_ofNat, minFac_eq_two_iff, Nat.dvd_iff_mod_eq_zero, h]
[GOAL]
n k : ℕ
h1 : MinFacHelper n k
h2 : 0 = n % k
⊢ IsNat (minFac n) k
[PROOFSTEP]
rw [eq_comm, ← Nat.dvd_iff_mod_eq_zero] at h2 
[GOAL]
n k : ℕ
h1 : MinFacHelper n k
h2 : k ∣ n
⊢ IsNat (minFac n) k
[PROOFSTEP]
exact ⟨le_antisymm (minFac_le_of_dvd h1.1.le h2) h1.2.2⟩
[GOAL]
n k : ℕ
h1 : MinFacHelper n k
h2 : ble (k * k) n = false
⊢ IsNat (minFac n) n
[PROOFSTEP]
refine ⟨(Nat.prime_def_minFac.mp ?_).2⟩
[GOAL]
n k : ℕ
h1 : MinFacHelper n k
h2 : ble (k * k) n = false
⊢ Nat.Prime n
[PROOFSTEP]
rw [Nat.prime_def_le_sqrt]
[GOAL]
n k : ℕ
h1 : MinFacHelper n k
h2 : ble (k * k) n = false
⊢ 2 ≤ n ∧ ∀ (m : ℕ), 2 ≤ m → m ≤ sqrt n → ¬m ∣ n
[PROOFSTEP]
refine ⟨h1.one_lt, λ m hm hmn h2mn ↦ ?_⟩
[GOAL]
n k : ℕ
h1 : MinFacHelper n k
h2 : ble (k * k) n = false
m : ℕ
hm : 2 ≤ m
hmn : m ≤ sqrt n
h2mn : m ∣ n
⊢ False
[PROOFSTEP]
exact
  lt_irrefl m <|
    calc
      m ≤ sqrt n := hmn
      _ < k := (sqrt_lt.mpr (ble_eq_false.mp h2))
      _ ≤ n.minFac := h1.2.2
      _ ≤ m := Nat.minFac_le_of_dvd hm h2mn
