case Hxpos
α : Type u_2
β : Type u_1
γ : Type ?u.289026
ι : Type ?u.289029
inst✝¹ : NormedDivisionRing α
inst✝ : Monoid β
φ : β →* α
x : β
k : ℕ+
h : x ^ ↑k = 1
⊢ 0 ≤ ‖↑φ x‖

case Hypos
α : Type u_2
β : Type u_1
γ : Type ?u.289026
ι : Type ?u.289029
inst✝¹ : NormedDivisionRing α
inst✝ : Monoid β
φ : β →* α
x : β
k : ℕ+
h : x ^ ↑k = 1
⊢ 0 ≤ 1

case Hnpos
α : Type u_2
β : Type u_1
γ : Type ?u.289026
ι : Type ?u.289029
inst✝¹ : NormedDivisionRing α
inst✝ : Monoid β
φ : β →* α
x : β
k : ℕ+
h : x ^ ↑k = 1
⊢ 0 < ↑k
α : Type u_2
β : Type u_1
γ : Type ?u.289026
ι : Type ?u.289029
inst✝¹ : NormedDivisionRing α
inst✝ : Monoid β
φ : β →* α
x : β
k : ℕ+
h : x ^ ↑k = 1
⊢ ‖↑φ x‖ = 1
rw [← pow_left_inj, ← norm_pow, ← map_pow, h, map_one, norm_one, one_pow]
no goals
case Hxpos
α : Type u_2
β : Type u_1
γ : Type ?u.289026
ι : Type ?u.289029
inst✝¹ : NormedDivisionRing α
inst✝ : Monoid β
φ : β →* α
x : β
k : ℕ+
h : x ^ ↑k = 1
⊢ 0 ≤ ‖↑φ x‖

case Hypos
α : Type u_2
β : Type u_1
γ : Type ?u.289026
ι : Type ?u.289029
inst✝¹ : NormedDivisionRing α
inst✝ : Monoid β
φ : β →* α
x : β
k : ℕ+
h : x ^ ↑k = 1
⊢ 0 ≤ 1

case Hnpos
α : Type u_2
β : Type u_1
γ : Type ?u.289026
ι : Type ?u.289029
inst✝¹ : NormedDivisionRing α
inst✝ : Monoid β
φ : β →* α
x : β
k : ℕ+
h : x ^ ↑k = 1
⊢ 0 < ↑k
exacts [norm_nonneg _, zero_le_one, k.pos]