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

State before:
R : Type u_2
S✝ : Type ?u.184718
inst✝⁴ : Ring R
inst✝³ : Ring S✝
inst✝² : NoZeroDivisors S✝
g✝ : R → S✝
hg✝ : ShiftGood23 g✝
S : Type u_1
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
x : R
⊢ (g (x + 1) - g (x - 1)) ^ 2 = 2 ^ 4 * g x
Tactic:
rw [sub_sq', ← sub_eq_of_eq_add (add_sq' (g _) _),
  Eq1 hg, mul_assoc, Eq3_1 hg]
State after:
R : Type u_2
S✝ : Type ?u.184718
inst✝⁴ : Ring R
inst✝³ : Ring S✝
inst✝² : NoZeroDivisors S✝
g✝ : R → S✝
hg✝ : ShiftGood23 g✝
S : Type u_1
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
x : R
⊢ (2 * (g x + 1)) ^ 2 - 2 * (g x - 1) ^ 2 - 2 * (g x - 1) ^ 2 = 2 ^ 4 * g x

State before:
R : Type u_2
S✝ : Type ?u.184718
inst✝⁴ : Ring R
inst✝³ : Ring S✝
inst✝² : NoZeroDivisors S✝
g✝ : R → S✝
hg✝ : ShiftGood23 g✝
S : Type u_1
inst✝¹ : CommRing S
inst✝ : NoZeroDivisors S
g : R → S
hg : ShiftGood23 g
x : R
⊢ (2 * (g x + 1)) ^ 2 - 2 * (g x - 1) ^ 2 - 2 * (g x - 1) ^ 2 = 2 ^ 4 * g x
Tactic:
ring
State after:
no goals