case inl
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝ : LinearOrderedRing G
h : abs x ≠ 1
⊢ orderOf x ≤ 2

case inr
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝ : LinearOrderedRing G
h : abs x = 1
⊢ orderOf x ≤ 2
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝ : LinearOrderedRing G
⊢ orderOf x ≤ 2
cases' ne_or_eq (|x|) 1 with h h
case inr.inl
G : Type u
A : Type v
y : G
a b : A
n m : ℕ
inst✝ : LinearOrderedRing G
h : abs 1 = 1
⊢ orderOf 1 ≤ 2

case inr.inr
G : Type u
A : Type v
y : G
a b : A
n m : ℕ
inst✝ : LinearOrderedRing G
h : abs (-1) = 1
⊢ orderOf (-1) ≤ 2
case inr
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝ : LinearOrderedRing G
h : abs x = 1
⊢ orderOf x ≤ 2
rcases eq_or_eq_neg_of_abs_eq h with (rfl | rfl)
no goals
case inr.inr
G : Type u
A : Type v
y : G
a b : A
n m : ℕ
inst✝ : LinearOrderedRing G
h : abs (-1) = 1
⊢ orderOf (-1) ≤ 2
apply orderOf_le_of_pow_eq_one <;> norm_num
no goals
case inl
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝ : LinearOrderedRing G
h : abs x ≠ 1
⊢ orderOf x ≤ 2
simp [orderOf_abs_ne_one h]
no goals
case inr.inl
G : Type u
A : Type v
y : G
a b : A
n m : ℕ
inst✝ : LinearOrderedRing G
h : abs 1 = 1
⊢ orderOf 1 ≤ 2
simp