Theorem: IMOSL.IMO2012A5.Case1.Eq2 (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
x : R
⊢ f (-x) = -f (x + 2)
Tactic:
replace hf := Eq1 hf
State after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
h : f (-1) ≠ 0
x : R
hf : ∀ (x : R), f (-x) = f (x + 1) * f (-1) + f x
⊢ f (-x) = -f (x + 2)

State before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
h : f (-1) ≠ 0
x : R
hf : ∀ (x : R), f (-x) = f (x + 1) * f (-1) + f x
⊢ f (-x) = -f (x + 2)
Tactic:
have h0 := hf (-(x + 1))
State after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
h : f (-1) ≠ 0
x : R
hf : ∀ (x : R), f (-x) = f (x + 1) * f (-1) + f x
h0 : f (- -(x + 1)) = f (-(x + 1) + 1) * f (-1) + f (-(x + 1))
⊢ f (-x) = -f (x + 2)

State before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
h : f (-1) ≠ 0
x : R
hf : ∀ (x : R), f (-x) = f (x + 1) * f (-1) + f x
h0 : f (- -(x + 1)) = f (-(x + 1) + 1) * f (-1) + f (-(x + 1))
⊢ f (-x) = -f (x + 2)
Tactic:
rw [neg_neg, hf (x + 1), neg_add, neg_add_cancel_right, ← add_assoc, self_eq_add_left,
  ← add_mul, mul_eq_zero, or_iff_left h, add_assoc, one_add_one_eq_two] at h0
State after:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
h : f (-1) ≠ 0
x : R
hf : ∀ (x : R), f (-x) = f (x + 1) * f (-1) + f x
h0 : f (-x) + f (x + 2) = 0
⊢ f (-x) = -f (x + 2)

State before:
R : Type u_2
S : Type u_1
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NoZeroDivisors S
f : R → S
h : f (-1) ≠ 0
x : R
hf : ∀ (x : R), f (-x) = f (x + 1) * f (-1) + f x
h0 : f (-x) + f (x + 2) = 0
⊢ f (-x) = -f (x + 2)
Tactic:
exact eq_neg_of_add_eq_zero_left h0
State after:
no goals