awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
k : ℕ
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ a₁ * HMul.hMul (β := A) a₂ ((algebraMap R A : (a : R) → A) ((p₁ * p₂).coeff k) : A) =
    a₁ *
      (a₂ *
        ∑ i ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k,
          HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (p₂.coeff i.2) : A)
            ((algebraMap R A : (a : R) → A) (p₁.coeff i.1) : A))
have e_a : Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) ((p₁ * p₂).coeff k) : A)
  (∑ i ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k,
      HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (p₂.coeff i.2) : A)
        ((algebraMap R A : (a : R) → A) (p₁.coeff i.1) : A) :
    A)
Tactic: congr
-- 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
k : ℕ
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) ((p₁ * p₂).coeff k) : A)
    (∑ i ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k,
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (p₂.coeff i.2) : A)
          ((algebraMap R A : (a : R) → A) (p₁.coeff i.1) : A) :
      A)
have e_a : Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) ((p₁ * p₂).coeff k) : A)
  (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k,
      HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (p₁.coeff x.1) : A)
        ((algebraMap R A : (a : R) → A) (p₂.coeff x.2) : A) :
    A)
Tactic: simp_rw [Algebra.commutes (coeff p₂ _), coeff_mul, map_sum, map_mul]
-- 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
k : ℕ
a₁ a₂ : A
p₁ p₂ : R[X]
e_a :
  Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) ((p₁ * p₂).coeff k) : A)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k,
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (p₁.coeff x.1) : A)
          ((algebraMap R A : (a : R) → A) (p₂.coeff x.2) : A) :
      A)
⊢ Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) ((p₁ * p₂).coeff k) : A)
    (∑ i ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k,
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (p₂.coeff i.2) : A)
          ((algebraMap R A : (a : R) → A) (p₁.coeff i.1) : A) :
      A)
have e_a₁ : Eq.{u_3 + 1} (α := A)
  ((algebraMap R A : (a : R) → A) (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k, p₁.coeff x.1 * p₂.coeff x.2) : A)
  (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k,
      HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (p₁.coeff x.1) : A)
        ((algebraMap R A : (a : R) → A) (p₂.coeff x.2) : A) :
    A)
Tactic: simp_rw [Algebra.commutes (coeff p₂ _), coeff_mul, map_sum, map_mul]
-- 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
k : ℕ
a₁ a₂ : A
p₁ p₂ : R[X]
e_a :
  Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) ((p₁ * p₂).coeff k) : A)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k,
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (p₁.coeff x.1) : A)
          ((algebraMap R A : (a : R) → A) (p₂.coeff x.2) : A) :
      A)
e_a₁ :
  Eq.{u_3 + 1} (α := A)
    ((algebraMap R A : (a : R) → A) (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k, p₁.coeff x.1 * p₂.coeff x.2) :
      A)
    (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k,
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (p₁.coeff x.1) : A)
          ((algebraMap R A : (a : R) → A) (p₂.coeff x.2) : A) :
      A)
⊢ Eq.{u_3 + 1} (α := A) ((algebraMap R A : (a : R) → A) ((p₁ * p₂).coeff k) : A)
    (∑ i ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k,
        HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (p₂.coeff i.2) : A)
          ((algebraMap R A : (a : R) → A) (p₁.coeff i.1) : A) :
      A)
have e_a₂ : Eq.{u_3 + 1} (α := A)
  (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k, (algebraMap R A : (a : R) → A) (p₁.coeff x.1 * p₂.coeff x.2))
  (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k,
    HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) (p₁.coeff x.1) : A)
      ((algebraMap R A : (a : R) → A) (p₂.coeff x.2) : A))
Tactic: simp_rw [Algebra.commutes (coeff p₂ _), coeff_mul, map_sum, map_mul]
-- 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]
⊢ (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 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)))
Tactic: simp only [toFunLinear_tmul_apply, toFunBilinear_apply_eq_sum]
-- 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]
⊢ ((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)))
have 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
Tactic: ext k
-- 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]
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
have a : (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
Tactic: simp_rw [coeff_sum, coeff_monomial, sum_def, Finset.sum_ite_eq', mem_support_iff, Ne]
-- 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]
k : ℕ
| (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
have rw : ∑ 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)
Tactic: rw [coeff_mul]
-- 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]
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
have a : (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)
Tactic: conv_rhs => rw [coeff_mul]
-- 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]
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)
have a : (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: simp_rw [finsetSum_coeff, coeff_monomial, Finset.sum_ite_eq', mem_support_iff, Ne, mul_ite,
      mul_zero, ite_mul, zero_mul]
-- 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]
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
have a : (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) else 0) *
        HMul.hMul (β := A) a₂ ((algebraMap R A : (a : R) → A) (p₂.coeff x.2) : A)
    else 0
Tactic: simp_rw [← ite_zero_mul (¬coeff p₁ _ = 0) (a₁ * (algebraMap R A) (coeff p₁ _))]
-- 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]
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) else 0) *
          HMul.hMul (β := A) a₂ ((algebraMap R A : (a : R) → A) (p₂.coeff x.2) : A)
      else 0
have a : (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.1 = 0 then HMul.hMul (β := A) a₁ ((algebraMap R A : (a : R) → A) (p₁.coeff x.1) : A) else 0) *
      if ¬p₂.coeff x.2 = 0 then HMul.hMul (β := A) a₂ ((algebraMap R A : (a : R) → A) (p₂.coeff x.2) : A) else 0
Tactic: simp_rw [← mul_ite_zero (¬coeff p₂ _ = 0) _ (_ * _)]
-- 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]
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.1 = 0 then HMul.hMul (β := A) a₁ ((algebraMap R A : (a : R) → A) (p₁.coeff x.1) : A) else 0) *
        if ¬p₂.coeff x.2 = 0 then HMul.hMul (β := A) a₂ ((algebraMap R A : (a : R) → A) (p₂.coeff x.2) : A) else 0
have a : HMul.hMul (β := A) (a₁ * a₂) ((algebraMap R A : (a : R) → A) ((p₁ * p₂).coeff k) : A) =
  ∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ k,
    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)
Tactic: simp_rw [toFunLinear_mul_tmul_mul_aux_1, toFunLinear_mul_tmul_mul_aux_2]
-- 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]
⊢ (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 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)))
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]
-- 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)))
⊢ (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 : ℕ),
  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
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]
-- 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
⊢ (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) =
    (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
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]
-- 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
⊢ (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,
      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)
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]
-- 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
⊢ Eq.{u_3 + 1} (α := A[X]) ((toFunLinear R A : (a : A ⊗[R] R[X]) → A[X]) (1 ⊗ₜ[R] 1) : A[X]) (1 : A[X])
have rw : Eq.{u_3 + 1} (α := A[X]) (((toFunBilinear R A : (a : A) → R[X] →ₗ[R] A[X]) 1 : (a : R[X]) → A[X]) 1) 1
Tactic: rw [toFunLinear_tmul_apply, toFunBilinear_apply_apply, Polynomial.aeval_one, one_smul]