case inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedCommGroup α
n : ℤ
a b : α
hn : n ≠ 0
h : 0 < n
⊢ Function.Injective fun x => x ^ n

case inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedCommGroup α
n : ℤ
a b : α
hn : n ≠ 0
h : n < 0
⊢ Function.Injective fun x => x ^ n
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedCommGroup α
n : ℤ
a b : α
hn : n ≠ 0
⊢ Function.Injective fun x => x ^ n
rcases hn.symm.lt_or_lt with (h | h)
no goals
case inl
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedCommGroup α
n : ℤ
a b : α
hn : n ≠ 0
h : 0 < n
⊢ Function.Injective fun x => x ^ n
exact (zpow_strictMono_left α h).injective
case inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedCommGroup α
n : ℤ
a✝ b✝ : α
hn : n ≠ 0
h : n < 0
a b : α
hab : a ^ n = b ^ n
⊢ a ^ (-n) = b ^ (-n)
case inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedCommGroup α
n : ℤ
a b : α
hn : n ≠ 0
h : n < 0
⊢ Function.Injective fun x => x ^ n
refine' fun a b (hab : a ^ n = b ^ n) => (zpow_strictMono_left α (neg_pos.mpr h)).injective _
no goals
case inr
α : Type u_1
M : Type u
N : Type v
G : Type w
H : Type x
A : Type y
B : Type z
R : Type u₁
S : Type u₂
inst✝ : LinearOrderedCommGroup α
n : ℤ
a✝ b✝ : α
hn : n ≠ 0
h : n < 0
a b : α
hab : a ^ n = b ^ n
⊢ a ^ (-n) = b ^ (-n)
rw [zpow_neg, zpow_neg, hab]