internlm/Lean-Github huggingface dataset:
Theorem: Imo1962P1.no_smaller_solutions
Proof state before:
case inl.«3»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 3
h3 : 3 < 6
⊢ False
Tactic:
exact case_3_digit h h2
Proof state after:
no goals
Theorem: Imo1962P1.no_smaller_solutions
Proof state before:
case inl.«4»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 4
h3 : 4 < 6
⊢ n ≥ 153846
Tactic:
exfalso
Proof state after:
case inl.«4»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 4
h3 : 4 < 6
⊢ False
Theorem: Imo1962P1.no_smaller_solutions
Proof state before:
case inl.«4»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 4
h3 : 4 < 6
⊢ False
Tactic:
exact case_4_digit h h2
Proof state after:
no goals
Theorem: Imo1962P1.no_smaller_solutions
Proof state before:
case inl.«5»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 5
h3 : 5 < 6
⊢ n ≥ 153846
Tactic:
have h4 : c = 15384 := case_5_digit h h2
Proof state after:
case inl.«5»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 5
h3 : 5 < 6
h4 : c = 15384
⊢ n ≥ 153846
Theorem: Imo1962P1.no_smaller_solutions
Proof state before:
case inl.«5»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 5
h3 : 5 < 6
h4 : c = 15384
⊢ n ≥ 153846
Tactic:
have h5 : n = 10 * 15384 + 6 := h4 ▸ h2.left
Proof state after:
case inl.«5»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 5
h3 : 5 < 6
h4 : c = 15384
h5 : n = 10 * 15384 + 6
⊢ n ≥ 153846
Theorem: Imo1962P1.no_smaller_solutions
Proof state before:
case inl.«5»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 5
h3 : 5 < 6
h4 : c = 15384
h5 : n = 10 * 15384 + 6
⊢ n ≥ 153846
Tactic:
norm_num at h5
Proof state after:
case inl.«5»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 5
h3 : 5 < 6
h4 : c = 15384
h5 : n = 153846
⊢ n ≥ 153846
Theorem: Imo1962P1.no_smaller_solutions
Proof state before:
case inl.«5»
n : ℕ
h1 : ProblemPredicate n
c : ℕ
h2 : ProblemPredicate' c n
h : (digits 10 c).length = 5
h3 : 5 < 6
h4 : c = 15384
h5 : n = 153846
⊢ n ≥ 153846
Tactic:
exact h5.ge
Proof state after:
no goals
Theorem: Imo2017P2.good_one_sub
Proof state before:
R : Type u_1
inst✝ : Ring R
x y : R
⊢ (fun x => 1 - x) ((fun x => 1 - x) x * (fun x => 1 - x) y) + (fun x => 1 - x) (x + y) = (fun x => 1 - x) (x * y)
Tactic:
noncomm_ring
Proof state after:
no goals
Theorem: Imo2017P2.good_neg
Proof state before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
x y : R
⊢ (-f) ((-f) x * (-f) y) + (-f) (x + y) = (-f) (x * y)
Tactic:
repeat rw [Pi.neg_apply]
Proof state after:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
x y : R
⊢ -f (-f x * -f y) + -f (x + y) = -f (x * y)
Theorem: Imo2017P2.good_neg
Proof state before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
x y : R
⊢ -f (-f x * -f y) + -f (x + y) = -f (x * y)
Tactic:
rw [neg_mul_neg, ← neg_add, h]
Proof state after:
no goals
Theorem: Imo2017P2.good_neg
Proof state before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
x y : R
⊢ -f (-f x * -f y) + -f (x + y) = (-f) (x * y)
Tactic:
rw [Pi.neg_apply]
Proof state after:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
x y : R
⊢ -f (-f x * -f y) + -f (x + y) = -f (x * y)
Theorem: Imo2017P2.good_special_equality
Proof state before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
x y : R
h0 : x * y = 1
⊢ f (f (x + 1) * f (y + 1)) = 0
Tactic:
rw [← add_left_eq_self, h, add_one_mul x, mul_add_one x, h0, add_comm 1 x]
Proof state after:
no goals
Theorem: Imo2017P2.good_map_map_zero_sq
Proof state before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
⊢ f (f 0 ^ 2) = 0
Tactic:
have h1 : (-1 : R) * (-1) = 1 := by rw [neg_mul_neg, mul_one]
Proof state after:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h1 : -1 * -1 = 1
⊢ f (f 0 ^ 2) = 0
Theorem: Imo2017P2.good_map_map_zero_sq
Proof state before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h1 : -1 * -1 = 1
⊢ f (f 0 ^ 2) = 0
Tactic:
have h2 := good_special_equality h h1
Proof state after:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h1 : -1 * -1 = 1
h2 : f (f (-1 + 1) * f (-1 + 1)) = 0
⊢ f (f 0 ^ 2) = 0
Theorem: Imo2017P2.good_map_map_zero_sq
Proof state before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h1 : -1 * -1 = 1
h2 : f (f (-1 + 1) * f (-1 + 1)) = 0
⊢ f (f 0 ^ 2) = 0
Tactic:
rwa [neg_add_self, ← sq] at h2
Proof state after:
no goals
Theorem: Imo2017P2.good_map_map_zero_sq
Proof state before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
⊢ -1 * -1 = 1
Tactic:
rw [neg_mul_neg, mul_one]
Proof state after:
no goals
Theorem: Imo2017P2.good_eq_of_inj
Proof state before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h0 : f 0 = 1
h1 : Injective f
x : R
⊢ f (f x) + f x = 1
Tactic:
rw [← h0, ← mul_zero x, ← h, add_zero, h0, mul_one]
Proof state after:
no goals
Theorem: Imo2017P2.good_eq_of_inj
Proof state before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h0 : f 0 = 1
h1 : Injective f
h2 : ∀ (x : R), f (f x) + f x = 1
x : R
⊢ f x = 1 - x
Tactic:
rw [eq_sub_iff_add_eq', ← h2 x, add_left_inj]
Proof state after:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h0 : f 0 = 1
h1 : Injective f
h2 : ∀ (x : R), f (f x) + f x = 1
x : R
⊢ x = f (f x)
Theorem: Imo2017P2.good_eq_of_inj
Proof state before:
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h0 : f 0 = 1
h1 : Injective f
h2 : ∀ (x : R), f (f x) + f x = 1
x : R
⊢ x = f (f x)
Tactic:
apply h1
Proof state after:
case a
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h0 : f 0 = 1
h1 : Injective f
h2 : ∀ (x : R), f (f x) + f x = 1
x : R
⊢ f x = f (f (f x))
Theorem: Imo2017P2.good_eq_of_inj
Proof state before:
case a
R : Type u_1
inst✝ : Ring R
f : R → R
h : good f
h0 : f 0 = 1
h1 : Injective f
h2 : ∀ (x : R), f (f x) + f x = 1
x : R
⊢ f x = f (f (f x))
Tactic:
rw [← add_left_inj (f (f x)), h2, add_comm, h2]
Proof state after:
no goals
Theorem: Imo2017P2.good_map_eq_zero
Proof state before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f ≠ 0
c : D
h1 : f c = 0
h2 : ¬c = 1
⊢ f = 0
Tactic:
have h3 := good_special_equality h (mul_inv_cancel <| sub_ne_zero_of_ne h2)
Proof state after:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f ≠ 0
c : D
h1 : f c = 0
h2 : ¬c = 1
h3 : f (f (c - 1 + 1) * f ((c - 1)⁻¹ + 1)) = 0
⊢ f = 0
Theorem: Imo2017P2.good_map_eq_zero
Proof state before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f ≠ 0
c : D
h1 : f c = 0
h2 : ¬c = 1
h3 : f (f (c - 1 + 1) * f ((c - 1)⁻¹ + 1)) = 0
⊢ f = 0
Tactic:
rw [sub_add_cancel, h1, zero_mul] at h3
Proof state after:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f ≠ 0
c : D
h1 : f c = 0
h2 : ¬c = 1
h3 : f 0 = 0
⊢ f = 0
Theorem: Imo2017P2.good_map_eq_zero
Proof state before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f ≠ 0
c : D
h1 : f c = 0
h2 : ¬c = 1
h3 : f 0 = 0
⊢ f = 0
Tactic:
ext x
Proof state after:
case h
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f ≠ 0
c : D
h1 : f c = 0
h2 : ¬c = 1
h3 : f 0 = 0
x : D
⊢ f x = 0 x
Theorem: Imo2017P2.good_map_eq_zero
Proof state before:
case h
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f ≠ 0
c : D
h1 : f c = 0
h2 : ¬c = 1
h3 : f 0 = 0
x : D
⊢ f x = 0 x
Tactic:
rw [Pi.zero_apply, ← h3, ← mul_zero x, ← h,
  h3, mul_zero, h3, zero_add, add_zero]
Proof state after:
no goals
Theorem: Imo2017P2.good_map_eq_zero_iff
Proof state before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f 0 = 1
c : D
h1 : f = 0
⊢ 0 = 1
Tactic:
rwa [h1] at h0
Proof state after:
no goals
Theorem: Imo2017P2.good_shift
Proof state before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f 0 = 1
x : D
⊢ f (x + 1) + 1 = f x
Tactic:
have h1 := h x 1
Proof state after:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f 0 = 1
x : D
h1 : f (f x * f 1) + f (x + 1) = f (x * 1)
⊢ f (x + 1) + 1 = f x
Theorem: Imo2017P2.good_shift
Proof state before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f 0 = 1
x : D
h1 : f (f x * f 1) + f (x + 1) = f (x * 1)
⊢ f (x + 1) + 1 = f x
Tactic:
rwa [good_map_one h, mul_zero, h0, add_comm, mul_one] at h1
Proof state after:
no goals
Theorem: Imo2017P2.good_shift2
Proof state before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f 0 = 1
x : D
⊢ f (x - 1) = f x + 1
Tactic:
rw [← good_shift h h0, sub_add_cancel]
Proof state after:
no goals
Theorem: Imo2017P2.good_map_add_one_eq_zero_iff
Proof state before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h : good f
h0 : f 0 = 1
x : D
⊢ f (x + 1) = 0 ↔ x = 0
Tactic:
rw [good_map_eq_zero_iff h h0, add_left_eq_self]
Proof state after:
no goals
Theorem: Imo2017P2.solution_of_map_zero_eq_one_imp_injective
Proof state before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
f : D → D
⊢ good f ↔ f = 0 ∨ (f = fun x => 1 - x) ∨ f = -fun x => 1 - x
Tactic:
constructor
Proof state after:
case mp
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
f : D → D
⊢ good f → f = 0 ∨ (f = fun x => 1 - x) ∨ f = -fun x => 1 - x

case mpr
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
f : D → D
⊢ (f = 0 ∨ (f = fun x => 1 - x) ∨ f = -fun x => 1 - x) → good f
Theorem: Imo2017P2.solution_of_map_zero_eq_one_imp_injective
Proof state before:
case mp
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
f : D → D
⊢ good f → f = 0 ∨ (f = fun x => 1 - x) ∨ f = -fun x => 1 - x
Tactic:
rw [or_iff_not_imp_left]
Proof state after:
case mp
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
f : D → D
⊢ good f → ¬f = 0 → (f = fun x => 1 - x) ∨ f = -fun x => 1 - x
Theorem: Imo2017P2.solution_of_map_zero_eq_one_imp_injective
Proof state before:
case mp
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
f : D → D
⊢ good f → ¬f = 0 → (f = fun x => 1 - x) ∨ f = -fun x => 1 - x
Tactic:
intros h0 h1
Proof state after:
case mp
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
f : D → D
h0 : good f
h1 : ¬f = 0
⊢ (f = fun x => 1 - x) ∨ f = -fun x => 1 - x
Theorem: Imo2017P2.solution_of_map_zero_eq_one_imp_injective
Proof state before:
case mp
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
f : D → D
h0 : good f
h1 : ¬f = 0
⊢ (f = fun x => 1 - x) ∨ f = -fun x => 1 - x
Tactic:
apply (good_map_zero h0 h1).imp <;> intro h1
Proof state after:
case mp.f
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : f 0 = 1
⊢ f = fun x => 1 - x

case mp.g
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : f 0 = -1
⊢ f = -fun x => 1 - x
Theorem: Imo2017P2.solution_of_map_zero_eq_one_imp_injective
Proof state before:
case mp.f
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : f 0 = 1
⊢ f = fun x => 1 - x
Tactic:
exact good_eq_of_inj h0 h1 (h f h0 h1)
Proof state after:
no goals
Theorem: Imo2017P2.solution_of_map_zero_eq_one_imp_injective
Proof state before:
case mp.g
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : f 0 = -1
⊢ f = -fun x => 1 - x
Tactic:
rw [← neg_eq_iff_eq_neg] at h1 ⊢
Proof state after:
case mp.g
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : -f 0 = 1
⊢ -f = fun x => 1 - x
Theorem: Imo2017P2.solution_of_map_zero_eq_one_imp_injective
Proof state before:
case mp.g
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : -f 0 = 1
⊢ -f = fun x => 1 - x
Tactic:
have h2 := good_neg h0
Proof state after:
case mp.g
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : -f 0 = 1
h2 : good (-f)
⊢ -f = fun x => 1 - x
Theorem: Imo2017P2.solution_of_map_zero_eq_one_imp_injective
Proof state before:
case mp.g
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : -f 0 = 1
h2 : good (-f)
⊢ -f = fun x => 1 - x
Tactic:
exact good_eq_of_inj h2 h1 (h (-f) h2 h1)
Proof state after:
no goals
Theorem: Imo2017P2.solution_of_map_zero_eq_one_imp_injective
Proof state before:
case mpr
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
f : D → D
⊢ (f = 0 ∨ (f = fun x => 1 - x) ∨ f = -fun x => 1 - x) → good f
Tactic:
intro h0
Proof state after:
case mpr
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
f : D → D
h0 : f = 0 ∨ (f = fun x => 1 - x) ∨ f = -fun x => 1 - x
⊢ good f
Theorem: Imo2017P2.solution_of_map_zero_eq_one_imp_injective
Proof state before:
case mpr
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
f : D → D
h0 : f = 0 ∨ (f = fun x => 1 - x) ∨ f = -fun x => 1 - x
⊢ good f
Tactic:
rcases h0 with rfl | rfl | rfl
Proof state after:
case mpr.inl
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h✝ : good f
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
⊢ good 0

case mpr.inr.inl
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h✝ : good f
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
⊢ good fun x => 1 - x

case mpr.inr.inr
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h✝ : good f
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
⊢ good (-fun x => 1 - x)
Theorem: Imo2017P2.solution_of_map_zero_eq_one_imp_injective
Proof state before:
case mpr.inl
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h✝ : good f
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
⊢ good 0

case mpr.inr.inl
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h✝ : good f
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
⊢ good fun x => 1 - x

case mpr.inr.inr
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f : D → D
h✝ : good f
h : ∀ (f : D → D), good f → f 0 = 1 → Injective f
⊢ good (-fun x => 1 - x)
Tactic:
exacts [good_zero, good_one_sub, good_neg good_one_sub]
Proof state after:
no goals
Theorem: Imo2017P2.case1_injective
Proof state before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
⊢ Injective f
Tactic:
have h2 := good_shift2 h0 h1
Proof state after:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : D), f (x - 1) = f x + 1
⊢ Injective f
Theorem: Imo2017P2.case1_injective
Proof state before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : D), f (x - 1) = f x + 1
h3 : ∀ (y : D), f (2 * f y) + 1 + f y = f (-y)
⊢ Injective f
Tactic:
replace h2 : ∀ y, f y = f (-y) → y = 0 := λ y h4 ↦ by
  rwa [← h3, self_eq_add_left, ← h2, good_map_eq_zero_iff h0 h1,
    sub_eq_iff_eq_add, one_add_one_eq_two, mul_right_eq_self₀,
    or_iff_left h, ← add_sub_cancel_right y 1, h2, add_left_eq_self,
    good_map_add_one_eq_zero_iff h0 h1] at h4
Proof state after:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h3 : ∀ (y : D), f (2 * f y) + 1 + f y = f (-y)
h2 : ∀ (y : D), f y = f (-y) → y = 0
⊢ Injective f
Theorem: Imo2017P2.case1_injective
Proof state before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h3 : ∀ (y : D), f (2 * f y) + 1 + f y = f (-y)
h2 : ∀ (y : D), f y = f (-y) → y = 0
⊢ Injective f
Tactic:
intros a b h4
Proof state after:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h3 : ∀ (y : D), f (2 * f y) + 1 + f y = f (-y)
h2 : ∀ (y : D), f y = f (-y) → y = 0
a b : D
h4 : f a = f b
⊢ a = b
Theorem: Imo2017P2.case1_injective
Proof state before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h3 : ∀ (y : D), f (2 * f y) + 1 + f y = f (-y)
h2 : ∀ (y : D), f y = f (-y) → y = 0
a b : D
h4 : f a = f b
⊢ a = b
Tactic:
refine eq_of_sub_eq_zero (h2 _ ?_)
Proof state after:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h3 : ∀ (y : D), f (2 * f y) + 1 + f y = f (-y)
h2 : ∀ (y : D), f y = f (-y) → y = 0
a b : D
h4 : f a = f b
⊢ f (a - b) = f (-(a - b))
Theorem: Imo2017P2.case1_injective
Proof state before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h3 : ∀ (y : D), f (2 * f y) + 1 + f y = f (-y)
h2 : ∀ (y : D), f y = f (-y) → y = 0
a b : D
h4 : f a = f b
⊢ f (a - b) = f (-(a - b))
Tactic:
have h5 : ∀ y z, f y = f z → f (-y) = f (-z) :=
  λ y z h5 ↦ by rw [← h3, h5, h3]
Proof state after:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h3 : ∀ (y : D), f (2 * f y) + 1 + f y = f (-y)
h2 : ∀ (y : D), f y = f (-y) → y = 0
a b : D
h4 : f a = f b
h5 : ∀ (y z : D), f y = f z → f (-y) = f (-z)
⊢ f (a - b) = f (-(a - b))
Theorem: Imo2017P2.case1_injective
Proof state before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h3 : ∀ (y : D), f (2 * f y) + 1 + f y = f (-y)
h2 : ∀ (y : D), f y = f (-y) → y = 0
a b : D
h4 : f a = f b
h5 : ∀ (y z : D), f y = f z → f (-y) = f (-z)
⊢ f (a - b) = f (-(a - b))
Tactic:
have h6 : f (a * b) = f (b * a) := by rw [← h0, ← h0 b, h4, add_comm a]
Proof state after:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h3 : ∀ (y : D), f (2 * f y) + 1 + f y = f (-y)
h2 : ∀ (y : D), f y = f (-y) → y = 0
a b : D
h4 : f a = f b
h5 : ∀ (y z : D), f y = f z → f (-y) = f (-z)
h6 : f (a * b) = f (b * a)
⊢ f (a - b) = f (-(a - b))
Theorem: Imo2017P2.case1_injective
Proof state before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h3 : ∀ (y : D), f (2 * f y) + 1 + f y = f (-y)
h2 : ∀ (y : D), f y = f (-y) → y = 0
a b : D
h4 : f a = f b
h5 : ∀ (y z : D), f y = f z → f (-y) = f (-z)
h6 : f (a * b) = f (b * a)
⊢ f (a - b) = f (-(a - b))
Tactic:
have h8 := h0 a (-b)
Proof state after:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h3 : ∀ (y : D), f (2 * f y) + 1 + f y = f (-y)
h2 : ∀ (y : D), f y = f (-y) → y = 0
a b : D
h4 : f a = f b
h5 : ∀ (y z : D), f y = f z → f (-y) = f (-z)
h6 : f (a * b) = f (b * a)
h8 : f (f a * f (-b)) + f (a + -b) = f (a * -b)
⊢ f (a - b) = f (-(a - b))
Theorem: Imo2017P2.case1_injective
Proof state before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h3 : ∀ (y : D), f (2 * f y) + 1 + f y = f (-y)
h2 : ∀ (y : D), f y = f (-y) → y = 0
a b : D
h4 : f a = f b
h5 : ∀ (y z : D), f y = f z → f (-y) = f (-z)
h6 : f (a * b) = f (b * a)
h8 : f (f a * f (-b)) + f (a + -b) = f (a * -b)
⊢ f (a - b) = f (-(a - b))
Tactic:
rwa [mul_neg, h5 _ _ h6, ← mul_neg, ← h0 b, h4, h5 a b h4,
  add_right_inj, ← sub_eq_add_neg, ← sub_eq_add_neg, ← neg_sub a] at h8
Proof state after:
no goals
Theorem: Imo2017P2.case1_injective
Proof state before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : D), f (x - 1) = f x + 1
y : D
⊢ f (2 * f y) + 1 + f y = f (-y)
Tactic:
rw [add_assoc, ← neg_one_mul, ← h0 (-1)]
Proof state after:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : D), f (x - 1) = f x + 1
y : D
⊢ f (2 * f y) + (1 + f y) = f (f (-1) * f y) + f (-1 + y)
Theorem: Imo2017P2.case1_injective
Proof state before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : D), f (x - 1) = f x + 1
y : D
⊢ f (2 * f y) + (1 + f y) = f (f (-1) * f y) + f (-1 + y)
Tactic:
refine congr_arg₂ _ ?_ ?_
Proof state after:
case refine_1
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : D), f (x - 1) = f x + 1
y : D
⊢ f (2 * f y) = f (f (-1) * f y)

case refine_2
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : D), f (x - 1) = f x + 1
y : D
⊢ 1 + f y = f (-1 + y)
Theorem: Imo2017P2.case1_injective
Proof state before:
case refine_1
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : D), f (x - 1) = f x + 1
y : D
⊢ f (2 * f y) = f (f (-1) * f y)
Tactic:
rw [← zero_sub, h2, h1, one_add_one_eq_two]
Proof state after:
no goals
Theorem: Imo2017P2.case1_injective
Proof state before:
case refine_2
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : D), f (x - 1) = f x + 1
y : D
⊢ 1 + f y = f (-1 + y)
Tactic:
rw [add_comm, ← h2, neg_add_eq_sub]
Proof state after:
no goals
Theorem: Imo2017P2.case1_injective
Proof state before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : D), f (x - 1) = f x + 1
h3 : ∀ (y : D), f (2 * f y) + 1 + f y = f (-y)
y : D
h4 : f y = f (-y)
⊢ y = 0
Tactic:
rwa [← h3, self_eq_add_left, ← h2, good_map_eq_zero_iff h0 h1,
  sub_eq_iff_eq_add, one_add_one_eq_two, mul_right_eq_self₀,
  or_iff_left h, ← add_sub_cancel_right y 1, h2, add_left_eq_self,
  good_map_add_one_eq_zero_iff h0 h1] at h4
Proof state after:
no goals
Theorem: Imo2017P2.case1_injective
Proof state before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h3 : ∀ (y : D), f (2 * f y) + 1 + f y = f (-y)
h2 : ∀ (y : D), f y = f (-y) → y = 0
a b : D
h4 : f a = f b
y z : D
h5 : f y = f z
⊢ f (-y) = f (-z)
Tactic:
rw [← h3, h5, h3]
Proof state after:
no goals
Theorem: Imo2017P2.case1_injective
Proof state before:
R : Type u_1
D : Type u_2
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
h3 : ∀ (y : D), f (2 * f y) + 1 + f y = f (-y)
h2 : ∀ (y : D), f y = f (-y) → y = 0
a b : D
h4 : f a = f b
h5 : ∀ (y z : D), f y = f z → f (-y) = f (-z)
⊢ f (a * b) = f (b * a)
Tactic:
rw [← h0, ← h0 b, h4, add_comm a]
Proof state after:
no goals
Theorem: Imo2017P2.case2_injective
Proof state before:
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
⊢ Injective f
Tactic:
have h2 := good_shift h0 h1
Proof state after:
R : Type u_1
F : Type u_2
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
h2 : ∀ (x : F), f (x + 1) + 1 = f x
⊢ Injective f