internlm/Lean-Github huggingface dataset:
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case mp.refine_1
x y : ℕ
⊢ x ≤ (fun x => x) y + (fun x => x) (y + (fun x => x) x)
Tactic:
rw [← add_assoc]
Proof state after:
case mp.refine_1
x y : ℕ
⊢ x ≤ (fun x => x) y + y + (fun x => x) x
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case mp.refine_1
x y : ℕ
⊢ x ≤ (fun x => x) y + y + (fun x => x) x
Tactic:
exact le_add_self
Proof state after:
no goals
Theorem: Imo2009P5.final_solution_nat
Proof state before:
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 0 = 0
Tactic:
contrapose! h0
Proof state after:
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
h0 : f 0 ≠ 0
⊢ ∃ x y, f y + f (y + f x) < x
Theorem: Imo2009P5.final_solution_nat
Proof state before:
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
h0 : f 0 ≠ 0
⊢ ∃ x y, f y + f (y + f x) < x
Tactic:
rw [← zero_lt_iff] at h0
Proof state after:
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
h0 : 0 < f 0
⊢ ∃ x y, f y + f (y + f x) < x
Theorem: Imo2009P5.final_solution_nat
Proof state before:
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
h0 : 0 < f 0
⊢ ∃ x y, f y + f (y + f x) < x
Tactic:
obtain ⟨K, h2⟩ := exists_sup_fn_fin f (f 0)
Proof state after:
case intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
h0 : 0 < f 0
K : ℕ
h2 : ∀ n < f 0, f n ≤ K
⊢ ∃ x y, f y + f (y + f x) < x
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
h0 : 0 < f 0
K : ℕ
h2 : ∀ n < f 0, f n ≤ K
⊢ ∃ x y, f y + f (y + f x) < x
Tactic:
refine ⟨K + K + 1, 0, Nat.lt_succ_of_le (add_le_add (h2 0 h0) ?_)⟩
Proof state after:
case intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
h0 : 0 < f 0
K : ℕ
h2 : ∀ n < f 0, f n ≤ K
⊢ f (0 + f (K + K + 1)) ≤ K
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
h0 : 0 < f 0
K : ℕ
h2 : ∀ n < f 0, f n ≤ K
⊢ f (0 + f (K + K + 1)) ≤ K
Tactic:
rw [zero_add, ← Function.Periodic.map_mod_nat (λ y ↦ le_antisymm (h 0 y) (h1 0 y))]
Proof state after:
case intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
h0 : 0 < f 0
K : ℕ
h2 : ∀ n < f 0, f n ≤ K
⊢ f (f (K + K + 1) % f 0) ≤ K
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case intro
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : ∀ (x y : ℕ), f y ≤ f (y + f x) + x
h0 : 0 < f 0
K : ℕ
h2 : ∀ n < f 0, f n ≤ K
⊢ f (f (K + K + 1) % f 0) ≤ K
Tactic:
exact h2 _ (Nat.mod_lt (f (K + K + 1)) h0)
Proof state after:
no goals
Theorem: Imo2009P5.final_solution_nat
Proof state before:
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
⊢ ∀ (x : ℕ), f (f x) = x
Tactic:
intros x
Proof state after:
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
x : ℕ
⊢ f (f x) = x
Theorem: Imo2009P5.final_solution_nat
Proof state before:
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
x : ℕ
⊢ f (f x) = x
Tactic:
apply le_antisymm
Proof state after:
case a
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
x : ℕ
⊢ f (f x) ≤ x

case a
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
x : ℕ
⊢ x ≤ f (f x)
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case a
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
x : ℕ
⊢ f (f x) ≤ x

case a
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
x : ℕ
⊢ x ≤ f (f x)
Tactic:
replace h := h x 0
Proof state after:
case a
f : ℕ → ℕ
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : f 0 = 0
x : ℕ
h : f (0 + f x) ≤ f 0 + x
⊢ f (f x) ≤ x

case a
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
x : ℕ
⊢ x ≤ f (f x)
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case a
f : ℕ → ℕ
h0 : ∀ (x y : ℕ), x ≤ f y + f (y + f x)
h1 : f 0 = 0
x : ℕ
h : f (0 + f x) ≤ f 0 + x
⊢ f (f x) ≤ x

case a
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
x : ℕ
⊢ x ≤ f (f x)
Tactic:
rwa [h1, zero_add, zero_add] at h
Proof state after:
case a
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
x : ℕ
⊢ x ≤ f (f x)
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case a
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
x : ℕ
⊢ x ≤ f (f x)
Tactic:
replace h0 := h0 x 0
Proof state after:
case a
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : f 0 = 0
x : ℕ
h0 : x ≤ f 0 + f (0 + f x)
⊢ x ≤ f (f x)
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case a
f : ℕ → ℕ
h : ∀ (x y : ℕ), f (y + f x) ≤ f y + x
h1 : f 0 = 0
x : ℕ
h0 : x ≤ f 0 + f (0 + f x)
⊢ x ≤ f (f x)
Tactic:
rwa [h1, zero_add, zero_add] at h0
Proof state after:
no goals
Theorem: Imo2009P5.final_solution_nat
Proof state before:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
⊢ f 1 = 1
Tactic:
suffices this : ∀ n : ℕ, f (n * f 1) = n by
  replace this := congr_arg f (this (f 1))
  rw [h0, h0] at this
  exact Nat.eq_one_of_mul_eq_one_left this
Proof state after:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
⊢ ∀ (n : ℕ), f (n * f 1) = n
Theorem: Imo2009P5.final_solution_nat
Proof state before:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
⊢ ∀ (n : ℕ), f (n * f 1) = n
Tactic:
intro n
Proof state after:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
n : ℕ
⊢ f (n * f 1) = n
Theorem: Imo2009P5.final_solution_nat
Proof state before:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
n : ℕ
⊢ f (n * f 1) = n
Tactic:
induction' n using Nat.strong_induction_on with n n_ih
Proof state after:
case h
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
n : ℕ
n_ih : ∀ m < n, f (m * f 1) = m
⊢ f (n * f 1) = n
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case h
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
n : ℕ
n_ih : ∀ m < n, f (m * f 1) = m
⊢ f (n * f 1) = n
Tactic:
cases' n with n
Proof state after:
case h.zero
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
n_ih : ∀ m < 0, f (m * f 1) = m
⊢ f (0 * f 1) = 0

case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
n : ℕ
n_ih : ∀ m < n + 1, f (m * f 1) = m
⊢ f ((n + 1) * f 1) = n + 1
Theorem: Imo2009P5.final_solution_nat
Proof state before:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
this : ∀ (n : ℕ), f (n * f 1) = n
⊢ f 1 = 1
Tactic:
replace this := congr_arg f (this (f 1))
Proof state after:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
this : f (f (f 1 * f 1)) = f (f 1)
⊢ f 1 = 1
Theorem: Imo2009P5.final_solution_nat
Proof state before:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
this : f (f (f 1 * f 1)) = f (f 1)
⊢ f 1 = 1
Tactic:
rw [h0, h0] at this
Proof state after:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
this : f 1 * f 1 = 1
⊢ f 1 = 1
Theorem: Imo2009P5.final_solution_nat
Proof state before:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
this : f 1 * f 1 = 1
⊢ f 1 = 1
Tactic:
exact Nat.eq_one_of_mul_eq_one_left this
Proof state after:
no goals
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case h.zero
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
n_ih : ∀ m < 0, f (m * f 1) = m
⊢ f (0 * f 1) = 0
Tactic:
simp[h1]
Proof state after:
no goals
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
h : ∀ (y : ℕ), f (y + f 1) ≤ f y + 1
n : ℕ
n_ih : ∀ m < n + 1, f (m * f 1) = m
⊢ f ((n + 1) * f 1) = n + 1
Tactic:
replace h := h (n * f 1)
Proof state after:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
n_ih : ∀ m < n + 1, f (m * f 1) = m
h : f (n * f 1 + f 1) ≤ f (n * f 1) + 1
⊢ f ((n + 1) * f 1) = n + 1
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
n_ih : ∀ m < n + 1, f (m * f 1) = m
h : f (n * f 1 + f 1) ≤ f (n * f 1) + 1
⊢ f ((n + 1) * f 1) = n + 1
Tactic:
rw [n_ih n n.lt_succ_self, ← add_one_mul, le_iff_eq_or_lt, Nat.lt_succ_iff] at h
Proof state after:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
n_ih : ∀ m < n + 1, f (m * f 1) = m
h : f ((n + 1) * f 1) = n + 1 ∨ f ((n + 1) * f 1) ≤ n
⊢ f ((n + 1) * f 1) = n + 1
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
n_ih : ∀ m < n + 1, f (m * f 1) = m
h : f ((n + 1) * f 1) = n + 1 ∨ f ((n + 1) * f 1) ≤ n
⊢ f ((n + 1) * f 1) = n + 1
Tactic:
revert h
Proof state after:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
n_ih : ∀ m < n + 1, f (m * f 1) = m
⊢ f ((n + 1) * f 1) = n + 1 ∨ f ((n + 1) * f 1) ≤ n → f ((n + 1) * f 1) = n + 1
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
n_ih : ∀ m < n + 1, f (m * f 1) = m
⊢ f ((n + 1) * f 1) = n + 1 ∨ f ((n + 1) * f 1) ≤ n → f ((n + 1) * f 1) = n + 1
Tactic:
refine (or_iff_left_of_imp (λ h ↦ ?_)).mp
Proof state after:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
n_ih : ∀ m < n + 1, f (m * f 1) = m
h : f ((n + 1) * f 1) ≤ n
⊢ f ((n + 1) * f 1) = n + 1
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
n_ih : ∀ m < n + 1, f (m * f 1) = m
h : f ((n + 1) * f 1) ≤ n
⊢ f ((n + 1) * f 1) = n + 1
Tactic:
replace n_ih := congr_arg f (n_ih _ (lt_of_le_of_lt h n.lt_succ_self))
Proof state after:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
n_ih : f (f (f ((n + 1) * f 1) * f 1)) = f (f ((n + 1) * f 1))
⊢ f ((n + 1) * f 1) = n + 1
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
n_ih : f (f (f ((n + 1) * f 1) * f 1)) = f (f ((n + 1) * f 1))
⊢ f ((n + 1) * f 1) = n + 1
Tactic:
rw [h0, h0, mul_eq_mul_right_iff] at n_ih
Proof state after:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
n_ih : f ((n + 1) * f 1) = n + 1 ∨ f 1 = 0
⊢ f ((n + 1) * f 1) = n + 1
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
n_ih : f ((n + 1) * f 1) = n + 1 ∨ f 1 = 0
⊢ f ((n + 1) * f 1) = n + 1
Tactic:
revert n_ih
Proof state after:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
⊢ f ((n + 1) * f 1) = n + 1 ∨ f 1 = 0 → f ((n + 1) * f 1) = n + 1
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
⊢ f ((n + 1) * f 1) = n + 1 ∨ f 1 = 0 → f ((n + 1) * f 1) = n + 1
Tactic:
refine (or_iff_left ?_).mp
Proof state after:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
⊢ ¬f 1 = 0
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
⊢ ¬f 1 = 0
Tactic:
rw [← h1]
Proof state after:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
⊢ ¬f 1 = f 0
Theorem: Imo2009P5.final_solution_nat
Proof state before:
case h.succ
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
⊢ ¬f 1 = f 0
Tactic:
apply_fun f
Proof state after:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
⊢ f (f 1) ≠ f (f 0)
Theorem: Imo2009P5.final_solution_nat
Proof state before:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
⊢ f (f 1) ≠ f (f 0)
Tactic:
rw [h0, h0]
Proof state after:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
⊢ 1 ≠ 0
Theorem: Imo2009P5.final_solution_nat
Proof state before:
f : ℕ → ℕ
h1 : f 0 = 0
h0 : ∀ (x : ℕ), f (f x) = x
n : ℕ
h : f ((n + 1) * f 1) ≤ n
⊢ 1 ≠ 0
Tactic:
exact one_ne_zero
Proof state after:
no goals
Theorem: Imo2009P5.final_solution_nat
Proof state before:
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
Tactic:
exact h1
Proof state after:
no goals
Theorem: Imo2009P5.final_solution_pnat
Proof state before:
f : ℕ+ → ℕ+
⊢ ((∀ (x y : ℕ+), f (y + f x - 1) < f y + x) ∧
      (∀ (x y : ℕ+), x < f y + f (y + f x - 1)) ∧ ∀ (x y : ℕ+), f y < f (y + f x - 1) + x) ↔
    f = fun x => x
Tactic:
obtain ⟨g, rfl⟩ : ∃ g : ℕ → ℕ, f = λ x ↦ (g x.natPred).succPNat :=
  ⟨λ x ↦ (f x.succPNat).natPred,
    funext (λ x ↦ by rw [PNat.succPNat_natPred, PNat.succPNat_natPred])⟩
Proof state after:
case intro
g : ℕ → ℕ
⊢ ((∀ (x y : ℕ+),
        (fun x => (g x.natPred).succPNat) (y + (fun x => (g x.natPred).succPNat) x - 1) <
          (fun x => (g x.natPred).succPNat) y + x) ∧
      (∀ (x y : ℕ+),
          x <
            (fun x => (g x.natPred).succPNat) y +
              (fun x => (g x.natPred).succPNat) (y + (fun x => (g x.natPred).succPNat) x - 1)) ∧
        ∀ (x y : ℕ+),
          (fun x => (g x.natPred).succPNat) y <
            (fun x => (g x.natPred).succPNat) (y + (fun x => (g x.natPred).succPNat) x - 1) + x) ↔
    (fun x => (g x.natPred).succPNat) = fun x => x
Theorem: Imo2009P5.final_solution_pnat
Proof state before:
case intro
g : ℕ → ℕ
⊢ ((∀ (x y : ℕ+),
        (fun x => (g x.natPred).succPNat) (y + (fun x => (g x.natPred).succPNat) x - 1) <
          (fun x => (g x.natPred).succPNat) y + x) ∧
      (∀ (x y : ℕ+),
          x <
            (fun x => (g x.natPred).succPNat) y +
              (fun x => (g x.natPred).succPNat) (y + (fun x => (g x.natPred).succPNat) x - 1)) ∧
        ∀ (x y : ℕ+),
          (fun x => (g x.natPred).succPNat) y <
            (fun x => (g x.natPred).succPNat) (y + (fun x => (g x.natPred).succPNat) x - 1) + x) ↔
    (fun x => (g x.natPred).succPNat) = fun x => x
Tactic:
simp_rw [pnat_to_nat_prop2, Function.funext_iff, pnat_to_nat_prop, Nat.natPred_succPNat,
         Nat.succPNat_inj, ← Function.funext_iff, succ_pnat_add_succ_pnat, pnat_add_sub_cancel,
         Nat.natPred_succPNat, PNat.lt_add_one_iff, Nat.succPNat_le_succPNat]
Proof state after:
case intro
g : ℕ → ℕ
⊢ ((∀ (m n : ℕ), g (n + g m) ≤ g n + m) ∧ (∀ (m n : ℕ), m ≤ g n + g (n + g m)) ∧ ∀ (m n : ℕ), g n ≤ g (n + g m) + m) ↔
    (fun a => g a) = fun a => a
Theorem: Imo2009P5.final_solution_pnat
Proof state before:
case intro
g : ℕ → ℕ
⊢ ((∀ (m n : ℕ), g (n + g m) ≤ g n + m) ∧ (∀ (m n : ℕ), m ≤ g n + g (n + g m)) ∧ ∀ (m n : ℕ), g n ≤ g (n + g m) + m) ↔
    (fun a => g a) = fun a => a
Tactic:
exact final_solution_nat g
Proof state after:
no goals
Theorem: Imo2009P5.final_solution_pnat
Proof state before:
f : ℕ+ → ℕ+
x : ℕ+
⊢ f x = ((fun x => (f x.succPNat).natPred) x.natPred).succPNat
Tactic:
rw [PNat.succPNat_natPred, PNat.succPNat_natPred]
Proof state after:
no goals
Theorem: Imo2008P2.subst_abc
Proof state before:
x y z : ℝ
h : x * y * z = 1
⊢ ∃ a b c, a ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0 ∧ x = a / b ∧ y = b / c ∧ z = c / a
Tactic:
use x, 1, 1 / y
Proof state after:
case h
x y z : ℝ
h : x * y * z = 1
⊢ x ≠ 0 ∧ 1 ≠ 0 ∧ 1 / y ≠ 0 ∧ x = x / 1 ∧ y = 1 / (1 / y) ∧ z = 1 / y / x
Theorem: Imo2008P2.subst_abc
Proof state before:
case h
x y z : ℝ
h : x * y * z = 1
⊢ x ≠ 0 ∧ 1 ≠ 0 ∧ 1 / y ≠ 0 ∧ x = x / 1 ∧ y = 1 / (1 / y) ∧ z = 1 / y / x
Tactic:
obtain ⟨⟨hx, hy⟩, _⟩ : (x ≠ 0 ∧ y ≠ 0) ∧ z ≠ 0 := by
  have := h.symm ▸ one_ne_zero
  simpa [not_or] using this
Proof state after:
case h.intro.intro
x y z : ℝ
h : x * y * z = 1
right✝ : z ≠ 0
hx : x ≠ 0
hy : y ≠ 0
⊢ x ≠ 0 ∧ 1 ≠ 0 ∧ 1 / y ≠ 0 ∧ x = x / 1 ∧ y = 1 / (1 / y) ∧ z = 1 / y / x
Theorem: Imo2008P2.subst_abc
Proof state before:
case h.intro.intro
x y z : ℝ
h : x * y * z = 1
right✝ : z ≠ 0
hx : x ≠ 0
hy : y ≠ 0
⊢ x ≠ 0 ∧ 1 ≠ 0 ∧ 1 / y ≠ 0 ∧ x = x / 1 ∧ y = 1 / (1 / y) ∧ z = 1 / y / x
Tactic:
have : z * (y * x) = 1 := by rw [← h]; ac_rfl
Proof state after:
case h.intro.intro
x y z : ℝ
h : x * y * z = 1
right✝ : z ≠ 0
hx : x ≠ 0
hy : y ≠ 0
this : z * (y * x) = 1
⊢ x ≠ 0 ∧ 1 ≠ 0 ∧ 1 / y ≠ 0 ∧ x = x / 1 ∧ y = 1 / (1 / y) ∧ z = 1 / y / x
Theorem: Imo2008P2.subst_abc
Proof state before:
case h.intro.intro
x y z : ℝ
h : x * y * z = 1
right✝ : z ≠ 0
hx : x ≠ 0
hy : y ≠ 0
this : z * (y * x) = 1
⊢ x ≠ 0 ∧ 1 ≠ 0 ∧ 1 / y ≠ 0 ∧ x = x / 1 ∧ y = 1 / (1 / y) ∧ z = 1 / y / x
Tactic:
field_simp [*]
Proof state after:
no goals
Theorem: Imo2008P2.subst_abc
Proof state before:
x y z : ℝ
h : x * y * z = 1
⊢ (x ≠ 0 ∧ y ≠ 0) ∧ z ≠ 0
Tactic:
have := h.symm ▸ one_ne_zero
Proof state after:
x y z : ℝ
h : x * y * z = 1
this : x * y * z ≠ 0
⊢ (x ≠ 0 ∧ y ≠ 0) ∧ z ≠ 0
Theorem: Imo2008P2.subst_abc
Proof state before:
x y z : ℝ
h : x * y * z = 1
this : x * y * z ≠ 0
⊢ (x ≠ 0 ∧ y ≠ 0) ∧ z ≠ 0
Tactic:
simpa [not_or] using this
Proof state after:
no goals
Theorem: Imo2008P2.subst_abc
Proof state before:
x y z : ℝ
h : x * y * z = 1
right✝ : z ≠ 0
hx : x ≠ 0
hy : y ≠ 0
⊢ z * (y * x) = 1
Tactic:
rw [← h]
Proof state after:
x y z : ℝ
h : x * y * z = 1
right✝ : z ≠ 0
hx : x ≠ 0
hy : y ≠ 0
⊢ z * (y * x) = x * y * z
Theorem: Imo2008P2.subst_abc
Proof state before:
x y z : ℝ
h : x * y * z = 1
right✝ : z ≠ 0
hx : x ≠ 0
hy : y ≠ 0
⊢ z * (y * x) = x * y * z
Tactic:
ac_rfl
Proof state after:
no goals
Theorem: Imo1969P1.left_factor_large
Proof state before:
m n : ℤ
h : 1 < m
⊢ 1 < (n - m) ^ 2 + m ^ 2
Tactic:
nlinarith
Proof state after:
no goals
Theorem: Imo1969P1.right_factor_large
Proof state before:
m n : ℤ
h : 1 < m
⊢ 1 < (n + m) ^ 2 + m ^ 2
Tactic:
nlinarith
Proof state after:
no goals
Theorem: Imo1969P1.int_large
Proof state before:
m : ℤ
h : 1 < m
⊢ 1 < m.natAbs
Tactic:
exact_mod_cast lt_of_lt_of_le h le_natAbs
Proof state after:
no goals
Theorem: Imo1969P1.polynomial_not_prime
Proof state before:
m : ℕ
h1 : 1 < m
n : ℕ
⊢ ¬(n ^ 4 + 4 * m ^ 4).Prime
Tactic:
have h2 : 1 < (m : ℤ) := Int.ofNat_lt.mpr h1
Proof state after:
m : ℕ
h1 : 1 < m
n : ℕ
h2 : 1 < ↑m
⊢ ¬(n ^ 4 + 4 * m ^ 4).Prime
Theorem: Imo1969P1.polynomial_not_prime
Proof state before:
m : ℕ
h1 : 1 < m
n : ℕ
h2 : 1 < ↑m
⊢ ¬(n ^ 4 + 4 * m ^ 4).Prime
Tactic:
refine not_prime_of_int_mul' (left_factor_large (n : ℤ) h2) (right_factor_large (n : ℤ) h2) ?_
Proof state after:
m : ℕ
h1 : 1 < m
n : ℕ
h2 : 1 < ↑m
⊢ ((↑n - ↑m) ^ 2 + ↑m ^ 2) * ((↑n + ↑m) ^ 2 + ↑m ^ 2) = ↑(n ^ 4 + 4 * m ^ 4)
Theorem: Imo1969P1.polynomial_not_prime
Proof state before:
m : ℕ
h1 : 1 < m
n : ℕ
h2 : 1 < ↑m
⊢ ((↑n - ↑m) ^ 2 + ↑m ^ 2) * ((↑n + ↑m) ^ 2 + ↑m ^ 2) = ↑(n ^ 4 + 4 * m ^ 4)
Tactic:
apply factorization
Proof state after:
no goals
Theorem: Imo1969P1.aChoice_good
Proof state before:
b : ℕ
⊢ 1 < 2 + b
Tactic:
omega
Proof state after:
no goals
Theorem: Imo1969P1.aChoice_strictMono
Proof state before:
⊢ 4 ≠ 0
Tactic:
decide
Proof state after:
no goals
Theorem: Imo1969P1.aChoice_strictMono
Proof state before:
⊢ 0 < 4
Tactic:
decide
Proof state after:
no goals
Theorem: Usa2019P1.f_injective
Proof state before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
⊢ Function.Injective f
Tactic:
intro p q hpq
Proof state after:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
⊢ p = q
Theorem: Usa2019P1.f_injective
Proof state before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
⊢ p = q
Tactic:
have h1 : f^[2] p = f^[2] q := by
  apply_fun f at hpq
  exact hpq
Proof state after:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
⊢ p = q
Theorem: Usa2019P1.f_injective
Proof state before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
⊢ p = q
Tactic:
have h2 : ∀ n : ℕ+, f^[n] p = f^[n] q := by
  intro n
  obtain ⟨n, hn⟩ := n
  cases' n with n <;> aesop
Proof state after:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
h2 : ∀ (n : ℕ+), f^[↑n] p = f^[↑n] q
⊢ p = q
Theorem: Usa2019P1.f_injective
Proof state before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
h2 : ∀ (n : ℕ+), f^[↑n] p = f^[↑n] q
⊢ p = q
Tactic:
have h3 : f^[f p] p = f^[f q] q := by rw[hpq]; exact h2 (f q)
Proof state after:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
h2 : ∀ (n : ℕ+), f^[↑n] p = f^[↑n] q
h3 : f^[↑(f p)] p = f^[↑(f q)] q
⊢ p = q
Theorem: Usa2019P1.f_injective
Proof state before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
h2 : ∀ (n : ℕ+), f^[↑n] p = f^[↑n] q
h3 : f^[↑(f p)] p = f^[↑(f q)] q
⊢ p = q
Tactic:
have h4 :=
  calc p^2
    = f^[f p] p * f^[2] p := (hf p).symm
  _ = f^[f q] q * f^[2] q := by rw[h3, h1]
  _ = q^2 := hf q
Proof state after:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
h2 : ∀ (n : ℕ+), f^[↑n] p = f^[↑n] q
h3 : f^[↑(f p)] p = f^[↑(f q)] q
h4 : p ^ 2 = q ^ 2
⊢ p = q
Theorem: Usa2019P1.f_injective
Proof state before:
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
h2 : ∀ (n : ℕ+), f^[↑n] p = f^[↑n] q
h3 : f^[↑(f p)] p = f^[↑(f q)] q
h4 : p ^ 2 = q ^ 2
⊢ p = q
Tactic:
obtain ⟨p, hp⟩ := p
Proof state after:
case mk
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
q : ℕ+
p : ℕ
hp : 0 < p
hpq : f ⟨p, hp⟩ = f q
h1 : f^[2] ⟨p, hp⟩ = f^[2] q
h2 : ∀ (n : ℕ+), f^[↑n] ⟨p, hp⟩ = f^[↑n] q
h3 : f^[↑(f ⟨p, hp⟩)] ⟨p, hp⟩ = f^[↑(f q)] q
h4 : ⟨p, hp⟩ ^ 2 = q ^ 2
⊢ ⟨p, hp⟩ = q
Theorem: Usa2019P1.f_injective
Proof state before:
case mk
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
q : ℕ+
p : ℕ
hp : 0 < p
hpq : f ⟨p, hp⟩ = f q
h1 : f^[2] ⟨p, hp⟩ = f^[2] q
h2 : ∀ (n : ℕ+), f^[↑n] ⟨p, hp⟩ = f^[↑n] q
h3 : f^[↑(f ⟨p, hp⟩)] ⟨p, hp⟩ = f^[↑(f q)] q
h4 : ⟨p, hp⟩ ^ 2 = q ^ 2
⊢ ⟨p, hp⟩ = q
Tactic:
obtain ⟨q, hq⟩ := q
Proof state after:
case mk.mk
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p : ℕ
hp : 0 < p
q : ℕ
hq : 0 < q
hpq : f ⟨p, hp⟩ = f ⟨q, hq⟩
h1 : f^[2] ⟨p, hp⟩ = f^[2] ⟨q, hq⟩
h2 : ∀ (n : ℕ+), f^[↑n] ⟨p, hp⟩ = f^[↑n] ⟨q, hq⟩
h3 : f^[↑(f ⟨p, hp⟩)] ⟨p, hp⟩ = f^[↑(f ⟨q, hq⟩)] ⟨q, hq⟩
h4 : ⟨p, hp⟩ ^ 2 = ⟨q, hq⟩ ^ 2
⊢ ⟨p, hp⟩ = ⟨q, hq⟩
Theorem: Usa2019P1.f_injective
Proof state before:
case mk.mk
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p : ℕ
hp : 0 < p
q : ℕ
hq : 0 < q
hpq : f ⟨p, hp⟩ = f ⟨q, hq⟩
h1 : f^[2] ⟨p, hp⟩ = f^[2] ⟨q, hq⟩
h2 : ∀ (n : ℕ+), f^[↑n] ⟨p, hp⟩ = f^[↑n] ⟨q, hq⟩
h3 : f^[↑(f ⟨p, hp⟩)] ⟨p, hp⟩ = f^[↑(f ⟨q, hq⟩)] ⟨q, hq⟩
h4 : ⟨p, hp⟩ ^ 2 = ⟨q, hq⟩ ^ 2
⊢ ⟨p, hp⟩ = ⟨q, hq⟩
Tactic:
congr
Proof state after:
case mk.mk.e_val
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p : ℕ
hp : 0 < p
q : ℕ
hq : 0 < q
hpq : f ⟨p, hp⟩ = f ⟨q, hq⟩
h1 : f^[2] ⟨p, hp⟩ = f^[2] ⟨q, hq⟩
h2 : ∀ (n : ℕ+), f^[↑n] ⟨p, hp⟩ = f^[↑n] ⟨q, hq⟩
h3 : f^[↑(f ⟨p, hp⟩)] ⟨p, hp⟩ = f^[↑(f ⟨q, hq⟩)] ⟨q, hq⟩
h4 : ⟨p, hp⟩ ^ 2 = ⟨q, hq⟩ ^ 2
⊢ p = q