no goals
⊢ 0 ≠ 0 → List.prod (factors 0) = 0
simp
no goals
⊢ 1 ≠ 0 → List.prod (factors 1) = 1
simp
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
h₁ : (k + 2) / m ≠ 0
⊢ List.prod (factors (k + 2)) = k + 2
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
⊢ List.prod (factors (k + 2)) = k + 2
have h₁ : (k + 2) / m ≠ 0 := fun h => by
  have : (k + 2) = 0 * m := (Nat.div_eq_iff_eq_mul_left (minFac_pos _) (minFac_dvd _)).1 h
  rw [zero_mul] at this; exact (show k + 2 ≠ 0 by simp) this
no goals
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
h₁ : (k + 2) / m ≠ 0
⊢ List.prod (factors (k + 2)) = k + 2
rw [factors, List.prod_cons, prod_factors h₁, Nat.mul_div_cancel' (minFac_dvd _)]
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := minFac (k + 2)
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0 * m
⊢ False
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := minFac (k + 2)
this : (k + 2) / m < k + 2
h : (k + 2) / m = 0
⊢ False
have : (k + 2) = 0 * m := (Nat.div_eq_iff_eq_mul_left (minFac_pos _) (minFac_dvd _)).1 h
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := minFac (k + 2)
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0
⊢ False
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := minFac (k + 2)
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0 * m
⊢ False
rw [zero_mul] at this
no goals
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := minFac (k + 2)
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0
⊢ False
exact (show k + 2 ≠ 0 by simp) this
no goals
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := minFac (k + 2)
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0
⊢ k + 2 ≠ 0
simp