English
If the fuel bound h allows, then casting the result of minFacAux(n,fuel,k) to ℕ agrees with Nat.minFacAux(n,k.bit1).
Русский
При условии ограничения по топливу h результат minFacAux(n,fuel,k) приводится к ℕ так, что равенство выполняется: (minFacAux n fuel k) в ℕ равно Nat.minFacAux n k.bit1.
LaTeX
$$$$\forall {\text{fuel} : \mathbb{N}} {n k : \mathrm{PosNum}}\ (\mathrm{sqrt}\ n <\text{fuel} + k.\text{bit1})\ \Rightarrow\ (\minFacAux(n,\text{fuel},k) : \mathbb{N}) = \operatorname{Nat}.minFacAux(n,k.\text{bit1}).$$$$
Lean4
theorem minFacAux_to_nat {fuel : ℕ} {n k : PosNum} (h : Nat.sqrt n < fuel + k.bit1) :
(minFacAux n fuel k : ℕ) = Nat.minFacAux n k.bit1 :=
by
induction fuel generalizing k <;> rw [minFacAux, Nat.minFacAux]
case zero =>
rw [Nat.zero_add, Nat.sqrt_lt] at h
simp only [h, ite_true]
case succ fuel ih =>
simp_rw [← mul_to_nat]
simp only [cast_lt, dvd_to_nat]
split_ifs <;> try rfl
rw [ih] <;> [congr; convert Nat.lt_succ_of_lt h using 1] <;>
simp only [cast_bit1, cast_succ, Nat.succ_eq_add_one, add_assoc, add_left_comm, ← one_add_one_eq_two]
