case intro
α : 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✝ : OrderedCommGroup α
m n✝ : ℤ
a b : α
ha : 1 < a
k : ℤ
hk : 0 < k
n : ℕ
hn : k = ↑n
⊢ 1 < a ^ k
α : 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✝ : OrderedCommGroup α
m n : ℤ
a b : α
ha : 1 < a
k : ℤ
hk : 0 < k
⊢ 1 < a ^ k
obtain ⟨n, hn⟩ := Int.eq_ofNat_of_zero_le hk.le
case intro
α : 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✝ : OrderedCommGroup α
m n✝ : ℤ
a b : α
ha : 1 < a
k : ℤ
hk : 0 < k
n : ℕ
hn : k = ↑n
⊢ 1 < a ^ n
case intro
α : 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✝ : OrderedCommGroup α
m n✝ : ℤ
a b : α
ha : 1 < a
k : ℤ
hk : 0 < k
n : ℕ
hn : k = ↑n
⊢ 1 < a ^ k
rw [hn, zpow_ofNat]
case intro
α : 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✝ : OrderedCommGroup α
m n✝ : ℤ
a b : α
ha : 1 < a
k : ℤ
hk : 0 < k
n : ℕ
hn : k = ↑n
⊢ 0 < ↑n
case intro
α : 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✝ : OrderedCommGroup α
m n✝ : ℤ
a b : α
ha : 1 < a
k : ℤ
hk : 0 < k
n : ℕ
hn : k = ↑n
⊢ 1 < a ^ n
refine' one_lt_pow' ha (coe_nat_pos.mp _).ne'
no goals
case intro
α : 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✝ : OrderedCommGroup α
m n✝ : ℤ
a b : α
ha : 1 < a
k : ℤ
hk : 0 < k
n : ℕ
hn : k = ↑n
⊢ 0 < ↑n
rwa [← hn]