internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2017A6.solution_of_map_zero_eq_one_imp_injective
Proof state before:
case g
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : f 0 = -1
⊢ f = fun x => x - 1
Tactic:
rw [← neg_eq_iff_eq_neg] at h1
Proof state after:
case g
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : -f 0 = 1
⊢ f = fun x => x - 1
Theorem: IMOSL.IMO2017A6.solution_of_map_zero_eq_one_imp_injective
Proof state before:
case g
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : -f 0 = 1
⊢ f = fun x => x - 1
Tactic:
have h2 := good_neg h0
Proof state after:
case g
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : -f 0 = 1
h2 : good (-f)
⊢ f = fun x => x - 1
Theorem: IMOSL.IMO2017A6.solution_of_map_zero_eq_one_imp_injective
Proof state before:
case g
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : -f 0 = 1
h2 : good (-f)
⊢ f = fun x => x - 1
Tactic:
have h3 := good_eq_of_inj h2 h1 (h (-f) h2 h1)
Proof state after:
case g
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : -f 0 = 1
h2 : good (-f)
h3 : -f = fun x => 1 - x
⊢ f = fun x => x - 1
Theorem: IMOSL.IMO2017A6.solution_of_map_zero_eq_one_imp_injective
Proof state before:
case g
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : -f 0 = 1
h2 : good (-f)
h3 : -f = fun x => 1 - x
⊢ f = fun x => x - 1
Tactic:
rw [← neg_inj, h3]
Proof state after:
case g
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : -f 0 = 1
h2 : good (-f)
h3 : -f = fun x => 1 - x
⊢ (fun x => 1 - x) = -fun x => x - 1
Theorem: IMOSL.IMO2017A6.solution_of_map_zero_eq_one_imp_injective
Proof state before:
case g
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : good f
h1✝ : ¬f = 0
h1 : -f 0 = 1
h2 : good (-f)
h3 : -f = fun x => 1 - x
⊢ (fun x => 1 - x) = -fun x => x - 1
Tactic:
exact funext λ x ↦ (neg_sub x 1).symm
Proof state after:
no goals
Theorem: IMOSL.IMO2017A6.solution_of_map_zero_eq_one_imp_injective
Proof state before:
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
f : D → D
h0 : f = 0 ∨ (f = fun x => 1 - x) ∨ f = fun x => x - 1
⊢ good f
Tactic:
rcases h0 with rfl | rfl | rfl
Proof state after:
case inl
D : Type u_1
inst✝ : DivisionRing D
f : D → D
h✝ : good f
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
⊢ good 0

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

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

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

case inr.inr
D : Type u_1
inst✝ : DivisionRing D
f : D → D
h✝ : good f
h : ∀ (f : D → D), good f → f 0 = 1 → Function.Injective f
⊢ good fun x => x - 1
Tactic:
exacts [zero_is_good, one_sub_is_good, sub_one_is_good]
Proof state after:
no goals
Theorem: IMOSL.IMO2017A6.case1_injective
Proof state before:
D : Type u_1
inst✝ : DivisionRing D
f✝ : D → D
h✝ : good f✝
h : 2 ≠ 0
f : D → D
h0 : good f
h1 : f 0 = 1
⊢ Function.Injective f
Tactic:
have h2 := good_shift2 h0 h1
Proof state after:
D : Type u_1
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
⊢ Function.Injective f
Theorem: IMOSL.IMO2017A6.case1_injective
Proof state before:
D : Type u_1
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)
⊢ Function.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:
D : Type u_1
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
⊢ Function.Injective f
Theorem: IMOSL.IMO2017A6.case1_injective
Proof state before:
D : Type u_1
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
⊢ Function.Injective f
Tactic:
intros a b h4
Proof state after:
D : Type u_1
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: IMOSL.IMO2017A6.case1_injective
Proof state before:
D : Type u_1
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:
D : Type u_1
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: IMOSL.IMO2017A6.case1_injective
Proof state before:
D : Type u_1
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:
D : Type u_1
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: IMOSL.IMO2017A6.case1_injective
Proof state before:
D : Type u_1
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:
D : Type u_1
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: IMOSL.IMO2017A6.case1_injective
Proof state before:
D : Type u_1
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:
D : Type u_1
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: IMOSL.IMO2017A6.case1_injective
Proof state before:
D : Type u_1
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: IMOSL.IMO2017A6.case1_injective
Proof state before:
D : Type u_1
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:
D : Type u_1
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: IMOSL.IMO2017A6.case1_injective
Proof state before:
D : Type u_1
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
D : Type u_1
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
D : Type u_1
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: IMOSL.IMO2017A6.case1_injective
Proof state before:
case refine_1
D : Type u_1
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: IMOSL.IMO2017A6.case1_injective
Proof state before:
case refine_2
D : Type u_1
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: IMOSL.IMO2017A6.case1_injective
Proof state before:
D : Type u_1
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: IMOSL.IMO2017A6.case1_injective
Proof state before:
D : Type u_1
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: IMOSL.IMO2017A6.case1_injective
Proof state before:
D : Type u_1
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: IMOSL.IMO2017A6.case2_injective
Proof state before:
F : Type u_1
inst✝ : Field F
h : 2 = 0
f : F → F
h0 : good f
h1 : f 0 = 1
⊢ Function.Injective f
Tactic:
have h2 := good_shift h0 h1
Proof state after:
F : Type u_1
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
⊢ Function.Injective f
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
F : Type u_1
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
⊢ Function.Injective f
Tactic:
have h3 : ∀ c d : F, d ≠ 0 → f (c + 1) = f (d + 1) →
    f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1) := λ c d h3 h4 ↦ by
  rw [good_shift2 h0 h1, ← h0, h4, add_assoc, ← add_assoc (c + 1), h2,
    good_special_equality h0 (mul_inv_cancel h3), zero_add, add_right_comm]
Proof state after:
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
⊢ Function.Injective f
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
⊢ Function.Injective f
Tactic:
intros a b h4
Proof state after:
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f a = f b
⊢ a = b
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f a = f b
⊢ a = b
Tactic:
rw [← h2 a, ← h2 b, add_left_inj] at h4
Proof state after:
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
⊢ a = b
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
⊢ a = b
Tactic:
have h5 := good_map_add_one_eq_zero_iff h0 h1
Proof state after:
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
⊢ a = b
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
⊢ a = b
Tactic:
rcases eq_or_ne a 0 with rfl | ha
Proof state after:
case inl
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
b : F
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
h4 : f (0 + 1) = f (b + 1)
⊢ 0 = b

case inr
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
⊢ a = b
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
case inr
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
⊢ a = b
Tactic:
rcases eq_or_ne b 0 with rfl | hb
Proof state after:
case inr.inl
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a : F
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
h4 : f (a + 1) = f (0 + 1)
⊢ a = 0

case inr.inr
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
⊢ a = b
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
case inr.inr
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
⊢ a = b
Tactic:
have h6 : ((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1) =
  (a + b⁻¹) * (b + a⁻¹) + ((a + a⁻¹) * (b * b⁻¹) + (b + b⁻¹) * (a * a⁻¹))
    + a * a⁻¹ * (b * b⁻¹) := by ring
Proof state after:
case inr.inr
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 :
  ((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1) =
    (a + b⁻¹) * (b + a⁻¹) + ((a + a⁻¹) * (b * b⁻¹) + (b + b⁻¹) * (a * a⁻¹)) + a * a⁻¹ * (b * b⁻¹)
⊢ a = b
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
case inr.inr
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 :
  ((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1) =
    (a + b⁻¹) * (b + a⁻¹) + ((a + a⁻¹) * (b * b⁻¹) + (b + b⁻¹) * (a * a⁻¹)) + a * a⁻¹ * (b * b⁻¹)
⊢ a = b
Tactic:
have h7 : ∀ c d : F, (c + 1) * (d + 1) = c * d + c + d + 1 := λ c d ↦ by
  rw [add_one_mul (α := F), mul_add_one (α := F), ← add_assoc]
Proof state after:
case inr.inr
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 :
  ((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1) =
    (a + b⁻¹) * (b + a⁻¹) + ((a + a⁻¹) * (b * b⁻¹) + (b + b⁻¹) * (a * a⁻¹)) + a * a⁻¹ * (b * b⁻¹)
h7 : ∀ (c d : F), (c + 1) * (d + 1) = c * d + c + d + 1
⊢ a = b
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
case inr.inr
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 :
  ((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1) =
    (a + b⁻¹) * (b + a⁻¹) + ((a + a⁻¹) * (b * b⁻¹) + (b + b⁻¹) * (a * a⁻¹)) + a * a⁻¹ * (b * b⁻¹)
h7 : ∀ (c d : F), (c + 1) * (d + 1) = c * d + c + d + 1
⊢ a = b
Tactic:
rw [mul_inv_cancel ha, mul_inv_cancel hb, mul_one, mul_one, mul_one,
  add_comm b b⁻¹, add_add_add_comm, add_comm a⁻¹ b, ← add_assoc, ← h7] at h6
Proof state after:
case inr.inr
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 : ((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1) = (a + b⁻¹ + 1) * (b + a⁻¹ + 1)
h7 : ∀ (c d : F), (c + 1) * (d + 1) = c * d + c + d + 1
⊢ a = b
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
case inr.inr
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 : ((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1) = (a + b⁻¹ + 1) * (b + a⁻¹ + 1)
h7 : ∀ (c d : F), (c + 1) * (d + 1) = c * d + c + d + 1
⊢ a = b
Tactic:
replace h6 := congr_arg f h6
Proof state after:
case inr.inr
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h7 : ∀ (c d : F), (c + 1) * (d + 1) = c * d + c + d + 1
h6 : f (((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1)) = f ((a + b⁻¹ + 1) * (b + a⁻¹ + 1))
⊢ a = b
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
case inr.inr
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h7 : ∀ (c d : F), (c + 1) * (d + 1) = c * d + c + d + 1
h6 : f (((a + 1) * (b⁻¹ + 1) - 1) * ((b + 1) * (a⁻¹ + 1) - 1)) = f ((a + b⁻¹ + 1) * (b + a⁻¹ + 1))
⊢ a = b
Tactic:
rw [← h0, h3 a b hb h4, h3 b a ha h4.symm, h7, add_sub_cancel_right,
  h7, add_sub_cancel_right, ← h0 (a + b⁻¹ + 1), add_right_inj] at h6
Proof state after:
case inr.inr
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h7 : ∀ (c d : F), (c + 1) * (d + 1) = c * d + c + d + 1
h6 : f (a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹)) = f (a + b⁻¹ + 1 + (b + a⁻¹ + 1))
⊢ a = b
Theorem: IMOSL.IMO2017A6.case2_injective
Proof state before:
case inr.inr
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h7 : ∀ (c d : F), (c + 1) * (d + 1) = c * d + c + d + 1
h6 : f (a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹)) = f (a + b⁻¹ + 1 + (b + a⁻¹ + 1))
⊢ a = b
Tactic:
replace h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) =
  a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + (a * a⁻¹ + b * b⁻¹ + 1) := by ring
Proof state after:
case inr.inr
F : Type u_1
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
h3 : ∀ (c d : F), d ≠ 0 → f (c + 1) = f (d + 1) → f ((c + 1) * (d⁻¹ + 1) - 1) = f (c + d⁻¹ + 1)
a b : F
h4 : f (a + 1) = f (b + 1)
h5 : ∀ (x : F), f (x + 1) = 0 ↔ x = 0
ha : a ≠ 0
hb : b ≠ 0
h6 : f (a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹)) = f (a + b⁻¹ + 1 + (b + a⁻¹ + 1))
h7 : (a + b + 1) * (b⁻¹ + a⁻¹ + 1) = a * b⁻¹ + a + b⁻¹ + (b * a⁻¹ + b + a⁻¹) + (a * a⁻¹ + b * b⁻¹ + 1)
⊢ a = b