-- Mathlib/RingTheory/PolynomialAlgebra.lean
theorem toFunLinear_mul_tmul_mul (a₁ a₂ : A) (p₁ p₂ : R[X]) :
    (toFunLinear R A) ((a₁ * a₂) ⊗ₜ[R] (p₁ * p₂)) =
      (toFunLinear R A) (a₁ ⊗ₜ[R] p₁) * (toFunLinear R A) (a₂ ⊗ₜ[R] p₂)

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ (toFunLinear R A) ((a₁ * a₂) ⊗ₜ[R] (p₁ * p₂)) = (toFunLinear R A) (a₁ ⊗ₜ[R] p₁) * (toFunLinear R A) (a₂ ⊗ₜ[R] p₂)

Tactic:
classical
  simp only [toFunLinear_tmul_apply, toFunBilinear_apply_eq_sum]
  ext k
  simp_rw [coeff_sum, coeff_monomial, sum_def, Finset.sum_ite_eq', mem_support_iff, Ne]
  conv_rhs => rw [coeff_mul]
  simp_rw [finset_sum_coeff, coeff_monomial, Finset.sum_ite_eq', mem_support_iff, Ne, mul_ite,
    mul_zero, ite_mul, zero_mul]
  simp_rw [← ite_zero_mul (¬coeff p₁ _ = 0) (a₁ * (algebraMap R A) (coeff p₁ _))]
  simp_rw [← mul_ite_zero (¬coeff p₂ _ = 0) _ (_ * _)]
  simp_rw [toFunLinear_mul_tmul_mul_aux_1, toFunLinear_mul_tmul_mul_aux_2]

Result:
no goals

Proof state:
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬(p₁ * p₂).coeff k = 0 then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ∑ x ∈ Finset.antidiagonal k,
      (∑ n ∈ p₁.support, (monomial n) (a₁ * (algebraMap R A) (p₁.coeff n))).coeff x.1 *
        (∑ n ∈ p₂.support, (monomial n) (a₂ * (algebraMap R A) (p₂.coeff n))).coeff x.2

Tactic:
simp_rw [finset_sum_coeff, coeff_monomial, Finset.sum_ite_eq', mem_support_iff, Ne, mul_ite,
  mul_zero, ite_mul, zero_mul]

Result:
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬(p₁ * p₂).coeff k = 0 then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ∑ x ∈ Finset.antidiagonal k,
      if ¬p₂.coeff x.2 = 0 then
        if ¬p₁.coeff x.1 = 0 then a₁ * (algebraMap R A) (p₁.coeff x.1) * (a₂ * (algebraMap R A) (p₂.coeff x.2)) else 0
      else 0

Proof state:
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ ((p₁ * p₂).sum fun n r => (monomial n) (a₁ * a₂ * (algebraMap R A) r)).coeff k =
    ((p₁.sum fun n r => (monomial n) (a₁ * (algebraMap R A) r)) *
          p₂.sum fun n r => (monomial n) (a₂ * (algebraMap R A) r)).coeff
      k

Tactic:
simp_rw [coeff_sum, coeff_monomial, sum_def, Finset.sum_ite_eq', mem_support_iff, Ne]

Result:
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬(p₁ * p₂).coeff k = 0 then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ((∑ n ∈ p₁.support, (monomial n) (a₁ * (algebraMap R A) (p₁.coeff n))) *
          ∑ n ∈ p₂.support, (monomial n) (a₂ * (algebraMap R A) (p₂.coeff n))).coeff
      k

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ ((p₁ * p₂).sum fun n r => (monomial n) (a₁ * a₂ * (algebraMap R A) r)) =
    (p₁.sum fun n r => (monomial n) (a₁ * (algebraMap R A) r)) *
      p₂.sum fun n r => (monomial n) (a₂ * (algebraMap R A) r)

Tactic:
ext k

Result:
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ ((p₁ * p₂).sum fun n r => (monomial n) (a₁ * a₂ * (algebraMap R A) r)).coeff k =
    ((p₁.sum fun n r => (monomial n) (a₁ * (algebraMap R A) r)) *
          p₂.sum fun n r => (monomial n) (a₂ * (algebraMap R A) r)).coeff
      k

Proof state:
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬(p₁ * p₂).coeff k = 0 then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ∑ x ∈ Finset.antidiagonal k,
      (if ¬p₁.coeff x.1 = 0 then a₁ * (algebraMap R A) (p₁.coeff x.1) else 0) *
        if ¬p₂.coeff x.2 = 0 then a₂ * (algebraMap R A) (p₂.coeff x.2) else 0

Tactic:
simp_rw [toFunLinear_mul_tmul_mul_aux_1, toFunLinear_mul_tmul_mul_aux_2]

Result:
no goals

Proof state:
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬(p₁ * p₂).coeff k = 0 then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ∑ x ∈ Finset.antidiagonal k,
      if ¬p₂.coeff x.2 = 0 then
        if ¬p₁.coeff x.1 = 0 then a₁ * (algebraMap R A) (p₁.coeff x.1) * (a₂ * (algebraMap R A) (p₂.coeff x.2)) else 0
      else 0

Tactic:
simp_rw [← ite_zero_mul (¬coeff p₁ _ = 0) (a₁ * (algebraMap R A) (coeff p₁ _))]

Result:
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬(p₁ * p₂).coeff k = 0 then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ∑ x ∈ Finset.antidiagonal k,
      if ¬p₂.coeff x.2 = 0 then
        (if ¬p₁.coeff x.1 = 0 then a₁ * (algebraMap R A) (p₁.coeff x.1) else 0) * (a₂ * (algebraMap R A) (p₂.coeff x.2))
      else 0

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ (toFunLinear R A) ((a₁ * a₂) ⊗ₜ[R] (p₁ * p₂)) = (toFunLinear R A) (a₁ ⊗ₜ[R] p₁) * (toFunLinear R A) (a₂ ⊗ₜ[R] p₂)

Tactic:
simp only [toFunLinear_tmul_apply, toFunBilinear_apply_eq_sum]

Result:
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ ((p₁ * p₂).sum fun n r => (monomial n) (a₁ * a₂ * (algebraMap R A) r)) =
    (p₁.sum fun n r => (monomial n) (a₁ * (algebraMap R A) r)) *
      p₂.sum fun n r => (monomial n) (a₂ * (algebraMap R A) r)

Proof state:
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬(p₁ * p₂).coeff k = 0 then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ∑ x ∈ Finset.antidiagonal k,
      if ¬p₂.coeff x.2 = 0 then
        (if ¬p₁.coeff x.1 = 0 then a₁ * (algebraMap R A) (p₁.coeff x.1) else 0) * (a₂ * (algebraMap R A) (p₂.coeff x.2))
      else 0

Tactic:
simp_rw [← mul_ite_zero (¬coeff p₂ _ = 0) _ (_ * _)]

Result:
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬(p₁ * p₂).coeff k = 0 then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ∑ x ∈ Finset.antidiagonal k,
      (if ¬p₁.coeff x.1 = 0 then a₁ * (algebraMap R A) (p₁.coeff x.1) else 0) *
        if ¬p₂.coeff x.2 = 0 then a₂ * (algebraMap R A) (p₂.coeff x.2) else 0

Proof state:
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬(p₁ * p₂).coeff k = 0 then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ((∑ n ∈ p₁.support, (monomial n) (a₁ * (algebraMap R A) (p₁.coeff n))) *
          ∑ n ∈ p₂.support, (monomial n) (a₂ * (algebraMap R A) (p₂.coeff n))).coeff
      k

Tactic:
conv_rhs => rw [coeff_mul]

Result:
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬(p₁ * p₂).coeff k = 0 then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ∑ x ∈ Finset.antidiagonal k,
      (∑ n ∈ p₁.support, (monomial n) (a₁ * (algebraMap R A) (p₁.coeff n))).coeff x.1 *
        (∑ n ∈ p₂.support, (monomial n) (a₂ * (algebraMap R A) (p₂.coeff n))).coeff x.2