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

State before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
g : R → S
hg : ShiftGood23 g
x y : R
⊢ g (x * y - 1) = (g x - 1) * (g y - 1) + g (x - y)
Tactic:
have h := hg.is_good x (-y)
State after:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
g : R → S
hg : ShiftGood23 g
x y : R
h : g (x * -y + 1) = (g x - 1) * (g (-y) - 1) + g (x + -y)
⊢ g (x * y - 1) = (g x - 1) * (g y - 1) + g (x - y)

State before:
R : Type u_2
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
g : R → S
hg : ShiftGood23 g
x y : R
h : g (x * -y + 1) = (g x - 1) * (g (-y) - 1) + g (x + -y)
⊢ g (x * y - 1) = (g x - 1) * (g y - 1) + g (x - y)
Tactic:
rwa [hg.map_even, mul_neg, neg_add_eq_sub, ← neg_sub, hg.map_even, ← sub_eq_add_neg] at h
State after:
no goals