Theorem: IMOSL.IMO2012A5.Case1.Subcase11_solution (IMOSLLean4/IMO2012/A5/A5Cases/Case1.lean)

State before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
h0 : f (-1) = -2
x : R
⊢ f (x + 1) = f x + 1
Tactic:
rcases Eq5 hf h x with h2 | h2
State after:
case inl
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
h0 : f (-1) = -2
x : R
h2 : f (x + 1) = 0
⊢ f (x + 1) = f x + 1

case inr
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
h0 : f (-1) = -2
x : R
h2 : f x + f (-x) = f (-1)
⊢ f (x + 1) = f x + 1

State before:
case inl
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
h0 : f (-1) = -2
x : R
h2 : f (x + 1) = 0
⊢ f (x + 1) = f x + 1
Tactic:
rw [Eq6 hf h h2, h2, neg_add_self]
State after:
no goals

State before:
case inr
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
h0 : f (-1) = -2
x : R
h2 : f x + f (-x) = f (-1)
⊢ f (x + 1) = f x + 1
Tactic:
rw [Eq1 hf, h0, add_left_comm, ← mul_two, mul_neg, ← neg_mul, ← add_mul,
  eq_neg_iff_add_eq_zero, ← add_one_mul _ (2 : S), mul_eq_zero, add_assoc] at h2
State after:
case inr
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
h0 : f (-1) = -2
x : R
h2 : -f (x + 1) + (f x + 1) = 0 ∨ 2 = 0
⊢ f (x + 1) = f x + 1

State before:
case inr
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
hf : NontrivialGood f
h : f (-1) ≠ 0
h0 : f (-1) = -2
x : R
h2 : -f (x + 1) + (f x + 1) = 0 ∨ 2 = 0
⊢ f (x + 1) = f x + 1
Tactic:
exact neg_add_eq_zero.mp (h2.resolve_right (neg_ne_zero.mp (h0.symm.trans_ne h)))
State after:
no goals