have hd : 2 ^ pn.succ.succ ∣ prepend_two (2 ^ pn.succ * ↑pk) := by
  rw [prepend_two, factor_ten_pow, hpk1, ht]
  have hr : 2 * (2 ^ pn.succ * 5 ^ pn.succ) + 2 ^ pn.succ * (2 * t) =
               2 ^ pn.succ.succ * (5 ^ pn.succ + t) := by
    repeat rw [pow_succ]; ring_nf
  rw [hr]
  exact Dvd.intro (5 ^ Nat.succ pn + t) rfl
case succ.intro.intro.inl.intro
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t
⊢ ∃ k,
    (Nat.digits 10 (2 ^ (pn + 1).succ * ↑k)).length = (pn + 1).succ ∧
      all_one_or_two (Nat.digits 10 (2 ^ (pn + 1).succ * ↑k))
case succ.intro.intro.inl.intro
pn : ℕ
pk : ℕ+
hpk1 : (Nat.digits 10 (2 ^ pn.succ * ↑pk)).length = pn.succ
hpk2 : all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑pk))
t : ℕ
ht : ↑pk = 2 * t
hd : 2 ^ pn.succ.succ ∣ prepend_two (2 ^ pn.succ * ↑pk)
⊢ ∃ k,
    (Nat.digits 10 (2 ^ (pn + 1).succ * ↑k)).length = (pn + 1).succ ∧
      all_one_or_two (Nat.digits 10 (2 ^ (pn + 1).succ * ↑k))