English
For any positive number n, the cast of its minimal factor equals Nat.minFac applied to n.
Русский
Пусть n — положительное число. Отображение минимального делителя: (minFac n : ℕ) = Nat.minFac n.
LaTeX
$$$$\forall n \in \mathrm{PosNum},\ (\operatorname{minFac}~n:\mathbb{N}) = \operatorname{Nat}.minFac(n).$$$$
Lean4
@[simp]
theorem minFac_to_nat (n : PosNum) : (minFac n : ℕ) = Nat.minFac n :=
by
obtain - | n := n
· simp [minFac]
· rw [minFac, Nat.minFac_eq, if_neg]
swap
· simp [← two_mul]
rw [minFacAux_to_nat]
· rfl
simp only [cast_one, cast_bit1]
rw [Nat.sqrt_lt]
calc
(n : ℕ) + (n : ℕ) + 1 ≤ (n : ℕ) + (n : ℕ) + (n : ℕ) := by simp
_ = (n : ℕ) * (1 + 1 + 1) := by simp only [mul_add, mul_one]
_ < _ := by simp [mul_lt_mul]
· rw [minFac, Nat.minFac_eq, if_pos]
· rfl
simp [← two_mul]
