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

State before:
R : Type ?u.155749
S : Type u_1
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
g : R → S
hg : ShiftGood23 g
h : 2 = 0
⊢ (g - 1) 2 = -1
Tactic:
rw [Pi.sub_apply, Pi.one_apply, sub_eq_neg_self, hg.map_two, ← three_add_one_eq_four,
  ← two_add_one_eq_three, h, zero_add, one_add_one_eq_two, h]
State after:
no goals