no goals
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommRing S
inst✝ : Nontrivial R
abv : AbsoluteValue R S
x : ℤˣ
⊢ ↑abv ↑↑x = 1
rcases Int.units_eq_one_or x with (rfl | rfl) <;> simp