case ofNat
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarSemigroup R
U : { x // x ∈ unitary R }
a✝ : ℕ
⊢ ↑(U ^ Int.ofNat a✝) = ↑U ^ Int.ofNat a✝

case negSucc
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarSemigroup R
U : { x // x ∈ unitary R }
a✝ : ℕ
⊢ ↑(U ^ Int.negSucc a✝) = ↑U ^ Int.negSucc a✝
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarSemigroup R
U : { x // x ∈ unitary R }
z : ℤ
⊢ ↑(U ^ z) = ↑U ^ z
induction z
no goals
case ofNat
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarSemigroup R
U : { x // x ∈ unitary R }
a✝ : ℕ
⊢ ↑(U ^ Int.ofNat a✝) = ↑U ^ Int.ofNat a✝
simp [SubmonoidClass.coe_pow]
no goals
case negSucc
R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarSemigroup R
U : { x // x ∈ unitary R }
a✝ : ℕ
⊢ ↑(U ^ Int.negSucc a✝) = ↑U ^ Int.negSucc a✝
simp [coe_inv]