-- Lean 4 proof step from Mathlib.RingTheory.PolynomialAlgebra (goal)
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
simp :
  ((p₁ * p₂).sum fun (n : ℕ) (r : R) ↦
      (monomial n : (a : A) → A[X]) (HMul.hMul (β := A) (a₁ * a₂) ((algebraMap R A : (a : R) → A) r : A))) =
    HMul.hMul (α := A[X])
      (p₁.sum fun (n : ℕ) (r : R) ↦
        (monomial n : (a : A) → A[X]) (HMul.hMul (β := A) a₁ ((algebraMap R A : (a : R) → A) r : A)))
      (p₂.sum fun (n : ℕ) (r : R) ↦
        (monomial n : (a : A) → A[X]) (HMul.hMul (β := A) a₂ ((algebraMap R A : (a : R) → A) r : A)))
a :
  ∀ (k : ℕ),
    coeff
        ((p₁ * p₂).sum fun (n : ℕ) (r : R) ↦
          (monomial n : (a : A) → A[X]) (HMul.hMul (β := A) (a₁ * a₂) ((algebraMap R A : (a : R) → A) r : A)))
        k =
      (HMul.hMul (α := A[X])
            (p₁.sum fun (n : ℕ) (r : R) ↦
              (monomial n : (a : A) → A[X]) (HMul.hMul (β := A) a₁ ((algebraMap R A : (a : R) → A) r : A)))
            (p₂.sum fun (n : ℕ) (r : R) ↦
              (monomial n : (a : A) → A[X]) (HMul.hMul (β := A) a₂ ((algebraMap R A : (a : R) → A) r : A)))).coeff
        k
a₃ :
  ∀ (k : ℕ),
    (if ¬(p₁ * p₂).coeff k = 0 then
        HMul.hMul (β := A) (a₁ * a₂) ((algebraMap R A : (a : R) → A) ((p₁ * p₂).coeff k) : A)
      else 0) =
      (HMul.hMul (α := A[X])
            (∑ n ∈ p₁.support,
              (monomial n : (a : A) → A[X]) (HMul.hMul (β := A) a₁ ((algebraMap R A : (a : R) → A) (p₁.coeff n) : A)))
            (∑ n ∈ p₂.support,
              (monomial n : (a : A) → A[X])
                (HMul.hMul (β := A) a₂ ((algebraMap R A : (a : R) → A) (p₂.coeff n) : A)))).coeff
        k
a₄ :
  ∀ (k : ℕ),
    (if ¬(p₁ * p₂).coeff k = 0 then
        HMul.hMul (β := A) (a₁ * a₂) ((algebraMap R A : (a : R) → A) ((p₁ * p₂).coeff k) : A)
      else 0) =
      ∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k,
        HMul.hMul (α := A)
          (coeff
            (∑ n ∈ p₁.support,
              (monomial n : (a : A) → A[X]) (HMul.hMul (β := A) a₁ ((algebraMap R A : (a : R) → A) (p₁.coeff n) : A)))
            x.1)
          (coeff
            (∑ n ∈ p₂.support,
              (monomial n : (a : A) → A[X]) (HMul.hMul (β := A) a₂ ((algebraMap R A : (a : R) → A) (p₂.coeff n) : A)))
            x.2)
⊢ (toFunLinear R A : (a : A ⊗[R] R[X]) → A[X]) ((a₁ * a₂) ⊗ₜ[R] (p₁ * p₂)) =
    HMul.hMul (α := A[X]) (β := A[X]) ((toFunLinear R A : (a : A ⊗[R] R[X]) → A[X]) (a₁ ⊗ₜ[R] p₁) : A[X])
      ((toFunLinear R A : (a : A ⊗[R] R[X]) → A[X]) (a₂ ⊗ₜ[R] p₂) : A[X])
have a₅ : ∀ (k : ℕ),
  (if ¬(p₁ * p₂).coeff k = 0 then HMul.hMul (β := A) (a₁ * a₂) ((algebraMap R A : (a : R) → A) ((p₁ * p₂).coeff k) : A)
    else 0) =
    ∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k,
      if ¬p₂.coeff x.2 = 0 then
        if ¬p₁.coeff x.1 = 0 then
          HMul.hMul (β := A) a₁ ((algebraMap R A : (a : R) → A) (p₁.coeff x.1) : A) *
            HMul.hMul (β := A) a₂ ((algebraMap R A : (a : R) → A) (p₂.coeff x.2) : A)
        else 0
      else 0
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 [finsetSum_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]