u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
k : ℕ
⊢ a ^ Nat.mul 2 k = a ^ k * a ^ k
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
k : ℕ
b c : R
x✝¹ : a ^ k = b
x✝ : b * b = c
⊢ a ^ Nat.mul 2 k = c
subst_vars
no goals
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
k : ℕ
⊢ a ^ Nat.mul 2 k = a ^ k * a ^ k
simp [Nat.succ_mul, pow_add]