case h.e'_1.h.e'_2
β : Type ?u.248186
A : Type ?u.248189
G : Type ?u.248192
M : Type ?u.248195
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
n : ℕ
h : 0 < n
⊢ abs (a ^ n) = abs a ^ n

case h.e'_1.h.e'_3
β : Type ?u.248186
A : Type ?u.248189
G : Type ?u.248192
M : Type ?u.248195
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
n : ℕ
h : 0 < n
⊢ 1 = 1 ^ n
β : Type ?u.248186
A : Type ?u.248189
G : Type ?u.248192
M : Type ?u.248195
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
n : ℕ
h : 0 < n
⊢ abs (a ^ n) = 1 ↔ abs a = 1
convert pow_left_inj (abs_nonneg a) zero_le_one h
no goals
case h.e'_1.h.e'_2
β : Type ?u.248186
A : Type ?u.248189
G : Type ?u.248192
M : Type ?u.248195
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
n : ℕ
h : 0 < n
⊢ abs (a ^ n) = abs a ^ n

case h.e'_1.h.e'_3
β : Type ?u.248186
A : Type ?u.248189
G : Type ?u.248192
M : Type ?u.248195
R : Type u_1
inst✝ : LinearOrderedRing R
a : R
n : ℕ
h : 0 < n
⊢ 1 = 1 ^ n
exacts [(pow_abs _ _).symm, (one_pow _).symm]