internlm/Lean-Github huggingface dataset:
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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'⟩
Proof 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'⟩))
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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']
Proof 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)))
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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
Proof 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)))
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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]
Proof 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)
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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
Proof 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)
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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]
Proof 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)
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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]
Proof 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
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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'
Proof 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
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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
Proof 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
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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)
Proof 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
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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'
Proof 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
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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 _
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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]
Proof 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
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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]
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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
Proof 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))
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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
Proof 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))
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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'⟩
Proof 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'⟩))
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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']
Proof 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)))
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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
Proof 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)))
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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]
Proof 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)
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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
Proof 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)
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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]
Proof 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))
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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
Proof 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))
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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]
Proof 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)
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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
Proof 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)
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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']
Proof 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)
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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
Proof state after:
no goals