Theorem: IMOSL.IMO2017A6.case1_injective (IMOSLLean4/IMO2017/A6/A6.lean)

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
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

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
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

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
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

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 _ ?_)
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))

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]
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))

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]
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))

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)
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))

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
State after:
no goals

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)]
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)

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₂ _ ?_ ?_
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)

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]
State after:
no goals

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]
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals