Theorem: IMOSL.IMO2012A5.Case1.map_neg_one_cases (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
⊢ f (-1) = -2 ∨ f (-1) = 1
Tactic:
rw [← sub_eq_zero (b := 1), eq_neg_iff_add_eq_zero, ← mul_eq_zero,
  mul_sub_one, add_mul, two_mul, add_sub_assoc, 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
⊢ f (-1) * f (-1) + (f (-1) - 2) = 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
⊢ f (-1) * f (-1) + (f (-1) - 2) = 0
Tactic:
have h0 := Eq5 hf h (-1 + -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
h0 : f (-1 + -1 + 1) = 0 ∨ f (-1 + -1) + f (-(-1 + -1)) = f (-1)
⊢ f (-1) * f (-1) + (f (-1) - 2) = 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
h0 : f (-1 + -1 + 1) = 0 ∨ f (-1 + -1) + f (-(-1 + -1)) = f (-1)
⊢ f (-1) * f (-1) + (f (-1) - 2) = 0
Tactic:
rw [neg_add_cancel_right, or_iff_right h, ← eq_sub_iff_add_eq] at h0
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
h0 : f (-1 + -1) = f (-1) - f (-(-1 + -1))
⊢ f (-1) * f (-1) + (f (-1) - 2) = 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
h0 : f (-1 + -1) = f (-1) - f (-(-1 + -1))
⊢ f (-1) * f (-1) + (f (-1) - 2) = 0
Tactic:
have h1 := hf.is_good (-1) (-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
h0 : f (-1 + -1) = f (-1) - f (-(-1 + -1))
h1 : f (-1 * -1 + 1) = f (-1) * f (-1) + f (-1 + -1)
⊢ f (-1) * f (-1) + (f (-1) - 2) = 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
h0 : f (-1 + -1) = f (-1) - f (-(-1 + -1))
h1 : f (-1 * -1 + 1) = f (-1) * f (-1) + f (-1 + -1)
⊢ f (-1) * f (-1) + (f (-1) - 2) = 0
Tactic:
rwa [h0, neg_mul_neg, one_mul, ← neg_add, neg_neg, one_add_one_eq_two, map_two hf h,
  eq_comm, ← sub_eq_zero, add_sub_assoc, sub_sub, one_add_one_eq_two] at h1
State after:
no goals