Theorem: ZerosOnesAndTwos.ones_and_twos_aux (Compfiles/ZeroesOnesAndTwos.lean)

State before:
n : ℕ
⊢ ∃ k, (Nat.digits 10 (2 ^ n.succ * ↑k)).length = n.succ ∧ all_one_or_two (Nat.digits 10 (2 ^ n.succ * ↑k))
Tactic:
induction' n with pn hpn
State after:
case zero

⊢ ∃ k, (Nat.digits 10 (2 ^ Nat.succ 0 * ↑k)).length = Nat.succ 0 ∧ all_one_or_two (Nat.digits 10 (2 ^ Nat.succ 0 * ↑k))

case succ
pn : ℕ
hpn : ∃ k, (Nat.digits 10 (2 ^ pn.succ * ↑k)).length = pn.succ ∧ all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑k))
⊢ ∃ 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))

State before:
case succ
pn : ℕ
hpn : ∃ k, (Nat.digits 10 (2 ^ pn.succ * ↑k)).length = pn.succ ∧ all_one_or_two (Nat.digits 10 (2 ^ pn.succ * ↑k))
⊢ ∃ 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))
Tactic:
obtain ⟨pk, hpk1, hpk2⟩ := hpn
State after:
case succ.intro.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))
⊢ ∃ 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))

State before:
case succ.intro.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))
⊢ ∃ 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))
Tactic:
obtain ⟨t, ht : ↑pk = t + t⟩ | ⟨t, ht : ↑pk = 2 * t + 1⟩ := (pk : ℕ).even_or_odd
State after:
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 = t + 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.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))

State before:
case zero

⊢ ∃ k, (Nat.digits 10 (2 ^ Nat.succ 0 * ↑k)).length = Nat.succ 0 ∧ all_one_or_two (Nat.digits 10 (2 ^ Nat.succ 0 * ↑k))
Tactic:
use 1
State after:
case h

⊢ (Nat.digits 10 (2 ^ Nat.succ 0 * ↑1)).length = Nat.succ 0 ∧ all_one_or_two (Nat.digits 10 (2 ^ Nat.succ 0 * ↑1))

State before:
case h

⊢ (Nat.digits 10 (2 ^ Nat.succ 0 * ↑1)).length = Nat.succ 0 ∧ all_one_or_two (Nat.digits 10 (2 ^ Nat.succ 0 * ↑1))
Tactic:
norm_num [all_one_or_two]
State after:
no goals

State before:
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 = t + 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))
Tactic:
rw [← two_mul] at ht
State after:
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))

State before:
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))
Tactic:
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
State after:
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))

State before:
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))
Tactic:
obtain ⟨k', hk'⟩ := hd
State after:
case succ.intro.intro.inl.intro.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' : ℕ
hk' : prepend_two (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * k'
⊢ ∃ 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))

State before:
case succ.intro.intro.inl.intro.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' : ℕ
hk' : prepend_two (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * k'
hkp' : 0 < k'
⊢ ∃ 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))
Tactic:
use ⟨k', hkp'⟩
State after:
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
k' : ℕ
hk' : prepend_two (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'⟩))

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

State before:
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
k' : ℕ
hk' : prepend_two (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * k'
hkp' : 0 < k'
⊢ (Nat.digits 10 (prepend_two (2 ^ pn.succ * ↑pk))).length = (pn + 1).succ ∧
    all_one_or_two (Nat.digits 10 (prepend_two (2 ^ pn.succ * ↑pk)))
Tactic:
constructor
State after:
case h.left
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' : ℕ
hk' : prepend_two (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * k'
hkp' : 0 < k'
⊢ (Nat.digits 10 (prepend_two (2 ^ pn.succ * ↑pk))).length = (pn + 1).succ

case h.right
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' : ℕ
hk' : prepend_two (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * k'
hkp' : 0 < k'
⊢ all_one_or_two (Nat.digits 10 (prepend_two (2 ^ pn.succ * ↑pk)))

State before:
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
⊢ 2 ^ pn.succ.succ ∣ prepend_two (2 ^ pn.succ * ↑pk)
Tactic:
rw [prepend_two, factor_ten_pow, hpk1, ht]
State after:
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
⊢ 2 ^ pn.succ.succ ∣ 2 * (2 ^ pn.succ * 5 ^ pn.succ) + 2 ^ pn.succ * (2 * t)

State before:
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
⊢ 2 ^ pn.succ.succ ∣ 2 * (2 ^ pn.succ * 5 ^ pn.succ) + 2 ^ pn.succ * (2 * t)
Tactic:
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
State after:
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
hr : 2 * (2 ^ pn.succ * 5 ^ pn.succ) + 2 ^ pn.succ * (2 * t) = 2 ^ pn.succ.succ * (5 ^ pn.succ + t)
⊢ 2 ^ pn.succ.succ ∣ 2 * (2 ^ pn.succ * 5 ^ pn.succ) + 2 ^ pn.succ * (2 * t)

State before:
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
hr : 2 * (2 ^ pn.succ * 5 ^ pn.succ) + 2 ^ pn.succ * (2 * t) = 2 ^ pn.succ.succ * (5 ^ pn.succ + t)
⊢ 2 ^ pn.succ.succ ∣ 2 * (2 ^ pn.succ * 5 ^ pn.succ) + 2 ^ pn.succ * (2 * t)
Tactic:
rw [hr]
State after:
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
hr : 2 * (2 ^ pn.succ * 5 ^ pn.succ) + 2 ^ pn.succ * (2 * t) = 2 ^ pn.succ.succ * (5 ^ pn.succ + t)
⊢ 2 ^ pn.succ.succ ∣ 2 ^ pn.succ.succ * (5 ^ pn.succ + t)

State before:
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
hr : 2 * (2 ^ pn.succ * 5 ^ pn.succ) + 2 ^ pn.succ * (2 * t) = 2 ^ pn.succ.succ * (5 ^ pn.succ + t)
⊢ 2 ^ pn.succ.succ ∣ 2 ^ pn.succ.succ * (5 ^ pn.succ + t)
Tactic:
exact Dvd.intro (5 ^ Nat.succ pn + t) rfl
State after:
no goals

State before:
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
⊢ 2 * (2 ^ pn.succ * 5 ^ pn.succ) + 2 ^ pn.succ * (2 * t) = 2 ^ pn.succ.succ * (5 ^ pn.succ + t)
Tactic:
repeat rw [pow_succ]; ring_nf
State after:
no goals

State before:
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
⊢ t * 2 ^ pn * 4 + 2 ^ pn * 5 ^ pn * 20 = t * 2 ^ pn.succ.succ + 2 ^ pn.succ.succ * 5 ^ pn * 5
Tactic:
rw [pow_succ]
State after:
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
⊢ t * 2 ^ pn * 4 + 2 ^ pn * 5 ^ pn * 20 = t * (2 ^ (pn + 1) * 2) + 2 ^ (pn + 1) * 2 * 5 ^ pn * 5

State before:
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
⊢ t * 2 ^ pn * 4 + 2 ^ pn * 5 ^ pn * 20 = t * (2 ^ (pn + 1) * 2) + 2 ^ (pn + 1) * 2 * 5 ^ pn * 5
Tactic:
ring_nf
State after:
no goals

State before:
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' : ℕ
hk' : prepend_two (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * k'
⊢ 0 < k'
Tactic:
cases' k'
State after:
case zero
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
hk' : prepend_two (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * 0
⊢ 0 < 0

case succ
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
n✝ : ℕ
hk' : prepend_two (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * (n✝ + 1)
⊢ 0 < n✝ + 1

State before:
case zero
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
hk' : prepend_two (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * 0
⊢ 0 < 0
Tactic:
exfalso
State after:
case zero
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
hk' : prepend_two (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * 0
⊢ False

State before:
case zero
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
hk' : prepend_two (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * 0
⊢ False
Tactic:
have hzz := prepend_two_pos (2 ^ pn.succ * ↑pk)
State after:
case zero
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
hk' : prepend_two (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * 0
hzz : 0 < prepend_two (2 ^ pn.succ * ↑pk)
⊢ False

State before:
case zero
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
hk' : prepend_two (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * 0
hzz : 0 < prepend_two (2 ^ pn.succ * ↑pk)
⊢ False
Tactic:
rw [Nat.mul_zero] at hk'
State after:
case zero
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
hk' : prepend_two (2 ^ pn.succ * ↑pk) = 0
hzz : 0 < prepend_two (2 ^ pn.succ * ↑pk)
⊢ False

State before:
case zero
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
hk' : prepend_two (2 ^ pn.succ * ↑pk) = 0
hzz : 0 < prepend_two (2 ^ pn.succ * ↑pk)
⊢ False
Tactic:
omega
State after:
no goals

State before:
case succ
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
n✝ : ℕ
hk' : prepend_two (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * (n✝ + 1)
⊢ 0 < n✝ + 1
Tactic:
exact Nat.succ_pos _
State after:
no goals

State before:
case h.left
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' : ℕ
hk' : prepend_two (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * k'
hkp' : 0 < k'
⊢ (Nat.digits 10 (prepend_two (2 ^ pn.succ * ↑pk))).length = (pn + 1).succ
Tactic:
rw [prepend_two_eq_append]
State after:
case h.left
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' : ℕ
hk' : prepend_two (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * k'
hkp' : 0 < k'
⊢ (Nat.digits 10 (2 ^ pn.succ * ↑pk) ++ [2]).length = (pn + 1).succ

State before:
case h.left
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' : ℕ
hk' : prepend_two (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * k'
hkp' : 0 < k'
⊢ (Nat.digits 10 (2 ^ pn.succ * ↑pk) ++ [2]).length = (pn + 1).succ
Tactic:
rw [List.length_append, List.length_singleton, hpk1]
State after:
no goals

State before:
case h.right
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' : ℕ
hk' : prepend_two (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * k'
hkp' : 0 < k'
⊢ all_one_or_two (Nat.digits 10 (prepend_two (2 ^ pn.succ * ↑pk)))
Tactic:
exact prepend_two_all_one_or_two _ hpk2
State after:
no goals

State before:
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))
Tactic:
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
State after:
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))

State before:
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))
Tactic:
obtain ⟨k', hk'⟩ := hd
State after:
case succ.intro.intro.inr.intro.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' : ℕ
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * k'
⊢ ∃ 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))

State before:
case succ.intro.intro.inr.intro.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' : ℕ
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * k'
hkp' : 0 < k'
⊢ ∃ 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))
Tactic:
use ⟨k', hkp'⟩
State after:
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'⟩))

State before:
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'⟩))
Tactic:
rw [PNat.mk_coe,←hk']
State after:
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)))

State before:
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)))
Tactic:
constructor
State after:
case h.left
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

case h.right
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'
⊢ all_one_or_two (Nat.digits 10 (prepend_one (2 ^ pn.succ * ↑pk)))

State before:
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
⊢ 2 ^ pn.succ.succ ∣ prepend_one (2 ^ pn.succ * ↑pk)
Tactic:
rw [prepend_one, hpk1, factor_ten_pow, ht]
State after:
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
⊢ 2 ^ pn.succ.succ ∣ 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1)

State before:
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
⊢ 2 ^ pn.succ.succ ∣ 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1)
Tactic:
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
State after:
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
h5 : 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1) = 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
⊢ 2 ^ pn.succ.succ ∣ 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1)

State before:
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
h5 : 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1) = 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
⊢ 2 ^ pn.succ.succ ∣ 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1)
Tactic:
rw [h5]
State after:
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
h5 : 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1) = 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
⊢ 2 ^ pn.succ.succ ∣ 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))

State before:
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
h5 : 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1) = 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
⊢ 2 ^ pn.succ.succ ∣ 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
Tactic:
obtain ⟨k5,hk5⟩:= even_5_pow_plus_one pn
State after:
case 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
h5 : 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1) = 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
k5 : ℕ
hk5 : 5 ^ pn + 1 = 2 * k5
⊢ 2 ^ pn.succ.succ ∣ 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))

State before:
case 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
h5 : 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1) = 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
k5 : ℕ
hk5 : 5 ^ pn + 1 = 2 * k5
⊢ 2 ^ pn.succ.succ ∣ 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
Tactic:
rw [hk5]
State after:
case 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
h5 : 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1) = 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
k5 : ℕ
hk5 : 5 ^ pn + 1 = 2 * k5
⊢ 2 ^ pn.succ.succ ∣ 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + 2 * k5)

State before:
case 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
h5 : 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1) = 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
k5 : ℕ
hk5 : 5 ^ pn + 1 = 2 * k5
⊢ 2 ^ pn.succ.succ ∣ 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + 2 * k5)
Tactic:
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
State after:
case 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
h5 : 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1) = 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
k5 : ℕ
hk5 : 5 ^ pn + 1 = 2 * k5
h5' : 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + 2 * k5) = 2 ^ pn.succ.succ * (2 * 5 ^ pn + t + k5)
⊢ 2 ^ pn.succ.succ ∣ 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + 2 * k5)

State before:
case 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
h5 : 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1) = 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
k5 : ℕ
hk5 : 5 ^ pn + 1 = 2 * k5
h5' : 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + 2 * k5) = 2 ^ pn.succ.succ * (2 * 5 ^ pn + t + k5)
⊢ 2 ^ pn.succ.succ ∣ 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + 2 * k5)
Tactic:
rw [h5']
State after:
case 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
h5 : 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1) = 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
k5 : ℕ
hk5 : 5 ^ pn + 1 = 2 * k5
h5' : 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + 2 * k5) = 2 ^ pn.succ.succ * (2 * 5 ^ pn + t + k5)
⊢ 2 ^ pn.succ.succ ∣ 2 ^ pn.succ.succ * (2 * 5 ^ pn + t + k5)

State before:
case 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
h5 : 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1) = 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
k5 : ℕ
hk5 : 5 ^ pn + 1 = 2 * k5
h5' : 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + 2 * k5) = 2 ^ pn.succ.succ * (2 * 5 ^ pn + t + k5)
⊢ 2 ^ pn.succ.succ ∣ 2 ^ pn.succ.succ * (2 * 5 ^ pn + t + k5)
Tactic:
exact Dvd.intro (2 * 5 ^ pn + t + k5) rfl
State after:
no goals

State before:
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
⊢ 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1) = 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
Tactic:
repeat rw[pow_succ]; ring_nf
State after:
no goals

State before:
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
⊢ t * 2 ^ pn * 4 + 2 ^ pn * 2 + 2 ^ pn * 5 ^ pn.succ * 2 = t * 2 ^ pn * 4 + 2 ^ pn * 2 + 2 ^ pn * 5 ^ pn * 10
Tactic:
rw[pow_succ]
State after:
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
⊢ t * 2 ^ pn * 4 + 2 ^ pn * 2 + 2 ^ pn * (5 ^ pn * 5) * 2 = t * 2 ^ pn * 4 + 2 ^ pn * 2 + 2 ^ pn * 5 ^ pn * 10

State before:
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
⊢ t * 2 ^ pn * 4 + 2 ^ pn * 2 + 2 ^ pn * (5 ^ pn * 5) * 2 = t * 2 ^ pn * 4 + 2 ^ pn * 2 + 2 ^ pn * 5 ^ pn * 10
Tactic:
ring_nf
State after:
no goals

State before:
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
h5 : 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1) = 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
k5 : ℕ
hk5 : 5 ^ pn + 1 = 2 * k5
⊢ 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + 2 * k5) = 2 ^ pn.succ.succ * (2 * 5 ^ pn + t + k5)
Tactic:
repeat rw[pow_succ]; ring_nf
State after:
no goals

State before:
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
h5 : 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1) = 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
k5 : ℕ
hk5 : 5 ^ pn + 1 = 2 * k5
⊢ t * 2 ^ pn * 4 + k5 * 2 ^ pn * 4 + 2 ^ pn * 5 ^ pn * 8 =
    t * 2 ^ pn.succ.succ + k5 * 2 ^ pn.succ.succ + 2 ^ pn.succ.succ * 5 ^ pn * 2
Tactic:
rw[pow_succ]
State after:
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
h5 : 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1) = 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
k5 : ℕ
hk5 : 5 ^ pn + 1 = 2 * k5
⊢ t * 2 ^ pn * 4 + k5 * 2 ^ pn * 4 + 2 ^ pn * 5 ^ pn * 8 =
    t * (2 ^ (pn + 1) * 2) + k5 * (2 ^ (pn + 1) * 2) + 2 ^ (pn + 1) * 2 * 5 ^ pn * 2

State before:
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
h5 : 2 ^ pn.succ * 5 ^ pn.succ + 2 ^ pn.succ * (2 * t + 1) = 2 ^ pn.succ * (2 * (2 * 5 ^ pn + t) + (5 ^ pn + 1))
k5 : ℕ
hk5 : 5 ^ pn + 1 = 2 * k5
⊢ t * 2 ^ pn * 4 + k5 * 2 ^ pn * 4 + 2 ^ pn * 5 ^ pn * 8 =
    t * (2 ^ (pn + 1) * 2) + k5 * (2 ^ (pn + 1) * 2) + 2 ^ (pn + 1) * 2 * 5 ^ pn * 2
Tactic:
ring_nf
State after:
no goals

State before:
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'
⊢ 0 < k'
Tactic:
cases k'
State after:
case zero
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
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * 0
⊢ 0 < 0

case succ
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
n✝ : ℕ
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * (n✝ + 1)
⊢ 0 < n✝ + 1

State before:
case zero
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
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * 0
⊢ 0 < 0
Tactic:
exfalso
State after:
case zero
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
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * 0
⊢ False

State before:
case zero
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
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * 0
⊢ False
Tactic:
have hzz := prepend_one_pos (2 ^ pn.succ * ↑pk)
State after:
case zero
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
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * 0
hzz : 0 < prepend_one (2 ^ pn.succ * ↑pk)
⊢ False

State before:
case zero
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
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * 0
hzz : 0 < prepend_one (2 ^ pn.succ * ↑pk)
⊢ False
Tactic:
rw[Nat.mul_zero] at hk'
State after:
case zero
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
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 0
hzz : 0 < prepend_one (2 ^ pn.succ * ↑pk)
⊢ False

State before:
case zero
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
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 0
hzz : 0 < prepend_one (2 ^ pn.succ * ↑pk)
⊢ False
Tactic:
omega
State after:
no goals

State before:
case succ
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
n✝ : ℕ
hk' : prepend_one (2 ^ pn.succ * ↑pk) = 2 ^ pn.succ.succ * (n✝ + 1)
⊢ 0 < n✝ + 1
Tactic:
exact Nat.succ_pos _
State after:
no goals

State before:
case h.left
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
Tactic:
rw [prepend_one_eq_append]
State after:
case h.left
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.succ * ↑pk) ++ [1]).length = (pn + 1).succ

State before:
case h.left
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.succ * ↑pk) ++ [1]).length = (pn + 1).succ
Tactic:
rw [List.length_append, List.length_singleton, hpk1]
State after:
no goals

State before:
case h.right
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'
⊢ all_one_or_two (Nat.digits 10 (prepend_one (2 ^ pn.succ * ↑pk)))
Tactic:
exact prepend_one_all_one_or_two _ hpk2
State after:
no goals