Theorem: IMOSL.IMO2012A5.Case1.Eq6 (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
h0 : f (x + 1) = 0
⊢ f x = -1
Tactic:
have h1 := Eq1 hf x
State after:
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
h0 : f (x + 1) = 0
h1 : f (-x) = f (x + 1) * f (-1) + f x
⊢ f x = -1

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
h0 : f (x + 1) = 0
h1 : f (-x) = f (x + 1) * f (-1) + f x
⊢ f x = -1
Tactic:
rw [h0, zero_mul, zero_add] at h1
State after:
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
h0 : f (x + 1) = 0
h1 : f (-x) = f x
⊢ f x = -1

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
h0 : f (x + 1) = 0
h1 : f (-x) = f x
⊢ f x = -1
Tactic:
have h2 := Eq3 hf x (-(x + 1))
State after:
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
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h2 : f (-x) * f (- -(x + 1)) + f (-(x + -(x + 1))) = f x * f (-(x + 1)) + f (x + -(x + 1))
⊢ f x = -1

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
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h2 : f (-x) * f (- -(x + 1)) + f (-(x + -(x + 1))) = f x * f (-(x + 1)) + f (x + -(x + 1))
⊢ f x = -1
Tactic:
rw [neg_neg, h0, mul_zero, zero_add, ← sub_eq_add_neg,
  sub_add_cancel_left, neg_neg, hf.map_one] at h2
State after:
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
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h2 : 0 = f x * f (-(x + 1)) + f (-1)
⊢ f x = -1

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
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h2 : 0 = f x * f (-(x + 1)) + f (-1)
⊢ f x = -1
Tactic:
have h3 := Eq3 hf x (x + 1)
State after:
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
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h2 : 0 = f x * f (-(x + 1)) + f (-1)
h3 : f (-x) * f (-(x + 1)) + f (-(x + (x + 1))) = f x * f (x + 1) + f (x + (x + 1))
⊢ f x = -1

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
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h2 : 0 = f x * f (-(x + 1)) + f (-1)
h3 : f (-x) * f (-(x + 1)) + f (-(x + (x + 1))) = f x * f (x + 1) + f (x + (x + 1))
⊢ f x = -1
Tactic:
rw [h0, mul_zero, zero_add, ← add_assoc, ← two_mul,
  Eq4 hf h, h1, sub_self, h2, add_right_inj] at h3
State after:
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
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h2 : 0 = f x * f (-(x + 1)) + f (-1)
h3 : f (-(2 * x + 1)) = f (-1)
⊢ f x = -1

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
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h2 : 0 = f x * f (-(x + 1)) + f (-1)
h3 : f (-(2 * x + 1)) = f (-1)
⊢ f x = -1
Tactic:
replace h2 := Eq4 hf h (-x - 1)
State after:
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
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h3 : f (-(2 * x + 1)) = f (-1)
h2 : f (2 * (-x - 1) + 1) = f (-x - 1) - f (-(-x - 1))
⊢ f x = -1

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
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h3 : f (-(2 * x + 1)) = f (-1)
h2 : f (2 * (-x - 1) + 1) = f (-x - 1) - f (-(-x - 1))
⊢ f x = -1
Tactic:
rw [two_mul, add_assoc, sub_add_cancel, ← add_sub_right_comm, ← two_mul, mul_neg,
  ← neg_add', h3, eq_comm, Eq1 hf, sub_add_cancel_right, sub_add_cancel,
  neg_eq_iff_add_eq_zero, h1, ← add_one_mul (f x), mul_eq_zero] at h2
State after:
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
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h3 : f (-(2 * x + 1)) = f (-1)
h2 : f x + 1 = 0 ∨ f (-1) = 0
⊢ f x = -1

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
h0 : f (x + 1) = 0
h1 : f (-x) = f x
h3 : f (-(2 * x + 1)) = f (-1)
h2 : f x + 1 = 0 ∨ f (-1) = 0
⊢ f x = -1
Tactic:
exact eq_neg_of_add_eq_zero_left (h2.resolve_right h)
State after:
no goals