case one

⊢ ↑(minFac one) = Nat.minFac ↑one

case bit1
n : PosNum
⊢ ↑(minFac (bit1 n)) = Nat.minFac ↑(bit1 n)

case bit0
a✝ : PosNum
⊢ ↑(minFac (bit0 a✝)) = Nat.minFac ↑(bit0 a✝)
n : PosNum
⊢ ↑(minFac n) = Nat.minFac ↑n
cases' n with n
no goals
case one

⊢ ↑(minFac one) = Nat.minFac ↑one
rfl
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)
case bit1
n : PosNum
⊢ ↑(minFac (bit1 n)) = Nat.minFac ↑(bit1 n)
rw [minFac, Nat.minFac_eq, if_neg]
case bit1.hnc
n : PosNum
⊢ ¬2 ∣ ↑(bit1 n)

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
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)
swap
case bit1
n : PosNum
⊢ Nat.minFacAux ↑(bit1 n) ↑(bit1 1) = Nat.minFacAux (↑(bit1 n)) 3

case bit1
n : PosNum
⊢ Nat.sqrt ↑(bit1 n) < ↑n + ↑(bit1 1)
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
rw [minFacAux_to_nat]
case bit1
n : PosNum
⊢ Nat.sqrt (_root_.bit1 ↑n) < ↑n + _root_.bit1 1
case bit1
n : PosNum
⊢ Nat.sqrt ↑(bit1 n) < ↑n + ↑(bit1 1)
simp only [cast_one, cast_bit1]
case bit1
n : PosNum
⊢ Nat.sqrt (↑n + ↑n + 1) < ↑n + (1 + 1 + 1)
case bit1
n : PosNum
⊢ Nat.sqrt (_root_.bit1 ↑n) < ↑n + _root_.bit1 1
unfold _root_.bit1 _root_.bit0
case bit1
n : PosNum
⊢ ↑n + ↑n + 1 < (↑n + (1 + 1 + 1)) * (↑n + (1 + 1 + 1))
case bit1
n : PosNum
⊢ Nat.sqrt (↑n + ↑n + 1) < ↑n + (1 + 1 + 1)
rw [Nat.sqrt_lt]
no goals
case bit1
n : PosNum
⊢ ↑n + ↑n + 1 < (↑n + (1 + 1 + 1)) * (↑n + (1 + 1 + 1))
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]
no goals
case bit1.hnc
n : PosNum
⊢ ¬2 ∣ ↑(bit1 n)
simp
no goals
case bit1
n : PosNum
⊢ Nat.minFacAux ↑(bit1 n) ↑(bit1 1) = Nat.minFacAux (↑(bit1 n)) 3
rfl
no goals
n : PosNum
⊢ ↑n + ↑n + 1 ≤ ↑n + ↑n + ↑n
simp
no goals
n : PosNum
⊢ ↑n + ↑n + ↑n = ↑n * (1 + 1 + 1)
simp only [mul_add, mul_one]
no goals
n : PosNum
⊢ ↑n * (1 + 1 + 1) < (↑n + (1 + 1 + 1)) * (↑n + (1 + 1 + 1))
simp [mul_lt_mul]
case bit0
a✝ : PosNum
⊢ ↑(match bit0 a✝ with
      | one => 1
      | bit0 a => 2
      | bit1 n => minFacAux (bit1 n) (↑n) 1) =
    2

case bit0.hc
a✝ : PosNum
⊢ 2 ∣ ↑(bit0 a✝)
case bit0
a✝ : PosNum
⊢ ↑(minFac (bit0 a✝)) = Nat.minFac ↑(bit0 a✝)
rw [minFac, Nat.minFac_eq, if_pos]
no goals
case bit0.hc
a✝ : PosNum
⊢ 2 ∣ ↑(bit0 a✝)
simp
no goals
case bit0
a✝ : PosNum
⊢ ↑(match bit0 a✝ with
      | one => 1
      | bit0 a => 2
      | bit1 n => minFacAux (bit1 n) (↑n) 1) =
    2
rfl