[GOAL]
fuel : ℕ
n k : PosNum
h : Nat.sqrt ↑n < fuel + ↑(bit1 k)
⊢ ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
[PROOFSTEP]
induction' fuel with fuel ih generalizing k
[GOAL]
case zero
fuel : ℕ
n k✝ : PosNum
h✝ : Nat.sqrt ↑n < fuel + ↑(bit1 k✝)
k : PosNum
h : Nat.sqrt ↑n < Nat.zero + ↑(bit1 k)
⊢ ↑(minFacAux n Nat.zero k) = Nat.minFacAux ↑n ↑(bit1 k)
[PROOFSTEP]
rw [minFacAux, Nat.minFacAux]
[GOAL]
case succ
fuel✝ : ℕ
n k✝ : PosNum
h✝ : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
⊢ ↑(minFacAux n (Nat.succ fuel) k) = Nat.minFacAux ↑n ↑(bit1 k)
[PROOFSTEP]
rw [minFacAux, Nat.minFacAux]
[GOAL]
case zero
fuel : ℕ
n k✝ : PosNum
h✝ : Nat.sqrt ↑n < fuel + ↑(bit1 k✝)
k : PosNum
h : Nat.sqrt ↑n < Nat.zero + ↑(bit1 k)
⊢ ↑n =
    if h : ↑n < ↑(bit1 k) * ↑(bit1 k) then ↑n
    else
      if ↑(bit1 k) ∣ ↑n then ↑(bit1 k)
      else
        let_fun this := (_ : Nat.sqrt ↑n - ↑(bit1 k) < Nat.sqrt ↑n + 2 - ↑(bit1 k));
        Nat.minFacAux (↑n) (↑(bit1 k) + 2)
[PROOFSTEP]
rw [Nat.zero_add, Nat.sqrt_lt] at h 
[GOAL]
case zero
fuel : ℕ
n k✝ : PosNum
h✝ : Nat.sqrt ↑n < fuel + ↑(bit1 k✝)
k : PosNum
h : ↑n < ↑(bit1 k) * ↑(bit1 k)
⊢ ↑n =
    if h : ↑n < ↑(bit1 k) * ↑(bit1 k) then ↑n
    else
      if ↑(bit1 k) ∣ ↑n then ↑(bit1 k)
      else
        let_fun this := (_ : Nat.sqrt ↑n - ↑(bit1 k) < Nat.sqrt ↑n + 2 - ↑(bit1 k));
        Nat.minFacAux (↑n) (↑(bit1 k) + 2)
[PROOFSTEP]
simp only [h, dite_true]
[GOAL]
case succ
fuel✝ : ℕ
n k✝ : PosNum
h✝ : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
⊢ ↑(if n < bit1 k * bit1 k then n else if bit1 k ∣ n then bit1 k else minFacAux n fuel (succ k)) =
    if h : ↑n < ↑(bit1 k) * ↑(bit1 k) then ↑n
    else
      if ↑(bit1 k) ∣ ↑n then ↑(bit1 k)
      else
        let_fun this := (_ : Nat.sqrt ↑n - ↑(bit1 k) < Nat.sqrt ↑n + 2 - ↑(bit1 k));
        Nat.minFacAux (↑n) (↑(bit1 k) + 2)
[PROOFSTEP]
simp_rw [← mul_to_nat]
[GOAL]
case succ
fuel✝ : ℕ
n k✝ : PosNum
h✝ : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
⊢ ↑(if n < bit1 k * bit1 k then n else if bit1 k ∣ n then bit1 k else minFacAux n fuel (succ k)) =
    if h : ↑n < ↑(bit1 k * bit1 k) then ↑n else if ↑(bit1 k) ∣ ↑n then ↑(bit1 k) else Nat.minFacAux (↑n) (↑(bit1 k) + 2)
[PROOFSTEP]
simp only [cast_lt, dvd_to_nat]
[GOAL]
case succ
fuel✝ : ℕ
n k✝ : PosNum
h✝ : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
⊢ ↑(if n < bit1 k * bit1 k then n else if bit1 k ∣ n then bit1 k else minFacAux n fuel (succ k)) =
    if h : n < bit1 k * bit1 k then ↑n else if bit1 k ∣ n then ↑(bit1 k) else Nat.minFacAux (↑n) (↑(bit1 k) + 2)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
fuel✝ : ℕ
n k✝ : PosNum
h✝¹ : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝ : n < bit1 k * bit1 k
⊢ ↑n = ↑n
[PROOFSTEP]
try rfl
[GOAL]
case pos
fuel✝ : ℕ
n k✝ : PosNum
h✝¹ : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝ : n < bit1 k * bit1 k
⊢ ↑n = ↑n
[PROOFSTEP]
rfl
[GOAL]
case pos
fuel✝ : ℕ
n k✝ : PosNum
h✝² : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝¹ : ¬n < bit1 k * bit1 k
h✝ : bit1 k ∣ n
⊢ ↑(bit1 k) = ↑(bit1 k)
[PROOFSTEP]
try rfl
[GOAL]
case pos
fuel✝ : ℕ
n k✝ : PosNum
h✝² : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝¹ : ¬n < bit1 k * bit1 k
h✝ : bit1 k ∣ n
⊢ ↑(bit1 k) = ↑(bit1 k)
[PROOFSTEP]
rfl
[GOAL]
case neg
fuel✝ : ℕ
n k✝ : PosNum
h✝² : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝¹ : ¬n < bit1 k * bit1 k
h✝ : ¬bit1 k ∣ n
⊢ ↑(minFacAux n fuel (succ k)) = Nat.minFacAux (↑n) (↑(bit1 k) + 2)
[PROOFSTEP]
try rfl
[GOAL]
case neg
fuel✝ : ℕ
n k✝ : PosNum
h✝² : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝¹ : ¬n < bit1 k * bit1 k
h✝ : ¬bit1 k ∣ n
⊢ ↑(minFacAux n fuel (succ k)) = Nat.minFacAux (↑n) (↑(bit1 k) + 2)
[PROOFSTEP]
rfl
[GOAL]
case neg
fuel✝ : ℕ
n k✝ : PosNum
h✝² : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝¹ : ¬n < bit1 k * bit1 k
h✝ : ¬bit1 k ∣ n
⊢ ↑(minFacAux n fuel (succ k)) = Nat.minFacAux (↑n) (↑(bit1 k) + 2)
[PROOFSTEP]
rw [ih] <;> [congr; convert Nat.lt_succ_of_lt h using 1]
[GOAL]
case neg
fuel✝ : ℕ
n k✝ : PosNum
h✝² : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝¹ : ¬n < bit1 k * bit1 k
h✝ : ¬bit1 k ∣ n
⊢ ↑(minFacAux n fuel (succ k)) = Nat.minFacAux (↑n) (↑(bit1 k) + 2)
[PROOFSTEP]
rw [ih]
[GOAL]
case neg
fuel✝ : ℕ
n k✝ : PosNum
h✝² : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝¹ : ¬n < bit1 k * bit1 k
h✝ : ¬bit1 k ∣ n
⊢ Nat.minFacAux ↑n ↑(bit1 (succ k)) = Nat.minFacAux (↑n) (↑(bit1 k) + 2)
[PROOFSTEP]
congr
[GOAL]
case neg
fuel✝ : ℕ
n k✝ : PosNum
h✝² : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝¹ : ¬n < bit1 k * bit1 k
h✝ : ¬bit1 k ∣ n
⊢ Nat.sqrt ↑n < fuel + ↑(bit1 (succ k))
[PROOFSTEP]
convert Nat.lt_succ_of_lt h using 1
[GOAL]
case neg.e_a
fuel✝ : ℕ
n k✝ : PosNum
h✝² : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝¹ : ¬n < bit1 k * bit1 k
h✝ : ¬bit1 k ∣ n
⊢ ↑(bit1 (succ k)) = ↑(bit1 k) + 2
[PROOFSTEP]
simp only [_root_.bit1, _root_.bit0, cast_bit1, cast_succ, Nat.succ_eq_add_one, add_assoc, add_left_comm, ←
  one_add_one_eq_two]
[GOAL]
case h.e'_4
fuel✝ : ℕ
n k✝ : PosNum
h✝² : Nat.sqrt ↑n < fuel✝ + ↑(bit1 k✝)
fuel : ℕ
ih : ∀ {k : PosNum}, Nat.sqrt ↑n < fuel + ↑(bit1 k) → ↑(minFacAux n fuel k) = Nat.minFacAux ↑n ↑(bit1 k)
k : PosNum
h : Nat.sqrt ↑n < Nat.succ fuel + ↑(bit1 k)
h✝¹ : ¬n < bit1 k * bit1 k
h✝ : ¬bit1 k ∣ n
⊢ fuel + ↑(bit1 (succ k)) = Nat.succ (Nat.succ fuel + ↑(bit1 k))
[PROOFSTEP]
simp only [_root_.bit1, _root_.bit0, cast_bit1, cast_succ, Nat.succ_eq_add_one, add_assoc, add_left_comm, ←
  one_add_one_eq_two]
[GOAL]
n : PosNum
⊢ ↑(minFac n) = Nat.minFac ↑n
[PROOFSTEP]
cases' n with n
[GOAL]
case one
⊢ ↑(minFac one) = Nat.minFac ↑one
[PROOFSTEP]
rfl
[GOAL]
case bit1
n : PosNum
⊢ ↑(minFac (bit1 n)) = Nat.minFac ↑(bit1 n)
[PROOFSTEP]
rw [minFac, Nat.minFac_eq, if_neg]
[GOAL]
case bit1
n : PosNum
⊢ ↑(match bit1 n with
      | one => 1
      | bit0 a => 2
      | bit1 n => minFacAux (bit1 n) (↑n) 1) =
    Nat.minFacAux (↑(bit1 n)) 3
case bit1.hnc n : PosNum ⊢ ¬2 ∣ ↑(bit1 n)
[PROOFSTEP]
swap
[GOAL]
case bit1.hnc
n : PosNum
⊢ ¬2 ∣ ↑(bit1 n)
[PROOFSTEP]
simp
[GOAL]
case bit1
n : PosNum
⊢ ↑(match bit1 n with
      | one => 1
      | bit0 a => 2
      | bit1 n => minFacAux (bit1 n) (↑n) 1) =
    Nat.minFacAux (↑(bit1 n)) 3
[PROOFSTEP]
rw [minFacAux_to_nat]
[GOAL]
case bit1
n : PosNum
⊢ Nat.minFacAux ↑(bit1 n) ↑(bit1 1) = Nat.minFacAux (↑(bit1 n)) 3
[PROOFSTEP]
rfl
[GOAL]
case bit1
n : PosNum
⊢ Nat.sqrt ↑(bit1 n) < ↑n + ↑(bit1 1)
[PROOFSTEP]
simp only [cast_one, cast_bit1]
[GOAL]
case bit1
n : PosNum
⊢ Nat.sqrt (_root_.bit1 ↑n) < ↑n + _root_.bit1 1
[PROOFSTEP]
unfold _root_.bit1 _root_.bit0
[GOAL]
case bit1
n : PosNum
⊢ Nat.sqrt (↑n + ↑n + 1) < ↑n + (1 + 1 + 1)
[PROOFSTEP]
rw [Nat.sqrt_lt]
[GOAL]
case bit1
n : PosNum
⊢ ↑n + ↑n + 1 < (↑n + (1 + 1 + 1)) * (↑n + (1 + 1 + 1))
[PROOFSTEP]
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]
[GOAL]
n : PosNum
⊢ ↑n + ↑n + 1 ≤ ↑n + ↑n + ↑n
[PROOFSTEP]
simp
[GOAL]
n : PosNum
⊢ ↑n + ↑n + ↑n = ↑n * (1 + 1 + 1)
[PROOFSTEP]
simp only [mul_add, mul_one]
[GOAL]
n : PosNum
⊢ ↑n * (1 + 1 + 1) < (↑n + (1 + 1 + 1)) * (↑n + (1 + 1 + 1))
[PROOFSTEP]
simp [mul_lt_mul]
[GOAL]
case bit0
a✝ : PosNum
⊢ ↑(minFac (bit0 a✝)) = Nat.minFac ↑(bit0 a✝)
[PROOFSTEP]
rw [minFac, Nat.minFac_eq, if_pos]
[GOAL]
case bit0
a✝ : PosNum
⊢ ↑(match bit0 a✝ with
      | one => 1
      | bit0 a => 2
      | bit1 n => minFacAux (bit1 n) (↑n) 1) =
    2
[PROOFSTEP]
rfl
[GOAL]
case bit0.hc
a✝ : PosNum
⊢ 2 ∣ ↑(bit0 a✝)
[PROOFSTEP]
simp
[GOAL]
n : PosNum
⊢ Prime (bit0 n) ↔ n = 1
[PROOFSTEP]
refine' Nat.prime_def_minFac.trans ((and_iff_right _).trans <| eq_comm.trans _)
[GOAL]
case refine'_1
n : PosNum
⊢ 2 ≤ ↑(bit0 n)
[PROOFSTEP]
exact bit0_le_bit0.2 (Nat.succ_le_of_lt (to_nat_pos _))
[GOAL]
case refine'_2
n : PosNum
⊢ ↑(bit0 n) = Nat.minFac ↑(bit0 n) ↔ n = 1
[PROOFSTEP]
rw [← minFac_to_nat, to_nat_inj]
[GOAL]
case refine'_2
n : PosNum
⊢ bit0 n = minFac (bit0 n) ↔ n = 1
[PROOFSTEP]
exact ⟨bit0.inj, congr_arg _⟩
[GOAL]
n : PosNum
⊢ Prime (bit1 n) ↔ minFacAux (bit1 n) (↑n) 1 = bit1 n
[PROOFSTEP]
refine' Nat.prime_def_minFac.trans ((and_iff_right _).trans _)
[GOAL]
case refine'_1
n : PosNum
⊢ 2 ≤ ↑(bit1 n)
[PROOFSTEP]
exact Nat.bit0_le_bit1_iff.2 (to_nat_pos _)
[GOAL]
case refine'_2
n : PosNum
⊢ Nat.minFac ↑(bit1 n) = ↑(bit1 n) ↔ minFacAux (bit1 n) (↑n) 1 = bit1 n
[PROOFSTEP]
rw [← minFac_to_nat, to_nat_inj]
[GOAL]
case refine'_2
n : PosNum
⊢ minFac (bit1 n) = bit1 n ↔ minFacAux (bit1 n) (↑n) 1 = bit1 n
[PROOFSTEP]
rfl
