p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ factors p = [p]
p : ℕ
hp : Prime p
⊢ factors p = [p]
have : p = p - 2 + 2 := (tsub_eq_iff_eq_add_of_le hp.two_le).mp rfl
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ (let m := minFac (p - 2 + 2);
    let_fun this := (_ : (p - 2 + 2) / minFac (p - 2 + 2) < p - 2 + 2);
    m :: factors ((p - 2 + 2) / m)) =
    [p - 2 + 2]
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ factors p = [p]
rw [this, Nat.factors]
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ minFac p :: factors (p / minFac p) = [p]
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ (let m := minFac (p - 2 + 2);
    let_fun this := (_ : (p - 2 + 2) / minFac (p - 2 + 2) < p - 2 + 2);
    m :: factors ((p - 2 + 2) / m)) =
    [p - 2 + 2]
simp only [Eq.symm this]
p : ℕ
hp : Prime p
this✝ : p = p - 2 + 2
this : minFac p = p
⊢ minFac p :: factors (p / minFac p) = [p]
p : ℕ
hp : Prime p
this : p = p - 2 + 2
⊢ minFac p :: factors (p / minFac p) = [p]
have : Nat.minFac p = p := (Nat.prime_def_minFac.mp hp).2
no goals
p : ℕ
hp : Prime p
this✝ : p = p - 2 + 2
this : minFac p = p
⊢ minFac p :: factors (p / minFac p) = [p]
simp only [this, Nat.factors, Nat.div_self (Nat.Prime.pos hp)]