internlm/Lean-Github huggingface dataset:
Theorem: Usa1992P1.digits_sum
Proof state before:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
one_lt_ten : 1 < 10
h5 :
  Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ =
    Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * x.succ)
⊢ (Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * (x + 1))).sum =
    (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum
Tactic:
rw [←h5]
Proof state after:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
one_lt_ten : 1 < 10
h5 :
  Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ =
    Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * x.succ)
⊢ (Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ).sum =
    (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum
Theorem: Usa1992P1.digits_sum
Proof state before:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
one_lt_ten : 1 < 10
h5 :
  Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ =
    Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * x.succ)
⊢ (Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ).sum =
    (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum
Tactic:
simp only [List.sum_append]
Proof state after:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
one_lt_ten : 1 < 10
h5 :
  Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ =
    Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * x.succ)
⊢ (Nat.digits 10 y).sum + (List.replicate k 0).sum + (Nat.digits 10 x.succ).sum =
    (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum
Theorem: Usa1992P1.digits_sum
Proof state before:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
one_lt_ten : 1 < 10
h5 :
  Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ =
    Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * x.succ)
⊢ (Nat.digits 10 y).sum + (List.replicate k 0).sum + (Nat.digits 10 x.succ).sum =
    (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum
Tactic:
simp only [List.sum_replicate, smul_eq_mul, mul_zero, add_zero]
Proof state after:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
one_lt_ten : 1 < 10
h5 :
  Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ =
    Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * x.succ)
⊢ (Nat.digits 10 y).sum + (Nat.digits 10 x.succ).sum = (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum
Theorem: Usa1992P1.digits_sum
Proof state before:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
one_lt_ten : 1 < 10
h5 :
  Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ =
    Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * x.succ)
⊢ (Nat.digits 10 y).sum + (Nat.digits 10 x.succ).sum = (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum
Tactic:
rw [digits_sum_mul_pow]
Proof state after:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
one_lt_ten : 1 < 10
h5 :
  Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ =
    Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * x.succ)
⊢ (Nat.digits 10 y).sum + (Nat.digits 10 x.succ).sum = (Nat.digits 10 (x + 1)).sum + (Nat.digits 10 y).sum
Theorem: Usa1992P1.digits_sum
Proof state before:
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
one_lt_ten : 1 < 10
h5 :
  Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ =
    Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * x.succ)
⊢ (Nat.digits 10 y).sum + (Nat.digits 10 x.succ).sum = (Nat.digits 10 (x + 1)).sum + (Nat.digits 10 y).sum
Tactic:
ring
Proof state after:
no goals
Theorem: Usa1992P1.digits_sum
Proof state before:
case zero
m y : ℕ
h1 : y < 10 ^ m
⊢ (Nat.digits 10 (0 * 10 ^ m + y)).sum = (Nat.digits 10 (0 * 10 ^ m)).sum + (Nat.digits 10 y).sum
Tactic:
simp
Proof state after:
no goals
Theorem: Usa1992P1.digits_sum
Proof state before:
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
⊢ (Nat.digits 10 y).length ≤ m
Tactic:
have h4 := lemma2 h1
Proof state after:
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h4 : (Nat.digits 10 y).length < m + 1
⊢ (Nat.digits 10 y).length ≤ m
Theorem: Usa1992P1.digits_sum
Proof state before:
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h4 : (Nat.digits 10 y).length < m + 1
⊢ (Nat.digits 10 y).length ≤ m
Tactic:
exact Nat.le_of_lt_succ h4
Proof state after:
no goals
Theorem: Usa1992P1.digits_sum
Proof state before:
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
⊢ ∃ k, k + (Nat.digits 10 y).length = m
Tactic:
obtain ⟨k, hk⟩ := Nat.le.dest h3
Proof state after:
case intro
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : (Nat.digits 10 y).length + k = m
⊢ ∃ k, k + (Nat.digits 10 y).length = m
Theorem: Usa1992P1.digits_sum
Proof state before:
case intro
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : (Nat.digits 10 y).length + k = m
⊢ ∃ k, k + (Nat.digits 10 y).length = m
Tactic:
rw [add_comm] at hk
Proof state after:
case intro
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
⊢ ∃ k, k + (Nat.digits 10 y).length = m
Theorem: Usa1992P1.digits_sum
Proof state before:
case intro
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
⊢ ∃ k, k + (Nat.digits 10 y).length = m
Tactic:
exact ⟨k, hk⟩
Proof state after:
no goals
Theorem: Usa1992P1.digits_sum
Proof state before:
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
⊢ 1 < 10
Tactic:
norm_num
Proof state after:
no goals
Theorem: Usa1992P1.Finset.range_prod_odd
Proof state before:
n : ℕ
f : ℕ → ℕ
hs : ∀ i ∈ Finset.range n, Odd (f i)
⊢ Odd (∏ i ∈ Finset.range n, f i)
Tactic:
revert hs
Proof state after:
n : ℕ
f : ℕ → ℕ
⊢ (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
Theorem: Usa1992P1.Finset.range_prod_odd
Proof state before:
n : ℕ
f : ℕ → ℕ
⊢ (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
Tactic:
induction n
Proof state after:
case zero
f : ℕ → ℕ
⊢ (∀ i ∈ Finset.range 0, Odd (f i)) → Odd (∏ i ∈ Finset.range 0, f i)

case succ
f : ℕ → ℕ
n✝ : ℕ
a✝ : (∀ i ∈ Finset.range n✝, Odd (f i)) → Odd (∏ i ∈ Finset.range n✝, f i)
⊢ (∀ i ∈ Finset.range (n✝ + 1), Odd (f i)) → Odd (∏ i ∈ Finset.range (n✝ + 1), f i)
Theorem: Usa1992P1.Finset.range_prod_odd
Proof state before:
f : ℕ → ℕ
⊢ (∀ i ∈ Finset.range 0, Odd (f i)) → Odd (∏ i ∈ Finset.range 0, f i)
Tactic:
case zero => simp
Proof state after:
no goals
Theorem: Usa1992P1.Finset.range_prod_odd
Proof state before:
f : ℕ → ℕ
⊢ (∀ i ∈ Finset.range 0, Odd (f i)) → Odd (∏ i ∈ Finset.range 0, f i)
Tactic:
simp
Proof state after:
no goals
Theorem: Usa1992P1.Finset.range_prod_odd
Proof state before:
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
⊢ (∀ i ∈ Finset.range (n + 1), Odd (f i)) → Odd (∏ i ∈ Finset.range (n + 1), f i)
Tactic:
intro hs
Proof state after:
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ Odd (∏ i ∈ Finset.range (n + 1), f i)
Theorem: Usa1992P1.Finset.range_prod_odd
Proof state before:
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ Odd (∏ i ∈ Finset.range (n + 1), f i)
Tactic:
rw [Finset.prod_range_succ, Nat.odd_mul]
Proof state after:
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ Odd (∏ x ∈ Finset.range n, f x) ∧ Odd (f n)
Theorem: Usa1992P1.Finset.range_prod_odd
Proof state before:
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ Odd (∏ x ∈ Finset.range n, f x) ∧ Odd (f n)
Tactic:
constructor
Proof state after:
case left
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ Odd (∏ x ∈ Finset.range n, f x)

case right
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ Odd (f n)
Theorem: Usa1992P1.Finset.range_prod_odd
Proof state before:
case left
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ Odd (∏ x ∈ Finset.range n, f x)
Tactic:
apply ih
Proof state after:
case left
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ ∀ i ∈ Finset.range n, Odd (f i)
Theorem: Usa1992P1.Finset.range_prod_odd
Proof state before:
case left
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ ∀ i ∈ Finset.range n, Odd (f i)
Tactic:
intro i hi
Proof state after:
case left
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
i : ℕ
hi : i ∈ Finset.range n
⊢ Odd (f i)
Theorem: Usa1992P1.Finset.range_prod_odd
Proof state before:
case left
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
i : ℕ
hi : i ∈ Finset.range n
⊢ Odd (f i)
Tactic:
have : i ∈ Finset.range (n + 1) := by
  rw [Finset.mem_range] at *
  exact Nat.lt_add_right 1 hi
Proof state after:
case left
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
i : ℕ
hi : i ∈ Finset.range n
this : i ∈ Finset.range (n + 1)
⊢ Odd (f i)
Theorem: Usa1992P1.Finset.range_prod_odd
Proof state before:
case left
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
i : ℕ
hi : i ∈ Finset.range n
this : i ∈ Finset.range (n + 1)
⊢ Odd (f i)
Tactic:
exact hs i this
Proof state after:
no goals
Theorem: Usa1992P1.Finset.range_prod_odd
Proof state before:
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
i : ℕ
hi : i ∈ Finset.range n
⊢ i ∈ Finset.range (n + 1)
Tactic:
rw [Finset.mem_range] at *
Proof state after:
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
i : ℕ
hi : i < n
⊢ i < n + 1
Theorem: Usa1992P1.Finset.range_prod_odd
Proof state before:
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
i : ℕ
hi : i < n
⊢ i < n + 1
Tactic:
exact Nat.lt_add_right 1 hi
Proof state after:
no goals
Theorem: Usa1992P1.Finset.range_prod_odd
Proof state before:
case right
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ Odd (f n)
Tactic:
apply hs
Proof state after:
case right.a
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ n ∈ Finset.range (n + 1)
Theorem: Usa1992P1.Finset.range_prod_odd
Proof state before:
case right.a
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ n ∈ Finset.range (n + 1)
Tactic:
rw [Finset.mem_range]
Proof state after:
case right.a
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ n < n + 1
Theorem: Usa1992P1.Finset.range_prod_odd
Proof state before:
case right.a
f : ℕ → ℕ
n : ℕ
ih : (∀ i ∈ Finset.range n, Odd (f i)) → Odd (∏ i ∈ Finset.range n, f i)
hs : ∀ i ∈ Finset.range (n + 1), Odd (f i)
⊢ n < n + 1
Tactic:
exact lt_add_one n
Proof state after:
no goals
Theorem: Imo2009P5.exists_sup_fn_fin
Proof state before:
f : ℕ → ℕ
c : ℕ
⊢ ∃ K, ∀ n < c, f n ≤ K
Tactic:
induction' c with c ih
Proof state after:
case zero
f : ℕ → ℕ
⊢ ∃ K, ∀ n < 0, f n ≤ K

case succ
f : ℕ → ℕ
c : ℕ
ih : ∃ K, ∀ n < c, f n ≤ K
⊢ ∃ K, ∀ n < c + 1, f n ≤ K
Theorem: Imo2009P5.exists_sup_fn_fin
Proof state before:
case zero
f : ℕ → ℕ
⊢ ∃ K, ∀ n < 0, f n ≤ K
Tactic:
simp
Proof state after:
no goals
Theorem: Imo2009P5.exists_sup_fn_fin
Proof state before:
case succ
f : ℕ → ℕ
c : ℕ
ih : ∃ K, ∀ n < c, f n ≤ K
⊢ ∃ K, ∀ n < c + 1, f n ≤ K
Tactic:
obtain ⟨k, hk⟩ := ih
Proof state after:
case succ.intro
f : ℕ → ℕ
c k : ℕ
hk : ∀ n < c, f n ≤ k
⊢ ∃ K, ∀ n < c + 1, f n ≤ K
Theorem: Imo2009P5.exists_sup_fn_fin
Proof state before:
case succ.intro
f : ℕ → ℕ
c k : ℕ
hk : ∀ n < c, f n ≤ k
⊢ ∃ K, ∀ n < c + 1, f n ≤ K
Tactic:
use max k (f c)
Proof state after:
case h
f : ℕ → ℕ
c k : ℕ
hk : ∀ n < c, f n ≤ k
⊢ ∀ n < c + 1, f n ≤ max k (f c)
Theorem: Imo2009P5.exists_sup_fn_fin
Proof state before:
case h
f : ℕ → ℕ
c k : ℕ
hk : ∀ n < c, f n ≤ k
⊢ ∀ n < c + 1, f n ≤ max k (f c)
Tactic:
intro n hn
Proof state after:
case h
f : ℕ → ℕ
c k : ℕ
hk : ∀ n < c, f n ≤ k
n : ℕ
hn : n < c + 1
⊢ f n ≤ max k (f c)
Theorem: Imo2009P5.exists_sup_fn_fin
Proof state before:
case h
f : ℕ → ℕ
c k : ℕ
hk : ∀ n < c, f n ≤ k
n : ℕ
hn : n < c + 1
⊢ f n ≤ max k (f c)
Tactic:
obtain hlt | rfl := Nat.lt_succ_iff_lt_or_eq.mp hn <;> aesop
Proof state after:
no goals
Theorem: Imo2009P5.pnat_to_nat_prop
Proof state before:
P : ℕ+ → Prop
h : ∀ (n : ℕ), P n.succPNat
n : ℕ+
⊢ P n
Tactic:
rw [← PNat.succPNat_natPred n]
Proof state after:
P : ℕ+ → Prop
h : ∀ (n : ℕ), P n.succPNat
n : ℕ+
⊢ P n.natPred.succPNat
Theorem: Imo2009P5.pnat_to_nat_prop
Proof state before:
P : ℕ+ → Prop
h : ∀ (n : ℕ), P n.succPNat
n : ℕ+
⊢ P n.natPred.succPNat
Tactic:
exact h _
Proof state after:
no goals
Theorem: Imo2009P5.pnat_to_nat_prop2
Proof state before:
P : ℕ+ → ℕ+ → Prop
⊢ (∀ (m n : ℕ+), P m n) ↔ ∀ (m n : ℕ), P m.succPNat n.succPNat
Tactic:
rw [pnat_to_nat_prop]
Proof state after:
P : ℕ+ → ℕ+ → Prop
⊢ (∀ (n : ℕ) (n_1 : ℕ+), P n.succPNat n_1) ↔ ∀ (m n : ℕ), P m.succPNat n.succPNat
Theorem: Imo2009P5.pnat_to_nat_prop2
Proof state before:
P : ℕ+ → ℕ+ → Prop
⊢ (∀ (n : ℕ) (n_1 : ℕ+), P n.succPNat n_1) ↔ ∀ (m n : ℕ), P m.succPNat n.succPNat
Tactic:
refine forall_congr' (λ m ↦ ?_)
Proof state after:
P : ℕ+ → ℕ+ → Prop
m : ℕ
⊢ (∀ (n : ℕ+), P m.succPNat n) ↔ ∀ (n : ℕ), P m.succPNat n.succPNat
Theorem: Imo2009P5.pnat_to_nat_prop2
Proof state before:
P : ℕ+ → ℕ+ → Prop
m : ℕ
⊢ (∀ (n : ℕ+), P m.succPNat n) ↔ ∀ (n : ℕ), P m.succPNat n.succPNat
Tactic:
rw [pnat_to_nat_prop]
Proof state after:
no goals
Theorem: Imo2009P5.succ_pnat_add_succ_pnat
Proof state before:
m n : ℕ
⊢ m.succPNat + n.succPNat = (m + n).succPNat + 1
Tactic:
rw [← PNat.coe_inj, PNat.add_coe, PNat.add_coe, Nat.succPNat_coe, Nat.succPNat_coe,
    Nat.succPNat_coe, Nat.add_succ, Nat.succ_add]
Proof state after:
m n : ℕ
⊢ (m + n).succ.succ = (m + n).succ + ↑1
Theorem: Imo2009P5.succ_pnat_add_succ_pnat
Proof state before:
m n : ℕ
⊢ (m + n).succ.succ = (m + n).succ + ↑1
Tactic:
rfl
Proof state after:
no goals
Theorem: Imo2009P5.pnat_add_sub_cancel
Proof state before:
m n : ℕ+
⊢ m + n - n = m
Tactic:
rw [← add_right_inj n, PNat.add_sub_of_lt (n.lt_add_left m), add_comm]
Proof state after:
no goals
Theorem: Imo2009P5.final_solution_nat
Proof state before:
f : ℕ → ℕ
⊢ ((∀ (x y : ℕ), f (y + f x) ≤ f y + x) ∧ (∀ (x y : ℕ), x ≤ f y + f (y + f x)) ∧ ∀ (x y : ℕ), f y ≤ f (y + f x) + x) ↔
    f = fun x => x
Tactic:
symm
Proof state after:
f : ℕ → ℕ
⊢ (f = fun x => x) ↔
    (∀ (x y : ℕ), f (y + f x) ≤ f y + x) ∧ (∀ (x y : ℕ), x ≤ f y + f (y + f x)) ∧ ∀ (x y : ℕ), f y ≤ f (y + f x) + x
Theorem: Imo2009P5.final_solution_nat
Proof state before:
f : ℕ → ℕ
⊢ (f = fun x => x) ↔
    (∀ (x y : ℕ), f (y + f x) ≤ f y + x) ∧ (∀ (x y : ℕ), x ≤ f y + f (y + f x)) ∧ ∀ (x y : ℕ), f y ≤ f (y + f x) + x
Tactic:
constructor
Proof state after:
case mp
f : ℕ → ℕ
⊢ (f = fun x => x) →
    (∀ (x y : ℕ), f (y + f x) ≤ f y + x) ∧ (∀ (x y : ℕ), x ≤ f y + f (y + f x)) ∧ ∀ (x y : ℕ), f y ≤ f (y + f x) + x

case mpr
f : ℕ → ℕ
⊢ ((∀ (x y : ℕ), f (y + f x) ≤ f y + x) ∧ (∀ (x y : ℕ), x ≤ f y + f (y + f x)) ∧ ∀ (x y : ℕ), f y ≤ f (y + f x) + x) →
    f = fun x => x
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case mpr
f : ℕ → ℕ
⊢ ((∀ (x y : ℕ), f (y + f x) ≤ f y + x) ∧ (∀ (x y : ℕ), x ≤ f y + f (y + f x)) ∧ ∀ (x y : ℕ), f y ≤ f (y + f x) + x) →
    f = fun x => x
Tactic:
rintro ⟨h, h0, h1⟩
Proof state after:
case mpr.intro.intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
⊢ f = fun x => x
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case mpr.intro.intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
⊢ f = fun x => x
Tactic:
replace h1 : f 0 = 0 := by
  contrapose! h0; rw [← zero_lt_iff] at h0
  obtain ⟨K, h2⟩ := exists_sup_fn_fin f (f 0)
  refine ⟨K + K + 1, 0, Nat.lt_succ_of_le (add_le_add (h2 0 h0) ?_)⟩
  rw [zero_add, ← Function.Periodic.map_mod_nat (λ y ↦ le_antisymm (h 0 y) (h1 0 y))]
  exact h2 _ (Nat.mod_lt (f (K + K + 1)) h0)
Proof state after:
case mpr.intro.intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : f 0 = 0
⊢ f = fun x => x
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case mpr.intro.intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : f 0 = 0
⊢ f = fun x => x
Tactic:
replace h0 : ∀ x : ℕ, f (f x) = x := by
  intros x; apply le_antisymm
  replace h := h x 0
  rwa [h1, zero_add, zero_add] at h
  replace h0 := h0 x 0
  rwa [h1, zero_add, zero_add] at h0
Proof state after:
case mpr.intro.intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
⊢ f = fun x => x
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case mpr.intro.intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
⊢ f = fun x => x
Tactic:
replace h := h 1
Proof state after:
case mpr.intro.intro
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
⊢ f = fun x => x
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case mpr.intro.intro
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
h2 : f 1 = 1
⊢ f = fun x => x
Tactic:
funext x
Proof state after:
case mpr.intro.intro.h
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
h2 : f 1 = 1
x : ℕ
⊢ f x = x
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case mpr.intro.intro.h
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
h2 : f 1 = 1
x : ℕ
⊢ f x = x
Tactic:
induction' x using Nat.strong_induction_on with x x_ih
Proof state after:
case mpr.intro.intro.h.h
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x, f m = m
⊢ f x = x
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case mpr.intro.intro.h.h
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x, f m = m
⊢ f x = x
Tactic:
cases' x with x
Proof state after:
case mpr.intro.intro.h.h.zero
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
h2 : f 1 = 1
x_ih : ∀ m < 0, f m = m
⊢ f 0 = 0

case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x + 1, f m = m
⊢ f (x + 1) = x + 1
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x + 1, f m = m
⊢ f (x + 1) = x + 1
Tactic:
replace h := h x
Proof state after:
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x + 1, f m = m
h : f (x + f 1) ≤ f x + 1
⊢ f (x + 1) = x + 1
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x + 1, f m = m
h : f (x + f 1) ≤ f x + 1
⊢ f (x + 1) = x + 1
Tactic:
rw [h2, x_ih x x.lt_succ_self, le_iff_eq_or_lt, Nat.lt_succ_iff] at h
Proof state after:
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x + 1, f m = m
h : f (x + 1) = x + 1 ∨ f (x + 1) ≤ x
⊢ f (x + 1) = x + 1
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x + 1, f m = m
h : f (x + 1) = x + 1 ∨ f (x + 1) ≤ x
⊢ f (x + 1) = x + 1
Tactic:
revert h
Proof state after:
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x + 1, f m = m
⊢ f (x + 1) = x + 1 ∨ f (x + 1) ≤ x → f (x + 1) = x + 1
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x + 1, f m = m
⊢ f (x + 1) = x + 1 ∨ f (x + 1) ≤ x → f (x + 1) = x + 1
Tactic:
refine (or_iff_left_of_imp (λ h ↦ ?_)).mp
Proof state after:
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x + 1, f m = m
h : f (x + 1) ≤ x
⊢ f (x + 1) = x + 1
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h2 : f 1 = 1
x : ℕ
x_ih : ∀ m < x + 1, f m = m
h : f (x + 1) ≤ x
⊢ f (x + 1) = x + 1
Tactic:
replace x_ih := congr_arg f (x_ih _ (lt_of_le_of_lt h x.lt_succ_self))
Proof state after:
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h2 : f 1 = 1
x : ℕ
h : f (x + 1) ≤ x
x_ih : f (f (f (x + 1))) = f (f (x + 1))
⊢ f (x + 1) = x + 1
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case mpr.intro.intro.h.h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h2 : f 1 = 1
x : ℕ
h : f (x + 1) ≤ x
x_ih : f (f (f (x + 1))) = f (f (x + 1))
⊢ f (x + 1) = x + 1
Tactic:
rwa [h0, h0] at x_ih
Proof state after:
no goals
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case mp
f : ℕ → ℕ
⊢ (f = fun x => x) →
    (∀ (x y : ℕ), f (y + f x) ≤ f y + x) ∧ (∀ (x y : ℕ), x ≤ f y + f (y + f x)) ∧ ∀ (x y : ℕ), f y ≤ f (y + f x) + x
Tactic:
rintro rfl
Proof state after:
case mp

⊢ (∀ (x y : ℕ), (fun x => x) (y + (fun x => x) x) ≤ (fun x => x) y + x) ∧
    (∀ (x y : ℕ), x ≤ (fun x => x) y + (fun x => x) (y + (fun x => x) x)) ∧
      ∀ (x y : ℕ), (fun x => x) y ≤ (fun x => x) (y + (fun x => x) x) + x
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case mp

⊢ (∀ (x y : ℕ), (fun x => x) (y + (fun x => x) x) ≤ (fun x => x) y + x) ∧
    (∀ (x y : ℕ), x ≤ (fun x => x) y + (fun x => x) (y + (fun x => x) x)) ∧
      ∀ (x y : ℕ), (fun x => x) y ≤ (fun x => x) (y + (fun x => x) x) + x
Tactic:
refine ⟨λ x y ↦ le_refl (y + x), λ x y ↦ ?_, λ x y ↦ ?_⟩
Proof state after:
case mp.refine_1
x y : ℕ
⊢ x ≤ (fun x => x) y + (fun x => x) (y + (fun x => x) x)

case mp.refine_2
x y : ℕ
⊢ (fun x => x) y ≤ (fun x => x) (y + (fun x => x) x) + x
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case mp.refine_2
x y : ℕ
⊢ (fun x => x) y ≤ (fun x => x) (y + (fun x => x) x) + x
Tactic:
rw [add_assoc]
Proof state after:
case mp.refine_2
x y : ℕ
⊢ (fun x => x) y ≤ y + ((fun x => x) x + x)
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case mp.refine_2
x y : ℕ
⊢ (fun x => x) y ≤ y + ((fun x => x) x + x)
Tactic:
exact le_self_add
Proof state after:
no goals