exact (mul_one a).symm
α✝ : Type u
inst✝³ : OfNat α✝ 1
inst✝² : HMul α✝ α✝ α✝
α : Type u_1
inst✝¹ : OfNat α 1
inst✝ : HMul α α α
mul_one : ∀ (a : α), a * 1 = a
one_mul : ∀ (a : α), 1 * a = a
assoc : ∀ (a b c : α), a * b * c = a * (b * c)
a : α
⊢ a = gpow a 1
no goals