Theorem: IMOSL.IMO2012A5.Case2.ShiftGood23.Eq3_1 (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
⊢ g (x + 1) * g (x - 1) = (g x - 1) ^ 2
Tactic:
have h : (g - 1) 2 ≠ 1 := λ h0 ↦ by
  rw [Pi.sub_apply, hg.map_two, sub_eq_of_eq_add three_add_one_eq_four.symm,
    ← two_add_one_eq_three, add_left_eq_self] at h0
  exact hg.Schar_ne_two h0
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 - 1) 2 ≠ 1
⊢ g (x + 1) * g (x - 1) = (g x - 1) ^ 2

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) 2 ≠ 1
⊢ g (x + 1) * g (x - 1) = (g x - 1) ^ 2
Tactic:
replace h := hg.shift_good.Eq7 h x
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 - 1) (x + 1) + 1) * ((g - 1) (x - 1) + 1) = (g - 1) x ^ 2
⊢ g (x + 1) * g (x - 1) = (g x - 1) ^ 2

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 + 1) + 1) * ((g - 1) (x - 1) + 1) = (g - 1) x ^ 2
⊢ g (x + 1) * g (x - 1) = (g x - 1) ^ 2
Tactic:
simp only [Pi.sub_apply, Pi.one_apply, sub_add_cancel] 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 + 1) * g (x - 1) = (g x - 1) ^ 2
⊢ g (x + 1) * g (x - 1) = (g x - 1) ^ 2

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 + 1) * g (x - 1) = (g x - 1) ^ 2
⊢ g (x + 1) * g (x - 1) = (g x - 1) ^ 2
Tactic:
exact h
State after:
no goals

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
h0 : (g - 1) 2 = 1
⊢ False
Tactic:
rw [Pi.sub_apply, hg.map_two, sub_eq_of_eq_add three_add_one_eq_four.symm,
  ← two_add_one_eq_three, add_left_eq_self] at h0
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
h0 : 2 = 0
⊢ False

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
h0 : 2 = 0
⊢ False
Tactic:
exact hg.Schar_ne_two h0
State after:
no goals