u : Lean.Level
R : Type ?u.272248
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
c₂ k a₁ a₂ : ℕ
⊢ a₁ ^ a₂ * (c₂ * k) = a₁ ^ a₂ * c₂ * k
u : Lean.Level
R : Type ?u.272248
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
a₃ c₂ k a₁ a₂ : ℕ
x✝ : a₃ = c₂ * k
⊢ a₁ ^ a₂ * a₃ = a₁ ^ a₂ * c₂ * k
subst_vars
no goals
u : Lean.Level
R : Type ?u.272248
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
c₂ k a₁ a₂ : ℕ
⊢ a₁ ^ a₂ * (c₂ * k) = a₁ ^ a₂ * c₂ * k
rw [mul_assoc]