R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
k : ℕ
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ a₁ * (a₂ * ↑(algebraMap R A) (coeff (p₁ * p₂) k)) =
    a₁ *
      (a₂ *
        Finset.sum (Finset.Nat.antidiagonal k) fun x =>
          ↑(algebraMap R A) (coeff p₂ x.snd) * ↑(algebraMap R A) (coeff p₁ x.fst))
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
k : ℕ
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ a₁ * a₂ * ↑(algebraMap R A) (coeff (p₁ * p₂) k) =
    Finset.sum (Finset.Nat.antidiagonal k) fun x =>
      a₁ * ↑(algebraMap R A) (coeff p₁ x.fst) * (a₂ * ↑(algebraMap R A) (coeff p₂ x.snd))
simp_rw [mul_assoc, Algebra.commutes, ← Finset.mul_sum, mul_assoc, ← Finset.mul_sum]
case e_a.e_a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
k : ℕ
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ ↑(algebraMap R A) (coeff (p₁ * p₂) k) =
    Finset.sum (Finset.Nat.antidiagonal k) fun x =>
      ↑(algebraMap R A) (coeff p₂ x.snd) * ↑(algebraMap R A) (coeff p₁ x.fst)
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
k : ℕ
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ a₁ * (a₂ * ↑(algebraMap R A) (coeff (p₁ * p₂) k)) =
    a₁ *
      (a₂ *
        Finset.sum (Finset.Nat.antidiagonal k) fun x =>
          ↑(algebraMap R A) (coeff p₂ x.snd) * ↑(algebraMap R A) (coeff p₁ x.fst))
congr
no goals
case e_a.e_a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
k : ℕ
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ ↑(algebraMap R A) (coeff (p₁ * p₂) k) =
    Finset.sum (Finset.Nat.antidiagonal k) fun x =>
      ↑(algebraMap R A) (coeff p₂ x.snd) * ↑(algebraMap R A) (coeff p₁ x.fst)
simp_rw [Algebra.commutes (coeff p₂ _), coeff_mul, map_sum, RingHom.map_mul]