Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.Eq1 (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 : R
⊢ g (x + 1) + g (x - 1) = 2 * (g x + 1)
Tactic:
have h := hg.shift_good.Eq6 x
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 : R
h : (g - 1) (x + 1) + (g - 1) (x - 1) = ((g - 1) x + 1) * ((g - 1) 2 - 1)
⊢ g (x + 1) + g (x - 1) = 2 * (g x + 1)

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 : R
h : (g - 1) (x + 1) + (g - 1) (x - 1) = ((g - 1) x + 1) * ((g - 1) 2 - 1)
⊢ g (x + 1) + g (x - 1) = 2 * (g x + 1)
Tactic:
simp only [Pi.sub_apply, Pi.one_apply] 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 : R
h : g (x + 1) - 1 + (g (x - 1) - 1) = (g x - 1 + 1) * (g 2 - 1 - 1)
⊢ g (x + 1) + g (x - 1) = 2 * (g x + 1)

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 : R
h : g (x + 1) - 1 + (g (x - 1) - 1) = (g x - 1 + 1) * (g 2 - 1 - 1)
⊢ g (x + 1) + g (x - 1) = 2 * (g x + 1)
Tactic:
rwa [sub_add_cancel, hg.map_two, sub_eq_of_eq_add three_add_one_eq_four.symm,
  sub_eq_of_eq_add two_add_one_eq_three.symm, sub_add_sub_comm, mul_two,
  sub_eq_iff_eq_add, one_add_one_eq_two, ← two_mul, ← mul_add_one (α := S)] at h
State after:
no goals