no goals
F : Type ?u.77751
α : Type ?u.77754
β : Type ?u.77757
R : Type u_2
S : Type u_1
S' : Type ?u.77766
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R ≃+* S
x✝ y x : R
⊢ ↑f x = -1 ↔ x = -1
rw [← neg_eq_iff_eq_neg, ← neg_eq_iff_eq_neg, ← map_neg, RingEquiv.map_eq_one_iff]