n k : ℕ
h1 : MinFacHelper n k
h2 : ble (k * k) n = false
⊢ Nat.Prime n
n k : ℕ
h1 : MinFacHelper n k
h2 : ble (k * k) n = false
⊢ IsNat (minFac n) n
refine ⟨(Nat.prime_def_minFac.mp ?_).2⟩
n k : ℕ
h1 : MinFacHelper n k
h2 : ble (k * k) n = false
⊢ 2 ≤ n ∧ ∀ (m : ℕ), 2 ≤ m → m ≤ sqrt n → ¬m ∣ n
n k : ℕ
h1 : MinFacHelper n k
h2 : ble (k * k) n = false
⊢ Nat.Prime n
rw [Nat.prime_def_le_sqrt]
n k : ℕ
h1 : MinFacHelper n k
h2 : ble (k * k) n = false
m : ℕ
hm : 2 ≤ m
hmn : m ≤ sqrt n
h2mn : m ∣ n
⊢ False
n k : ℕ
h1 : MinFacHelper n k
h2 : ble (k * k) n = false
⊢ 2 ≤ n ∧ ∀ (m : ℕ), 2 ≤ m → m ≤ sqrt n → ¬m ∣ n
refine ⟨h1.one_lt, λ m hm hmn h2mn ↦ ?_⟩
no goals
n k : ℕ
h1 : MinFacHelper n k
h2 : ble (k * k) n = false
m : ℕ
hm : 2 ≤ m
hmn : m ≤ sqrt n
h2mn : m ∣ n
⊢ False
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