u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
k : ℕ
⊢ a ^ Nat.add (Nat.mul 2 k) 1 = a ^ k * a ^ k * a
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a : R
k : ℕ
b c d : R
x✝² : a ^ k = b
x✝¹ : b * b = c
x✝ : c * a = d
⊢ a ^ Nat.add (Nat.mul 2 k) 1 = d
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.add (Nat.mul 2 k) 1 = a ^ k * a ^ k * a
simp [Nat.succ_mul, pow_add]