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

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
x y : R
h : g (x * y + 1) + g (x * y - 1) = (g x - 1) * (g y - 1) + g (x + y) + ((g x - 1) * (g y - 1) + g (x - y))
⊢ 2 * (g (x * y) - g x * g y) = g (x + y) + g (x - y) - 2 * (g x + g y)
Tactic:
rw [Eq1 hg, add_add_add_comm, ← two_mul, ← sub_eq_iff_eq_add', ← mul_sub] at h
State after:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
x y : R
h : 2 * (g (x * y) + 1 - (g x - 1) * (g y - 1)) = g (x + y) + g (x - y)
⊢ 2 * (g (x * y) - g x * g y) = g (x + y) + g (x - y) - 2 * (g x + g y)

State before:
R : Type u_2
S : Type u_1
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
x y : R
h : 2 * (g (x * y) + 1 - (g x - 1) * (g y - 1)) = g (x + y) + g (x - y)
⊢ 2 * (g (x * y) - g x * g y) = g (x + y) + g (x - y) - 2 * (g x + g y)
Tactic:
rw [← h, ← mul_sub, sub_sub, sub_one_mul, mul_sub_one, sub_sub, sub_add,
  ← add_sub_assoc, sub_sub_cancel_left, sub_neg_eq_add, add_sub_add_right_eq_sub]
State after:
no goals