Theorem: IMOSL.IMO2012A5.Case1.Eq5 (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 + 1) = 0 ∨ f x + f (-x) = f (-1)
Tactic:
have h0 : f x * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x)) := by
  have h0 : x * -x = -x * x := by rw [mul_neg, neg_mul]
  rw [sub_mul, mul_add, mul_add, map_commute_of_commute hf.is_good h0,
    add_comm, add_sub_add_left_eq_sub]
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 * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
⊢ f (x + 1) = 0 ∨ f x + f (-x) = f (-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 * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
⊢ f (x + 1) = 0 ∨ f x + f (-x) = f (-1)
Tactic:
have h1 := Eq3 hf x 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 * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
h1 : f (-x) * f (-x) + f (-(x + x)) = f x * f x + f (x + x)
⊢ f (x + 1) = 0 ∨ f x + f (-x) = f (-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 * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
h1 : f (-x) * f (-x) + f (-(x + x)) = f x * f x + f (x + x)
⊢ f (x + 1) = 0 ∨ f x + f (-x) = f (-1)
Tactic:
rw [add_comm, ← sub_eq_sub_iff_add_eq_add, h0, Eq1 hf, add_sub_cancel_right,
  ← two_mul, Eq4 hf h, ← sub_eq_zero, ← mul_sub, mul_eq_zero] 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 * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
h1 : f x - f (-x) = 0 ∨ f (-1) - (f x + f (-x)) = 0
⊢ f (x + 1) = 0 ∨ f x + f (-x) = f (-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 * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
h1 : f x - f (-x) = 0 ∨ f (-1) - (f x + f (-x)) = 0
⊢ f (x + 1) = 0 ∨ f x + f (-x) = f (-1)
Tactic:
refine h1.imp (λ h1 ↦ ?_) (λ h1 ↦ (eq_of_sub_eq_zero h1).symm)
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 * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
h1✝ : f x - f (-x) = 0 ∨ f (-1) - (f x + f (-x)) = 0
h1 : f x - f (-x) = 0
⊢ f (x + 1) = 0

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 * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
h1✝ : f x - f (-x) = 0 ∨ f (-1) - (f x + f (-x)) = 0
h1 : f x - f (-x) = 0
⊢ f (x + 1) = 0
Tactic:
rw [Eq1 hf, sub_add_cancel_right, neg_eq_zero, mul_eq_zero] 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 * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
h1✝ : f x - f (-x) = 0 ∨ f (-1) - (f x + f (-x)) = 0
h1 : f (x + 1) = 0 ∨ f (-1) = 0
⊢ f (x + 1) = 0

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

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 - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
Tactic:
have h0 : x * -x = -x * x := by rw [mul_neg, neg_mul]
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 : x * -x = -x * x
⊢ f x * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))

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 : x * -x = -x * x
⊢ f x * f x - f (-x) * f (-x) = (f x - f (-x)) * (f x + f (-x))
Tactic:
rw [sub_mul, mul_add, mul_add, map_commute_of_commute hf.is_good h0,
  add_comm, add_sub_add_left_eq_sub]
State after:
no goals

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
⊢ x * -x = -x * x
Tactic:
rw [mul_neg, neg_mul]
State after:
no goals