Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.is_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.shift_good.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 - 1) (x * y + 1) = (g - 1) x * (g - 1) y + (g - 1) (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 - 1) (x * y + 1) = (g - 1) x * (g - 1) y + (g - 1) (x + y)
⊢ g (x * y + 1) = (g x - 1) * (g y - 1) + g (x + y)
Tactic:
simp only [Pi.sub_apply, Pi.one_apply] at h
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) - 1 = (g x - 1) * (g y - 1) + (g (x + y) - 1)
⊢ 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) - 1 = (g x - 1) * (g y - 1) + (g (x + y) - 1)
⊢ g (x * y + 1) = (g x - 1) * (g y - 1) + g (x + y)
Tactic:
rwa [← add_sub_assoc, sub_left_inj] at h
State after:
no goals