n : ℕ
pos : 0 < n
np : ¬Prime n
h0 : n = minFac n * 0
⊢ ¬0 < 0
n : ℕ
pos : 0 < n
np : ¬Prime n
h0 : n = minFac n * 0
⊢ ¬0 < n
rw [h0, mul_zero]
no goals
n : ℕ
pos : 0 < n
np : ¬Prime n
h0 : n = minFac n * 0
⊢ ¬0 < 0
exact by decide
no goals
n : ℕ
pos : 0 < n
np : ¬Prime n
h0 : n = minFac n * 0
⊢ ¬0 < 0
decide
n : ℕ
pos : 0 < n
np : ¬Prime n
h1 : n = minFac n
⊢ minFac n ≤ n / minFac n
n : ℕ
pos : 0 < n
np : ¬Prime n
h1 : n = minFac n * 1
⊢ minFac n ≤ n / minFac n
rw [mul_one] at h1
n : ℕ
pos : 0 < n
np : n < 2
h1 : n = minFac n
⊢ minFac n ≤ n / minFac n
n : ℕ
pos : 0 < n
np : ¬Prime n
h1 : n = minFac n
⊢ minFac n ≤ n / minFac n
rw [prime_def_minFac, not_and_or, ← h1, eq_self_iff_true, _root_.not_true, or_false_iff,
  not_le] at np
no goals
n : ℕ
pos : 0 < n
np : n < 2
h1 : n = minFac n
⊢ minFac n ≤ n / minFac n
rw [le_antisymm (le_of_lt_succ np) (succ_le_of_lt pos), minFac_one, Nat.div_one]
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = minFac n * (x + 2)
⊢ minFac n ≤ minFac n * (x + 2) / minFac n
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = minFac n * (x + 2)
⊢ minFac n ≤ n / minFac n
conv_rhs =>
  congr
  rw [hx]
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = minFac n * (x + 2)
⊢ minFac n ≤ x + 2
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = minFac n * (x + 2)
⊢ minFac n ≤ minFac n * (x + 2) / minFac n
rw [Nat.mul_div_cancel_left _ (minFac_pos _)]
no goals
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = minFac n * (x + 2)
⊢ minFac n ≤ x + 2
exact minFac_le_of_dvd (le_add_left 2 x) ⟨minFac n, by rwa [mul_comm]⟩
no goals
n : ℕ
pos : 0 < n
np : ¬Prime n
x : ℕ
hx : n = minFac n * (x + 2)
⊢ n = (x + 2) * minFac n
rwa [mul_comm]