Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.Eq5 (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
h :
  (g - 1) (x * 2 + 1) + (g - 1) (x * 2 - 1) =
    (g - 1) (x + 1) * (g - 1) 2 + (g - 1) (x - 1) + ((g - 1) (x - 1) * (g - 1) 2 + (g - 1) (x + 1))
⊢ g (x * 2) = g x * 4
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 * 2 + 1) - 1 + (g (x * 2 - 1) - 1) =
    (g (x + 1) - 1) * (g 2 - 1) + (g (x - 1) - 1) + ((g (x - 1) - 1) * (g 2 - 1) + (g (x + 1) - 1))
⊢ g (x * 2) = g x * 4

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 * 2 + 1) - 1 + (g (x * 2 - 1) - 1) =
    (g (x + 1) - 1) * (g 2 - 1) + (g (x - 1) - 1) + ((g (x - 1) - 1) * (g 2 - 1) + (g (x + 1) - 1))
⊢ g (x * 2) = g x * 4
Tactic:
rw [← add_sub_add_comm, Eq1 hg, add_add_add_comm, ← add_mul,
  add_comm (g (x - 1) - 1), mul_sub_one, sub_add_cancel, ← add_sub_add_comm,
  Eq1 hg, one_add_one_eq_two, mul_add_one (α := S), add_sub_cancel_right,
  mul_add_one (α := S), add_sub_cancel_right, hg.map_two, mul_assoc,
  ← sub_eq_zero, ← mul_sub, mul_eq_zero] 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 : 2 = 0 ∨ g (x * 2) - g x * 4 = 0
⊢ g (x * 2) = g x * 4

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 : 2 = 0 ∨ g (x * 2) - g x * 4 = 0
⊢ g (x * 2) = g x * 4
Tactic:
exact eq_of_sub_eq_zero (h.resolve_left hg.Schar_ne_two)
State after:
no goals