[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue ℤ S
x : ℤˣ
⊢ ↑abv ↑x = 1
[PROOFSTEP]
rcases Int.units_eq_one_or x with (rfl | rfl)
[GOAL]
case inl
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue ℤ S
⊢ ↑abv ↑1 = 1
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue ℤ S
⊢ ↑abv ↑(-1) = 1
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
rcases Int.units_eq_one_or x with (rfl | rfl)
[GOAL]
case inl
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommRing S
inst✝ : Nontrivial R
abv : AbsoluteValue R S
⊢ ↑abv ↑↑1 = 1
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u_1
S : Type u_2
inst✝² : Ring R
inst✝¹ : LinearOrderedCommRing S
inst✝ : Nontrivial R
abv : AbsoluteValue R S
⊢ ↑abv ↑↑(-1) = 1
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue R S
x : ℤˣ
y : R
⊢ ↑abv (x • y) = ↑abv y
[PROOFSTEP]
rcases Int.units_eq_one_or x with (rfl | rfl)
[GOAL]
case inl
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue R S
y : R
⊢ ↑abv (1 • y) = ↑abv y
[PROOFSTEP]
simp
[GOAL]
case inr
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : LinearOrderedCommRing S
abv : AbsoluteValue R S
y : R
⊢ ↑abv (-1 • y) = ↑abv y
[PROOFSTEP]
simp
