rw [PNat.mk_coe,←hk']
case h
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' : ℕ
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * k'
hkp' : 0 < k'
⊢ (Nat.digits 10 (2 ^ (pn + 1).succ * ↑⟨k', hkp'⟩)).length = (pn + 1).succ ∧
    all_one_or_two (Nat.digits 10 (2 ^ (pn + 1).succ * ↑⟨k', hkp'⟩))
case h
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' : ℕ
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * k'
hkp' : 0 < k'
⊢ (Nat.digits 10 (prepend_one (2 ^ pn.succ * ↑pk))).length = (pn + 1).succ ∧
    all_one_or_two (Nat.digits 10 (prepend_one (2 ^ pn.succ * ↑pk)))