have hd : 2 ^ pn.succ.succ ∣ prepend_one (2 ^ pn.succ * ↑pk) := by
  rw [prepend_one, hpk1, factor_ten_pow, ht]
  have h5 : 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1) =
        2^pn.succ * (2 * (2 * 5 ^ pn + t) + (5^pn + 1)) := by
    repeat rw[pow_succ]; ring_nf
  rw [h5]
  obtain ⟨k5,hk5⟩:= even_5_pow_plus_one pn
  rw [hk5]
  have h5' : 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + 2 * k5) =
       2^pn.succ.succ * (2 * 5 ^ pn + t + k5) := by
    repeat rw[pow_succ]; ring_nf
  rw [h5']
  exact Dvd.intro (2 * 5 ^ pn + t + k5) rfl
case succ.intro.intro.inr.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 + 1
⊢ ∃ 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.inr.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 + 1
hd : 2 ^ pn.succ.succ ∣ prepend_one (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))