internlm/Lean-Github huggingface dataset:
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case right
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
⊢ Function.Surjective b
Tactic:
rintro ⟨x, hx⟩
Proof state after:
case right.mk
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : s ∉ x
⊢ ∃ a, b a = ⟨x, hx⟩
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case right.mk
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : s ∉ x
⊢ ∃ a, b a = ⟨x, hx⟩
Tactic:
use Finset.subtype _ x
Proof state after:
case h
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : s ∉ x
⊢ b (Finset.subtype (fun a => a ≠ s) x) = ⟨x, hx⟩
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case h
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : s ∉ x
⊢ b (Finset.subtype (fun a => a ≠ s) x) = ⟨x, hx⟩
Tactic:
simp only [Finset.subtype_map, Subtype.mk.injEq, b]
Proof state after:
case h
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : s ∉ x
⊢ Finset.filter (fun a => a ≠ s) x = x
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case h
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : s ∉ x
⊢ Finset.filter (fun a => a ≠ s) x = x
Tactic:
have h7 : ∀ a ∈ x, ¬ a = s := by
  intro a ha has
  rw [has] at ha
  contradiction
Proof state after:
case h
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : s ∉ x
h7 : ∀ a ∈ x, ¬a = s
⊢ Finset.filter (fun a => a ≠ s) x = x
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
case h
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : s ∉ x
h7 : ∀ a ∈ x, ¬a = s
⊢ Finset.filter (fun a => a ≠ s) x = x
Tactic:
exact Finset.filter_eq_self.mpr h7
Proof state after:
no goals
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : s ∉ x
⊢ ∀ a ∈ x, ¬a = s
Tactic:
intro a ha has
Proof state after:
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : s ∉ x
a : S
ha : a ∈ x
has : a = s
⊢ False
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : s ∉ x
a : S
ha : a ∈ x
has : a = s
⊢ False
Tactic:
rw [has] at ha
Proof state after:
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : s ∉ x
a : S
ha : s ∈ x
has : a = s
⊢ False
Theorem: Usa2002P1.usa2002_p1_generalized
Proof state before:
k : ℕ
ih :
  ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α],
    Fintype.card α = k →
      ∀ N ≤ 2 ^ k,
        ∃ f, (∀ (s1 s2 : Finset α), f s1 = f s2 → f (s1 ∪ s2) = f s1) ∧ Fintype.card { a // f a = Color.red } = N
S : Type
hde : DecidableEq S
hft : Fintype S
hs : Fintype.card S = k + 1
N : ℕ
hN : N ≤ 2 ^ (k + 1)
s : S
S' : Type := { a // a ≠ s }
hs' : Fintype.card S' = k
hg : N > 2 ^ k
hl : N - 2 ^ k ≤ 2 ^ k
f' : Finset S' → Color
h5 : Fintype.card (Finset S') = 2 ^ k
b : Finset S' → { a // s ∉ a } := fun a => ⟨Finset.map (Function.Embedding.subtype fun a => a ≠ s) a, ⋯⟩
x : Finset S
hx : s ∉ x
a : S
ha : s ∈ x
has : a = s
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: Poland2016S1P8.even_of_add
Proof state before:
a b : ℤ
⊢ Even a → Even (a + b) → Even b
Tactic:
intro A
Proof state after:
a b : ℤ
A : Even a
⊢ Even (a + b) → Even b
Theorem: Poland2016S1P8.even_of_add
Proof state before:
a b : ℤ
A : Even a
⊢ Even (a + b) → Even b
Tactic:
obtain ⟨k, H⟩ := A
Proof state after:
case intro
a b k : ℤ
H : a = k + k
⊢ Even (a + b) → Even b
Theorem: Poland2016S1P8.even_of_add
Proof state before:
case intro
a b k : ℤ
H : a = k + k
⊢ Even (a + b) → Even b
Tactic:
intro A_B
Proof state after:
case intro
a b k : ℤ
H : a = k + k
A_B : Even (a + b)
⊢ Even b
Theorem: Poland2016S1P8.even_of_add
Proof state before:
case intro
a b k : ℤ
H : a = k + k
A_B : Even (a + b)
⊢ Even b
Tactic:
obtain ⟨k2, H2⟩ := A_B
Proof state after:
case intro.intro
a b k : ℤ
H : a = k + k
k2 : ℤ
H2 : a + b = k2 + k2
⊢ Even b
Theorem: Poland2016S1P8.even_of_add
Proof state before:
case intro.intro
a b k : ℤ
H : a = k + k
k2 : ℤ
H2 : a + b = k2 + k2
⊢ Even b
Tactic:
use (k2 - k)
Proof state after:
case h
a b k : ℤ
H : a = k + k
k2 : ℤ
H2 : a + b = k2 + k2
⊢ b = k2 - k + (k2 - k)
Theorem: Poland2016S1P8.even_of_add
Proof state before:
case h
a b k : ℤ
H : a = k + k
k2 : ℤ
H2 : a + b = k2 + k2
⊢ b = k2 - k + (k2 - k)
Tactic:
rw [H] at H2
Proof state after:
case h
a b k : ℤ
H : a = k + k
k2 : ℤ
H2 : k + k + b = k2 + k2
⊢ b = k2 - k + (k2 - k)
Theorem: Poland2016S1P8.even_of_add
Proof state before:
case h
a b k : ℤ
H : a = k + k
k2 : ℤ
H2 : k + k + b = k2 + k2
⊢ b = k2 - k + (k2 - k)
Tactic:
apply symm
Proof state after:
case h.a
a b k : ℤ
H : a = k + k
k2 : ℤ
H2 : k + k + b = k2 + k2
⊢ k2 - k + (k2 - k) = b
Theorem: Poland2016S1P8.even_of_add
Proof state before:
case h.a
a b k : ℤ
H : a = k + k
k2 : ℤ
H2 : k + k + b = k2 + k2
⊢ k2 - k + (k2 - k) = b
Tactic:
calc k2 - k + (k2 - k) = k2 + k2 - k - k := by ring
  _ = k + k + b - k -k := by rw[H2]
  _ = b := by ring
Proof state after:
no goals
Theorem: Poland2016S1P8.even_of_add
Proof state before:
a b k : ℤ
H : a = k + k
k2 : ℤ
H2 : k + k + b = k2 + k2
⊢ k2 - k + (k2 - k) = k2 + k2 - k - k
Tactic:
ring
Proof state after:
no goals
Theorem: Poland2016S1P8.even_of_add
Proof state before:
a b k : ℤ
H : a = k + k
k2 : ℤ
H2 : k + k + b = k2 + k2
⊢ k2 + k2 - k - k = k + k + b - k - k
Tactic:
rw[H2]
Proof state after:
no goals
Theorem: Poland2016S1P8.even_of_add
Proof state before:
a b k : ℤ
H : a = k + k
k2 : ℤ
H2 : k + k + b = k2 + k2
⊢ k + k + b - k - k = b
Tactic:
ring
Proof state after:
no goals
Theorem: Poland2016S1P8.div_4_mul_of_both_even
Proof state before:
a b : ℤ
H : Even a ∧ Even b
⊢ 4 ∣ a * b
Tactic:
obtain ⟨k, Hk⟩ := H.left
Proof state after:
case intro
a b : ℤ
H : Even a ∧ Even b
k : ℤ
Hk : a = k + k
⊢ 4 ∣ a * b
Theorem: Poland2016S1P8.div_4_mul_of_both_even
Proof state before:
case intro
a b : ℤ
H : Even a ∧ Even b
k : ℤ
Hk : a = k + k
⊢ 4 ∣ a * b
Tactic:
obtain ⟨l, Hl⟩ := H.right
Proof state after:
case intro.intro
a b : ℤ
H : Even a ∧ Even b
k : ℤ
Hk : a = k + k
l : ℤ
Hl : b = l + l
⊢ 4 ∣ a * b
Theorem: Poland2016S1P8.div_4_mul_of_both_even
Proof state before:
case intro.intro
a b : ℤ
H : Even a ∧ Even b
k : ℤ
Hk : a = k + k
l : ℤ
Hl : b = l + l
⊢ 4 ∣ a * b
Tactic:
use k * l
Proof state after:
case h
a b : ℤ
H : Even a ∧ Even b
k : ℤ
Hk : a = k + k
l : ℤ
Hl : b = l + l
⊢ a * b = 4 * (k * l)
Theorem: Poland2016S1P8.div_4_mul_of_both_even
Proof state before:
case h
a b : ℤ
H : Even a ∧ Even b
k : ℤ
Hk : a = k + k
l : ℤ
Hl : b = l + l
⊢ a * b = 4 * (k * l)
Tactic:
rw[Hk]
Proof state after:
case h
a b : ℤ
H : Even a ∧ Even b
k : ℤ
Hk : a = k + k
l : ℤ
Hl : b = l + l
⊢ (k + k) * b = 4 * (k * l)
Theorem: Poland2016S1P8.div_4_mul_of_both_even
Proof state before:
case h
a b : ℤ
H : Even a ∧ Even b
k : ℤ
Hk : a = k + k
l : ℤ
Hl : b = l + l
⊢ (k + k) * b = 4 * (k * l)
Tactic:
rw[Hl]
Proof state after:
case h
a b : ℤ
H : Even a ∧ Even b
k : ℤ
Hk : a = k + k
l : ℤ
Hl : b = l + l
⊢ (k + k) * (l + l) = 4 * (k * l)
Theorem: Poland2016S1P8.div_4_mul_of_both_even
Proof state before:
case h
a b : ℤ
H : Even a ∧ Even b
k : ℤ
Hk : a = k + k
l : ℤ
Hl : b = l + l
⊢ (k + k) * (l + l) = 4 * (k * l)
Tactic:
ring
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.of_digits_zeros_eq_zero
Proof state before:
b m : ℕ
⊢ Nat.ofDigits b (List.replicate m 0) = 0
Tactic:
induction' m with m ih
Proof state after:
case zero
b : ℕ
⊢ Nat.ofDigits b (List.replicate 0 0) = 0

case succ
b m : ℕ
ih : Nat.ofDigits b (List.replicate m 0) = 0
⊢ Nat.ofDigits b (List.replicate (m + 1) 0) = 0
Theorem: ZerosOnesAndTwos.of_digits_zeros_eq_zero
Proof state before:
case zero
b : ℕ
⊢ Nat.ofDigits b (List.replicate 0 0) = 0
Tactic:
rfl
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.of_digits_zeros_eq_zero
Proof state before:
case succ
b m : ℕ
ih : Nat.ofDigits b (List.replicate m 0) = 0
⊢ Nat.ofDigits b (List.replicate (m + 1) 0) = 0
Tactic:
simp only [Nat.ofDigits, Nat.cast_zero, ih, mul_zero, add_zero]
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.ones_add
Proof state before:
b m n : ℕ
⊢ ones b (m + n) = ones b m + Nat.ofDigits b (List.replicate m 0 ++ List.replicate n 1)
Tactic:
unfold ones
Proof state after:
b m n : ℕ
⊢ (let k := m + n;
    Nat.ofDigits b (List.replicate k 1)) =
    (let k := m;
      Nat.ofDigits b (List.replicate k 1)) +
      Nat.ofDigits b (List.replicate m 0 ++ List.replicate n 1)
Theorem: ZerosOnesAndTwos.ones_add
Proof state before:
b m n : ℕ
⊢ (let k := m + n;
    Nat.ofDigits b (List.replicate k 1)) =
    (let k := m;
      Nat.ofDigits b (List.replicate k 1)) +
      Nat.ofDigits b (List.replicate m 0 ++ List.replicate n 1)
Tactic:
dsimp only
Proof state after:
b m n : ℕ
⊢ Nat.ofDigits b (List.replicate (m + n) 1) =
    Nat.ofDigits b (List.replicate m 1) + Nat.ofDigits b (List.replicate m 0 ++ List.replicate n 1)
Theorem: ZerosOnesAndTwos.ones_add
Proof state before:
b m n : ℕ
⊢ Nat.ofDigits b (List.replicate (m + n) 1) =
    Nat.ofDigits b (List.replicate m 1) + Nat.ofDigits b (List.replicate m 0 ++ List.replicate n 1)
Tactic:
rw [List.replicate_add, Nat.ofDigits_append, Nat.ofDigits_append]
Proof state after:
b m n : ℕ
⊢ Nat.ofDigits b (List.replicate m 1) + b ^ (List.replicate m 1).length * Nat.ofDigits b (List.replicate n 1) =
    Nat.ofDigits b (List.replicate m 1) +
      (Nat.ofDigits b (List.replicate m 0) + b ^ (List.replicate m 0).length * Nat.ofDigits b (List.replicate n 1))
Theorem: ZerosOnesAndTwos.ones_add
Proof state before:
b m n : ℕ
⊢ Nat.ofDigits b (List.replicate m 1) + b ^ (List.replicate m 1).length * Nat.ofDigits b (List.replicate n 1) =
    Nat.ofDigits b (List.replicate m 1) +
      (Nat.ofDigits b (List.replicate m 0) + b ^ (List.replicate m 0).length * Nat.ofDigits b (List.replicate n 1))
Tactic:
rw [List.length_replicate, List.length_replicate, of_digits_zeros_eq_zero, zero_add]
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.lemma_3
Proof state before:
a n : ℕ
ha : 0 < a
hm : a % n = 0
⊢ ∃ k, a = n * ↑k
Tactic:
obtain ⟨k', hk'⟩ := exists_eq_mul_right_of_dvd (Nat.dvd_of_mod_eq_zero hm)
Proof state after:
case intro
a n : ℕ
ha : 0 < a
hm : a % n = 0
k' : ℕ
hk' : a = n * k'
⊢ ∃ k, a = n * ↑k
Theorem: ZerosOnesAndTwos.lemma_3
Proof state before:
case intro
a n : ℕ
ha : 0 < a
hm : a % n = 0
k' : ℕ
hk' : a = n * k'
⊢ ∃ k, a = n * ↑k
Tactic:
have hkp : 0 < k' := lt_of_mul_lt_mul_left' (hk' ▸ ha)
Proof state after:
case intro
a n : ℕ
ha : 0 < a
hm : a % n = 0
k' : ℕ
hk' : a = n * k'
hkp : 0 < k'
⊢ ∃ k, a = n * ↑k
Theorem: ZerosOnesAndTwos.lemma_3
Proof state before:
case intro
a n : ℕ
ha : 0 < a
hm : a % n = 0
k' : ℕ
hk' : a = n * k'
hkp : 0 < k'
⊢ ∃ k, a = n * ↑k
Tactic:
exact ⟨⟨k', hkp⟩, hk'⟩
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.prepend_one_pos
Proof state before:
n : ℕ
⊢ 0 < prepend_one n
Tactic:
cases' n
Proof state after:
case zero

⊢ 0 < prepend_one 0

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

⊢ 0 < prepend_one 0
Tactic:
simp [prepend_one]
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.prepend_one_pos
Proof state before:
case succ
n✝ : ℕ
⊢ 0 < prepend_one (n✝ + 1)
Tactic:
rw [prepend_one]
Proof state after:
case succ
n✝ : ℕ
⊢ 0 < 10 ^ (Nat.digits 10 (n✝ + 1)).length + (n✝ + 1)
Theorem: ZerosOnesAndTwos.prepend_one_pos
Proof state before:
case succ
n✝ : ℕ
⊢ 0 < 10 ^ (Nat.digits 10 (n✝ + 1)).length + (n✝ + 1)
Tactic:
norm_num
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.digits_len'
Proof state before:
n : ℕ
hn : 0 < n
⊢ (Nat.digits 10 n).length = 1 + (Nat.digits 10 (n / 10)).length
Tactic:
rw [Nat.digits_def' two_le_ten hn, List.length]
Proof state after:
n : ℕ
hn : 0 < n
⊢ (Nat.digits 10 (n / 10)).length + 1 = 1 + (Nat.digits 10 (n / 10)).length
Theorem: ZerosOnesAndTwos.digits_len'
Proof state before:
n : ℕ
hn : 0 < n
⊢ (Nat.digits 10 (n / 10)).length + 1 = 1 + (Nat.digits 10 (n / 10)).length
Tactic:
exact add_comm _ _
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.prepend_one_div
Proof state before:
n : ℕ
hn : 0 < n
⊢ prepend_one n / 10 = prepend_one (n / 10)
Tactic:
rw [prepend_one, prepend_one]
Proof state after:
n : ℕ
hn : 0 < n
⊢ (10 ^ (Nat.digits 10 n).length + n) / 10 = 10 ^ (Nat.digits 10 (n / 10)).length + n / 10
Theorem: ZerosOnesAndTwos.prepend_one_div
Proof state before:
n : ℕ
hn : 0 < n
⊢ (10 ^ (Nat.digits 10 n).length + n) / 10 = 10 ^ (Nat.digits 10 (n / 10)).length + n / 10
Tactic:
cases' n with n
Proof state after:
case zero
hn : 0 < 0
⊢ (10 ^ (Nat.digits 10 0).length + 0) / 10 = 10 ^ (Nat.digits 10 (0 / 10)).length + 0 / 10

case succ
n : ℕ
hn : 0 < n + 1
⊢ (10 ^ (Nat.digits 10 (n + 1)).length + (n + 1)) / 10 = 10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10
Theorem: ZerosOnesAndTwos.prepend_one_div
Proof state before:
case zero
hn : 0 < 0
⊢ (10 ^ (Nat.digits 10 0).length + 0) / 10 = 10 ^ (Nat.digits 10 (0 / 10)).length + 0 / 10
Tactic:
exact (Nat.lt_asymm hn hn).elim
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.prepend_one_div
Proof state before:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (10 ^ (Nat.digits 10 (n + 1)).length + (n + 1)) / 10 = 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
⊢ (10 ^ (1 + (Nat.digits 10 (n.succ / 10)).length) + (n + 1)) / 10 =
    10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10
Theorem: ZerosOnesAndTwos.prepend_one_div
Proof state before:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (10 ^ (1 + (Nat.digits 10 (n.succ / 10)).length) + (n + 1)) / 10 =
    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 + 10 * 10 ^ (Nat.digits 10 (n.succ / 10)).length) / 10 =
    10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10
Theorem: ZerosOnesAndTwos.prepend_one_div
Proof state before:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (n + 1 + 10 * 10 ^ (Nat.digits 10 (n.succ / 10)).length) / 10 =
    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 + 10 ^ (Nat.digits 10 (n.succ / 10)).length =
    10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10
Theorem: ZerosOnesAndTwos.prepend_one_div
Proof state before:
case succ
n : ℕ
hn : 0 < n + 1
⊢ (n + 1) / Nat.succ 9 + 10 ^ (Nat.digits 10 (n.succ / 10)).length =
    10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10
Tactic:
exact add_comm _ _
Proof state after:
no goals
Theorem: ZerosOnesAndTwos.prepend_one_mod
Proof state before:
n : ℕ
hn : 0 < n
⊢ prepend_one n % 10 = n % 10
Tactic:
rw [prepend_one]
Proof state after:
n : ℕ
hn : 0 < n
⊢ (10 ^ (Nat.digits 10 n).length + n) % 10 = n % 10
Theorem: ZerosOnesAndTwos.prepend_one_mod
Proof state before:
n : ℕ
hn : 0 < n
⊢ (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
⊢ (10 ^ (Nat.log 10 n + 1) + n) % 10 = n % 10
Theorem: ZerosOnesAndTwos.prepend_one_mod
Proof state before:
n : ℕ
hn : 0 < n
⊢ (10 ^ (Nat.log 10 n + 1) + n) % 10 = n % 10
Tactic:
rw [pow_add, pow_one]
Proof state after:
n : ℕ
hn : 0 < n
⊢ (10 ^ Nat.log 10 n * 10 + n) % 10 = n % 10
Theorem: ZerosOnesAndTwos.prepend_one_mod
Proof state before:
n : ℕ
hn : 0 < n
⊢ (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_one_eq_append
Proof state before:
n : ℕ
⊢ Nat.digits 10 (prepend_one n) = Nat.digits 10 n ++ [1]
Tactic:
induction' n using Nat.strong_induction_on with n' ih
Proof state after:
case h
n' : ℕ
ih : ∀ m < n', Nat.digits 10 (prepend_one m) = Nat.digits 10 m ++ [1]
⊢ Nat.digits 10 (prepend_one n') = Nat.digits 10 n' ++ [1]
Theorem: ZerosOnesAndTwos.prepend_one_eq_append
Proof state before:
case h
n' : ℕ
ih : ∀ m < n', Nat.digits 10 (prepend_one m) = Nat.digits 10 m ++ [1]
⊢ Nat.digits 10 (prepend_one n') = Nat.digits 10 n' ++ [1]
Tactic:
cases' n' with n'
Proof state after:
case h.zero
ih : ∀ m < 0, Nat.digits 10 (prepend_one m) = Nat.digits 10 m ++ [1]
⊢ Nat.digits 10 (prepend_one 0) = Nat.digits 10 0 ++ [1]

case h.succ
n' : ℕ
ih : ∀ m < n' + 1, Nat.digits 10 (prepend_one m) = Nat.digits 10 m ++ [1]
⊢ Nat.digits 10 (prepend_one (n' + 1)) = Nat.digits 10 (n' + 1) ++ [1]
Theorem: ZerosOnesAndTwos.prepend_one_eq_append
Proof state before:
case h.zero
ih : ∀ m < 0, Nat.digits 10 (prepend_one m) = Nat.digits 10 m ++ [1]
⊢ Nat.digits 10 (prepend_one 0) = Nat.digits 10 0 ++ [1]
Tactic:
simp_arith [prepend_one]
Proof state after:
no goals
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]
⊢ Nat.digits 10 (prepend_one (n' + 1)) = Nat.digits 10 (n' + 1) ++ [1]
Tactic:
rw [Nat.digits_def' two_le_ten (prepend_one_pos _)]
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' + 1) / 10) = Nat.digits 10 (n' + 1) ++ [1]