internlm/Lean-Github huggingface dataset:
Theorem: ZerosOnesAndTwos.prepend_one_eq_append
Proof state before:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_one m) = Nat.digits 10 m ++ [1]
⊢ prepend_one (n' + 1) % 10 :: Nat.digits 10 (prepend_one (n' + 1) / 10) = Nat.digits 10 (n' + 1) ++ [1]
Tactic:
rw [prepend_one_div _ (Nat.succ_pos n')]
Proof state after:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_one m) = Nat.digits 10 m ++ [1]
⊢ prepend_one (n' + 1) % 10 :: Nat.digits 10 (prepend_one (n'.succ / 10)) = Nat.digits 10 (n' + 1) ++ [1]
Theorem: ZerosOnesAndTwos.prepend_one_eq_append
Proof state before:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_one m) = Nat.digits 10 m ++ [1]
⊢ prepend_one (n' + 1) % 10 :: Nat.digits 10 (prepend_one (n'.succ / 10)) = Nat.digits 10 (n' + 1) ++ [1]
Tactic:
have hns : n'.succ / 10 < n'.succ := Nat.div_lt_self' n' 8
Proof state after:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_one m) = Nat.digits 10 m ++ [1]
hns : n'.succ / 10 < n'.succ
⊢ prepend_one (n' + 1) % 10 :: Nat.digits 10 (prepend_one (n'.succ / 10)) = Nat.digits 10 (n' + 1) ++ [1]
Theorem: ZerosOnesAndTwos.prepend_one_eq_append
Proof state before:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_one m) = Nat.digits 10 m ++ [1]
hns : n'.succ / 10 < n'.succ
⊢ prepend_one (n' + 1) % 10 :: Nat.digits 10 (prepend_one (n'.succ / 10)) = Nat.digits 10 (n' + 1) ++ [1]
Tactic:
rw [ih _ hns]
Proof state after:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_one m) = Nat.digits 10 m ++ [1]
hns : n'.succ / 10 < n'.succ
⊢ prepend_one (n' + 1) % 10 :: (Nat.digits 10 (n'.succ / 10) ++ [1]) = Nat.digits 10 (n' + 1) ++ [1]
Theorem: ZerosOnesAndTwos.prepend_one_eq_append
Proof state before:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_one m) = Nat.digits 10 m ++ [1]
hns : n'.succ / 10 < n'.succ
⊢ prepend_one (n' + 1) % 10 :: (Nat.digits 10 (n'.succ / 10) ++ [1]) = Nat.digits 10 (n' + 1) ++ [1]
Tactic:
rw [←List.cons_append]
Proof state after:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_one m) = Nat.digits 10 m ++ [1]
hns : n'.succ / 10 < n'.succ
⊢ prepend_one (n' + 1) % 10 :: Nat.digits 10 (n'.succ / 10) ++ [1] = Nat.digits 10 (n' + 1) ++ [1]
Theorem: ZerosOnesAndTwos.prepend_one_eq_append
Proof state before:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_one m) = Nat.digits 10 m ++ [1]
hns : n'.succ / 10 < n'.succ
⊢ prepend_one (n' + 1) % 10 :: Nat.digits 10 (n'.succ / 10) ++ [1] = Nat.digits 10 (n' + 1) ++ [1]
Tactic:
rw [prepend_one_mod _ (Nat.succ_pos _), Nat.digits_def' two_le_ten (Nat.succ_pos n')]
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.prepend_one_all_one_or_two
Proof state before:
n : ℕ
hn : all_one_or_two (Nat.digits 10 n)
⊢ all_one_or_two (Nat.digits 10 (prepend_one n))
Tactic:
rw [prepend_one_eq_append, all_one_or_two]
Proof state after:
n : ℕ
hn : all_one_or_two (Nat.digits 10 n)
⊢ ∀ e ∈ Nat.digits 10 n ++ [1], e = 1 ∨ e = 2
Theorem: ZerosOnesAndTwos.prepend_one_all_one_or_two
Proof state before:
n : ℕ
hn : all_one_or_two (Nat.digits 10 n)
⊢ ∀ e ∈ Nat.digits 10 n ++ [1], e = 1 ∨ e = 2
Tactic:
rw [all_one_or_two] at hn
Proof state after:
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
⊢ ∀ e ∈ Nat.digits 10 n ++ [1], e = 1 ∨ e = 2
Theorem: ZerosOnesAndTwos.prepend_one_all_one_or_two
Proof state before:
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
⊢ ∀ e ∈ Nat.digits 10 n ++ [1], e = 1 ∨ e = 2
Tactic:
intro e he
Proof state after:
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ Nat.digits 10 n ++ [1]
⊢ e = 1 ∨ e = 2
Theorem: ZerosOnesAndTwos.prepend_one_all_one_or_two
Proof state before:
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ Nat.digits 10 n ++ [1]
⊢ e = 1 ∨ e = 2
Tactic:
rw [List.mem_append] at he
Proof state after:
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ Nat.digits 10 n ∨ e ∈ [1]
⊢ e = 1 ∨ e = 2
Theorem: ZerosOnesAndTwos.prepend_one_all_one_or_two
Proof state before:
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ Nat.digits 10 n ∨ e ∈ [1]
⊢ e = 1 ∨ e = 2
Tactic:
cases' he with he he
Proof state after:
case inl
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ Nat.digits 10 n
⊢ e = 1 ∨ e = 2

case inr
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ [1]
⊢ e = 1 ∨ e = 2
Theorem: ZerosOnesAndTwos.prepend_one_all_one_or_two
Proof state before:
case inl
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ Nat.digits 10 n
⊢ e = 1 ∨ e = 2
Tactic:
exact hn e he
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.prepend_one_all_one_or_two
Proof state before:
case inr
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ [1]
⊢ e = 1 ∨ e = 2
Tactic:
rw [List.mem_singleton] at he
Proof state after:
case inr
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e = 1
⊢ e = 1 ∨ e = 2
Theorem: ZerosOnesAndTwos.prepend_one_all_one_or_two
Proof state before:
case inr
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e = 1
⊢ e = 1 ∨ e = 2
Tactic:
simp only [he, OfNat.one_ne_ofNat, or_false]
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.prepend_two_pos
Proof state before:
n : ℕ
⊢ 0 < prepend_two n
Tactic:
cases n
Proof state after:
case zero

⊢ 0 < prepend_two 0

case succ
n✝ : ℕ
⊢ 0 < prepend_two (n✝ + 1)
Theorem: ZerosOnesAndTwos.prepend_two_pos
Proof state before:
case zero

⊢ 0 < prepend_two 0
Tactic:
norm_num [prepend_two]
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.prepend_two_pos
Proof state before:
case succ
n✝ : ℕ
⊢ 0 < prepend_two (n✝ + 1)
Tactic:
rw [prepend_two]
Proof state after:
case succ
n✝ : ℕ
⊢ 0 < 2 * 10 ^ (Nat.digits 10 (n✝ + 1)).length + (n✝ + 1)
Theorem: ZerosOnesAndTwos.prepend_two_pos
Proof state before:
case succ
n✝ : ℕ
⊢ 0 < 2 * 10 ^ (Nat.digits 10 (n✝ + 1)).length + (n✝ + 1)
Tactic:
norm_num
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.prepend_two_div
Proof state before:
n : ℕ
hn : 0 < n
⊢ prepend_two n / 10 = prepend_two (n / 10)
Tactic:
rw [prepend_two, prepend_two]
Proof state after:
n : ℕ
hn : 0 < n
⊢ (2 * 10 ^ (Nat.digits 10 n).length + n) / 10 = 2 * 10 ^ (Nat.digits 10 (n / 10)).length + n / 10
Theorem: ZerosOnesAndTwos.prepend_two_div
Proof state before:
n : ℕ
hn : 0 < n
⊢ (2 * 10 ^ (Nat.digits 10 n).length + n) / 10 = 2 * 10 ^ (Nat.digits 10 (n / 10)).length + n / 10
Tactic:
cases' n with n
Proof state after:
case zero
hn : 0 < 0
⊢ (2 * 10 ^ (Nat.digits 10 0).length + 0) / 10 = 2 * 10 ^ (Nat.digits 10 (0 / 10)).length + 0 / 10

case succ
n : ℕ
hn : 0 < n + 1
⊢ (2 * 10 ^ (Nat.digits 10 (n + 1)).length + (n + 1)) / 10 =
    2 * 10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10
Theorem: ZerosOnesAndTwos.prepend_two_div
Proof state before:
case zero
hn : 0 < 0
⊢ (2 * 10 ^ (Nat.digits 10 0).length + 0) / 10 = 2 * 10 ^ (Nat.digits 10 (0 / 10)).length + 0 / 10
Tactic:
cases Nat.lt_asymm hn hn
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.prepend_two_div
Proof state before:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (2 * 10 ^ (Nat.digits 10 (n + 1)).length + (n + 1)) / 10 =
    2 * 10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10
Tactic:
rw [digits_len' n.succ (Nat.succ_pos n)]
Proof state after:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (2 * 10 ^ (1 + (Nat.digits 10 (n.succ / 10)).length) + (n + 1)) / 10 =
    2 * 10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10
Theorem: ZerosOnesAndTwos.prepend_two_div
Proof state before:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (2 * 10 ^ (1 + (Nat.digits 10 (n.succ / 10)).length) + (n + 1)) / 10 =
    2 * 10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10
Tactic:
rw [pow_add, pow_one, add_comm]
Proof state after:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (n + 1 + 2 * (10 * 10 ^ (Nat.digits 10 (n.succ / 10)).length)) / 10 =
    2 * 10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10
Theorem: ZerosOnesAndTwos.prepend_two_div
Proof state before:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (n + 1 + 2 * (10 * 10 ^ (Nat.digits 10 (n.succ / 10)).length)) / 10 =
    2 * 10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10
Tactic:
rw [←mul_left_comm]
Proof state after:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (n + 1 + 10 * (2 * 10 ^ (Nat.digits 10 (n.succ / 10)).length)) / 10 =
    2 * 10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10
Theorem: ZerosOnesAndTwos.prepend_two_div
Proof state before:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (n + 1 + 10 * (2 * 10 ^ (Nat.digits 10 (n.succ / 10)).length)) / 10 =
    2 * 10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10
Tactic:
rw [Nat.add_mul_div_left _ _ (Nat.succ_pos 9)]
Proof state after:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (n + 1) / Nat.succ 9 + 2 * 10 ^ (Nat.digits 10 (n.succ / 10)).length =
    2 * 10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10
Theorem: ZerosOnesAndTwos.prepend_two_div
Proof state before:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (n + 1) / Nat.succ 9 + 2 * 10 ^ (Nat.digits 10 (n.succ / 10)).length =
    2 * 10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10
Tactic:
exact add_comm _ _
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.prepend_two_mod
Proof state before:
n : ℕ
hn : 0 < n
⊢ prepend_two n % 10 = n % 10
Tactic:
rw [prepend_two]
Proof state after:
n : ℕ
hn : 0 < n
⊢ (2 * 10 ^ (Nat.digits 10 n).length + n) % 10 = n % 10
Theorem: ZerosOnesAndTwos.prepend_two_mod
Proof state before:
n : ℕ
hn : 0 < n
⊢ (2 * 10 ^ (Nat.digits 10 n).length + n) % 10 = n % 10
Tactic:
rw [Nat.digits_len _ _ two_le_ten (ne_of_gt hn)]
Proof state after:
n : ℕ
hn : 0 < n
⊢ (2 * 10 ^ (Nat.log 10 n + 1) + n) % 10 = n % 10
Theorem: ZerosOnesAndTwos.prepend_two_mod
Proof state before:
n : ℕ
hn : 0 < n
⊢ (2 * 10 ^ (Nat.log 10 n + 1) + n) % 10 = n % 10
Tactic:
rw [pow_add, pow_one, ←mul_assoc]
Proof state after:
n : ℕ
hn : 0 < n
⊢ (2 * 10 ^ Nat.log 10 n * 10 + n) % 10 = n % 10
Theorem: ZerosOnesAndTwos.prepend_two_mod
Proof state before:
n : ℕ
hn : 0 < n
⊢ (2 * 10 ^ Nat.log 10 n * 10 + n) % 10 = n % 10
Tactic:
exact Nat.mul_add_mod' _ 10 n
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.prepend_two_eq_append
Proof state before:
n : ℕ
⊢ Nat.digits 10 (prepend_two n) = Nat.digits 10 n ++ [2]
Tactic:
induction' n using Nat.strong_induction_on with n' ih
Proof state after:
case h
n' : ℕ
ih : ∀ m < n', Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
⊢ Nat.digits 10 (prepend_two n') = Nat.digits 10 n' ++ [2]
Theorem: ZerosOnesAndTwos.prepend_two_eq_append
Proof state before:
case h
n' : ℕ
ih : ∀ m < n', Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
⊢ Nat.digits 10 (prepend_two n') = Nat.digits 10 n' ++ [2]
Tactic:
cases' n' with n'
Proof state after:
case h.zero
ih : ∀ m < 0, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
⊢ Nat.digits 10 (prepend_two 0) = Nat.digits 10 0 ++ [2]

case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
⊢ Nat.digits 10 (prepend_two (n' + 1)) = Nat.digits 10 (n' + 1) ++ [2]
Theorem: ZerosOnesAndTwos.prepend_two_eq_append
Proof state before:
case h.zero
ih : ∀ m < 0, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
⊢ Nat.digits 10 (prepend_two 0) = Nat.digits 10 0 ++ [2]
Tactic:
norm_num [prepend_two]
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.prepend_two_eq_append
Proof state before:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
⊢ Nat.digits 10 (prepend_two (n' + 1)) = Nat.digits 10 (n' + 1) ++ [2]
Tactic:
rw [Nat.digits_def' two_le_ten (prepend_two_pos _)]
Proof state after:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
⊢ prepend_two (n' + 1) % 10 :: Nat.digits 10 (prepend_two (n' + 1) / 10) = Nat.digits 10 (n' + 1) ++ [2]
Theorem: ZerosOnesAndTwos.prepend_two_eq_append
Proof state before:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
⊢ prepend_two (n' + 1) % 10 :: Nat.digits 10 (prepend_two (n' + 1) / 10) = Nat.digits 10 (n' + 1) ++ [2]
Tactic:
rw [prepend_two_div _ (Nat.succ_pos n')]
Proof state after:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
⊢ prepend_two (n' + 1) % 10 :: Nat.digits 10 (prepend_two (n'.succ / 10)) = Nat.digits 10 (n' + 1) ++ [2]
Theorem: ZerosOnesAndTwos.prepend_two_eq_append
Proof state before:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
⊢ prepend_two (n' + 1) % 10 :: Nat.digits 10 (prepend_two (n'.succ / 10)) = Nat.digits 10 (n' + 1) ++ [2]
Tactic:
have hns : n'.succ / 10 < n'.succ := Nat.div_lt_self' n' 8
Proof state after:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
hns : n'.succ / 10 < n'.succ
⊢ prepend_two (n' + 1) % 10 :: Nat.digits 10 (prepend_two (n'.succ / 10)) = Nat.digits 10 (n' + 1) ++ [2]
Theorem: ZerosOnesAndTwos.prepend_two_eq_append
Proof state before:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
hns : n'.succ / 10 < n'.succ
⊢ prepend_two (n' + 1) % 10 :: Nat.digits 10 (prepend_two (n'.succ / 10)) = Nat.digits 10 (n' + 1) ++ [2]
Tactic:
rw [ih _ hns]
Proof state after:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
hns : n'.succ / 10 < n'.succ
⊢ prepend_two (n' + 1) % 10 :: (Nat.digits 10 (n'.succ / 10) ++ [2]) = Nat.digits 10 (n' + 1) ++ [2]
Theorem: ZerosOnesAndTwos.prepend_two_eq_append
Proof state before:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
hns : n'.succ / 10 < n'.succ
⊢ prepend_two (n' + 1) % 10 :: (Nat.digits 10 (n'.succ / 10) ++ [2]) = Nat.digits 10 (n' + 1) ++ [2]
Tactic:
rw [←List.cons_append]
Proof state after:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
hns : n'.succ / 10 < n'.succ
⊢ prepend_two (n' + 1) % 10 :: Nat.digits 10 (n'.succ / 10) ++ [2] = Nat.digits 10 (n' + 1) ++ [2]
Theorem: ZerosOnesAndTwos.prepend_two_eq_append
Proof state before:
case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_two m) = Nat.digits 10 m ++ [2]
hns : n'.succ / 10 < n'.succ
⊢ prepend_two (n' + 1) % 10 :: Nat.digits 10 (n'.succ / 10) ++ [2] = Nat.digits 10 (n' + 1) ++ [2]
Tactic:
rw [prepend_two_mod _ (Nat.succ_pos _), ←Nat.digits_def' two_le_ten (Nat.succ_pos n')]
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.prepend_two_all_one_or_two
Proof state before:
n : ℕ
hn : all_one_or_two (Nat.digits 10 n)
⊢ all_one_or_two (Nat.digits 10 (prepend_two n))
Tactic:
rw [prepend_two_eq_append, all_one_or_two]
Proof state after:
n : ℕ
hn : all_one_or_two (Nat.digits 10 n)
⊢ ∀ e ∈ Nat.digits 10 n ++ [2], e = 1 ∨ e = 2
Theorem: ZerosOnesAndTwos.prepend_two_all_one_or_two
Proof state before:
n : ℕ
hn : all_one_or_two (Nat.digits 10 n)
⊢ ∀ e ∈ Nat.digits 10 n ++ [2], e = 1 ∨ e = 2
Tactic:
rw [all_one_or_two] at hn
Proof state after:
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
⊢ ∀ e ∈ Nat.digits 10 n ++ [2], e = 1 ∨ e = 2
Theorem: ZerosOnesAndTwos.prepend_two_all_one_or_two
Proof state before:
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
⊢ ∀ e ∈ Nat.digits 10 n ++ [2], e = 1 ∨ e = 2
Tactic:
intro e he
Proof state after:
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ Nat.digits 10 n ++ [2]
⊢ e = 1 ∨ e = 2
Theorem: ZerosOnesAndTwos.prepend_two_all_one_or_two
Proof state before:
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ Nat.digits 10 n ++ [2]
⊢ e = 1 ∨ e = 2
Tactic:
rw [List.mem_append] at he
Proof state after:
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ Nat.digits 10 n ∨ e ∈ [2]
⊢ e = 1 ∨ e = 2
Theorem: ZerosOnesAndTwos.prepend_two_all_one_or_two
Proof state before:
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ Nat.digits 10 n ∨ e ∈ [2]
⊢ e = 1 ∨ e = 2
Tactic:
cases' he with he he
Proof state after:
case inl
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ Nat.digits 10 n
⊢ e = 1 ∨ e = 2

case inr
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ [2]
⊢ e = 1 ∨ e = 2
Theorem: ZerosOnesAndTwos.prepend_two_all_one_or_two
Proof state before:
case inl
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ Nat.digits 10 n
⊢ e = 1 ∨ e = 2
Tactic:
exact hn e he
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.prepend_two_all_one_or_two
Proof state before:
case inr
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e ∈ [2]
⊢ e = 1 ∨ e = 2
Tactic:
rw [List.mem_singleton] at he
Proof state after:
case inr
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e = 2
⊢ e = 1 ∨ e = 2
Theorem: ZerosOnesAndTwos.prepend_two_all_one_or_two
Proof state before:
case inr
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e = 2
⊢ e = 1 ∨ e = 2
Tactic:
right
Proof state after:
case inr.h
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e = 2
⊢ e = 2
Theorem: ZerosOnesAndTwos.prepend_two_all_one_or_two
Proof state before:
case inr.h
n : ℕ
hn : ∀ e ∈ Nat.digits 10 n, e = 1 ∨ e = 2
e : ℕ
he : e = 2
⊢ e = 2
Tactic:
exact he
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.factor_ten_pow
Proof state before:
k : ℕ
⊢ 10 ^ k = 2 ^ k * 5 ^ k
Tactic:
induction' k with k' ih
Proof state after:
case zero

⊢ 10 ^ 0 = 2 ^ 0 * 5 ^ 0

case succ
k' : ℕ
ih : 10 ^ k' = 2 ^ k' * 5 ^ k'
⊢ 10 ^ (k' + 1) = 2 ^ (k' + 1) * 5 ^ (k' + 1)
Theorem: ZerosOnesAndTwos.factor_ten_pow
Proof state before:
case zero

⊢ 10 ^ 0 = 2 ^ 0 * 5 ^ 0
Tactic:
simp only [pow_zero, mul_one]
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.factor_ten_pow
Proof state before:
case succ
k' : ℕ
ih : 10 ^ k' = 2 ^ k' * 5 ^ k'
⊢ 10 ^ (k' + 1) = 2 ^ (k' + 1) * 5 ^ (k' + 1)
Tactic:
rw [pow_succ, pow_succ, pow_succ, ih]
Proof state after:
case succ
k' : ℕ
ih : 10 ^ k' = 2 ^ k' * 5 ^ k'
⊢ 2 ^ k' * 5 ^ k' * 10 = 2 ^ k' * 2 * (5 ^ k' * 5)
Theorem: ZerosOnesAndTwos.factor_ten_pow
Proof state before:
case succ
k' : ℕ
ih : 10 ^ k' = 2 ^ k' * 5 ^ k'
⊢ 2 ^ k' * 5 ^ k' * 10 = 2 ^ k' * 2 * (5 ^ k' * 5)
Tactic:
ring
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.even_5_pow_plus_one
Proof state before:
n : ℕ
⊢ 2 ∣ 5 ^ n + 1
Tactic:
apply Nat.dvd_of_mod_eq_zero
Proof state after:
case H
n : ℕ
⊢ (5 ^ n + 1) % 2 = 0
Theorem: ZerosOnesAndTwos.even_5_pow_plus_one
Proof state before:
case H
n : ℕ
⊢ (5 ^ n + 1) % 2 = 0
Tactic:
rw [Nat.add_mod, Nat.pow_mod]
Proof state after:
case H
n : ℕ
⊢ ((5 % 2) ^ n % 2 + 1 % 2) % 2 = 0
Theorem: ZerosOnesAndTwos.even_5_pow_plus_one
Proof state before:
case H
n : ℕ
⊢ ((5 % 2) ^ n % 2 + 1 % 2) % 2 = 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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
Proof 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))
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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
Proof 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))
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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
Proof 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))
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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
Proof 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))
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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]
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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
Proof 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))
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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
Proof 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))
Theorem: ZerosOnesAndTwos.ones_and_twos_aux
Proof 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
Proof 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))