u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
ea eb : ℕ
a₂ b₂ x : R
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂)
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
ea eb e : ℕ
a₂ b₂ c x : R
x✝¹ : ea + eb = e
x✝ : a₂ * b₂ = c
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ e * c
subst_vars
no goals
u : Lean.Level
R : Type u_1
α : Q(Type u)
sα : Q(CommSemiring «$α»)
inst✝ : CommSemiring R
ea eb : ℕ
a₂ b₂ x : R
⊢ x ^ ea * a₂ * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂)
simp [pow_add, mul_mul_mul_comm]