Theorem: IMOSL.IMO2012A5.Case2.Eq5 (IMOSLLean4/IMO2012/A5/A5Cases/Case2.lean)

State before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
h0 : f x = 0
h1 : f (x + 1) = 0
this : ∀ (y : R), f (x + y + 1) = f (x - y)
y : R
⊢ f (y + (2 * x + 1)) = f y
Tactic:
rw [two_mul, ← add_assoc, add_left_comm, this, sub_add_cancel_right, h]
State after:
no goals

State before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
h0 : f x = 0
h1 : f (x + 1) = 0
y : R
⊢ f (x + y + 1) = f (x - y)
Tactic:
have h2 : f (x * ((x + 1) * y) + 1) = f ((x + 1) * (x * y) + 1) := by
  rw [add_one_mul x, mul_add, add_one_mul x]
State after:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
h0 : f x = 0
h1 : f (x + 1) = 0
y : R
h2 : f (x * ((x + 1) * y) + 1) = f ((x + 1) * (x * y) + 1)
⊢ f (x + y + 1) = f (x - y)

State before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
h0 : f x = 0
h1 : f (x + 1) = 0
y : R
h2 : f (x * ((x + 1) * y) + 1) = f ((x + 1) * (x * y) + 1)
⊢ f (x + y + 1) = f (x - y)
Tactic:
have h3 : x + (x + 1) * y = (x + 1) * (y + 1) - 1 := by
  rw [mul_add_one _ y, add_sub_assoc, add_sub_cancel_right, add_comm]
State after:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
h0 : f x = 0
h1 : f (x + 1) = 0
y : R
h2 : f (x * ((x + 1) * y) + 1) = f ((x + 1) * (x * y) + 1)
h3 : x + (x + 1) * y = (x + 1) * (y + 1) - 1
⊢ f (x + y + 1) = f (x - y)

State before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
h0 : f x = 0
h1 : f (x + 1) = 0
y : R
h2 : f (x * ((x + 1) * y) + 1) = f ((x + 1) * (x * y) + 1)
h3 : x + (x + 1) * y = (x + 1) * (y + 1) - 1
⊢ f (x + y + 1) = f (x - y)
Tactic:
rwa [hf.is_good, h3, Eq1 hf h, hf.is_good, ← add_rotate, ← mul_add_one x,
  hf.is_good, h0, h1, zero_mul, zero_add, zero_mul, zero_add, zero_add,
  zero_mul, zero_add, add_sub_add_right_eq_sub, ← add_assoc, eq_comm] at h2
State after:
no goals

State before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
h0 : f x = 0
h1 : f (x + 1) = 0
y : R
⊢ f (x * ((x + 1) * y) + 1) = f ((x + 1) * (x * y) + 1)
Tactic:
rw [add_one_mul x, mul_add, add_one_mul x]
State after:
no goals

State before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocSemiring S
f : R → S
hf : NontrivialGood f
h : ∀ (x : R), f (-x) = f x
x : R
h0 : f x = 0
h1 : f (x + 1) = 0
y : R
h2 : f (x * ((x + 1) * y) + 1) = f ((x + 1) * (x * y) + 1)
⊢ x + (x + 1) * y = (x + 1) * (y + 1) - 1
Tactic:
rw [mul_add_one _ y, add_sub_assoc, add_sub_cancel_right, add_comm]
State after:
no goals