awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PolynomialAlgebra
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)
    (∑ 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)
⊢ 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))

Tactic:
congr
-- Module: Mathlib.RingTheory.PolynomialAlgebra
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)
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))
⊢ 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:
simp_rw [Algebra.commutes (coeff p₂ _), coeff_mul, map_sum, map_mul]

Premises used: Polynomial.coeff_mul, map_sum, Polynomial.coeff, map_mul, Algebra.commutes
-- Module: Mathlib.RingTheory.PolynomialAlgebra
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])

Tactic:
simp only [toFunLinear_tmul_apply, toFunBilinear_apply_eq_sum]

Premises used: PolyEquivTensor.toFunBilinear_apply_eq_sum, PolyEquivTensor.toFunLinear_tmul_apply
-- Module: Mathlib.RingTheory.PolynomialAlgebra
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]
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
⊢ ((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:
ext k
-- Module: Mathlib.RingTheory.PolynomialAlgebra
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 : ℕ
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
⊢ 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:
simp_rw [coeff_sum, coeff_monomial, sum_def, Finset.sum_ite_eq', mem_support_iff, Ne]

Premises used: Finset.sum_ite_eq', Polynomial.mem_support_iff, Ne, Polynomial.coeff_monomial, Polynomial.coeff_sum, Polynomial.sum_def
-- Module: Mathlib.RingTheory.PolynomialAlgebra
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 : ℕ
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)
| (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:
rw [coeff_mul]

Premises used: Polynomial.coeff_mul
-- Module: Mathlib.RingTheory.PolynomialAlgebra
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 : ℕ
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)
⊢ (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:
conv_rhs => rw [coeff_mul]

Premises used: Polynomial.coeff_mul
-- Module: Mathlib.RingTheory.PolynomialAlgebra
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 : ℕ
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
⊢ (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:
simp_rw [finsetSum_coeff, coeff_monomial, Finset.sum_ite_eq', mem_support_iff, Ne, mul_ite,
      mul_zero, ite_mul, zero_mul]

Premises used: Finset.sum_ite_eq', MulZeroClass.zero_mul, mul_ite, Polynomial.mem_support_iff, Polynomial.finsetSum_coeff, Ne, Polynomial.coeff_monomial, MulZeroClass.mul_zero, ite_mul
-- Module: Mathlib.RingTheory.PolynomialAlgebra
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 : ℕ
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
⊢ (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 [← ite_zero_mul (¬coeff p₁ _ = 0) (a₁ * (algebraMap R A) (coeff p₁ _))]

Premises used: HMul.hMul, Algebra.algebraMap, ite_zero_mul, Polynomial.coeff, OfNat.ofNat, Eq, DFunLike.coe, Not
-- Module: Mathlib.RingTheory.PolynomialAlgebra
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 : ℕ
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
⊢ (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 [← mul_ite_zero (¬coeff p₂ _ = 0) _ (_ * _)]

Premises used: HMul.hMul, Polynomial.coeff, mul_ite_zero, OfNat.ofNat, Eq, Not
-- Module: Mathlib.RingTheory.PolynomialAlgebra
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 : ℕ
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)
⊢ (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 [toFunLinear_mul_tmul_mul_aux_1, toFunLinear_mul_tmul_mul_aux_2]

Premises used: PolyEquivTensor.toFunLinear_mul_tmul_mul_aux_2, PolyEquivTensor.toFunLinear_mul_tmul_mul_aux_1
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
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
rw₁ : HSMul.hSMul (α := A) (β := A[X]) 1 ((aeval X : (a : R[X]) → A[X]) 1) = 1
rw₂ : HSMul.hSMul (α := A) (β := A[X]) 1 1 = 1
rw₃ rw₄ : Eq.{u_3 + 1} (α := A[X]) 1 1
⊢ Eq.{u_3 + 1} (α := A[X]) ((toFunLinear R A : (a : A ⊗[R] R[X]) → A[X]) (1 ⊗ₜ[R] 1) : A[X]) (1 : A[X])

Tactic:
rw [toFunLinear_tmul_apply, toFunBilinear_apply_apply, Polynomial.aeval_one, one_smul]

Premises used: Polynomial.aeval_one, one_smul, PolyEquivTensor.toFunBilinear_apply_apply, PolyEquivTensor.toFunLinear_tmul_apply
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
p : R[X]
⊢ (toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) (a ⊗ₜ[R] p) =
    HSMul.hSMul (β := A[X]) a (Polynomial.map (algebraMap R A) p)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, MonoidHomClass.toMonoidHom, List.foldl, RingHomClass.toRingHom, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
a : A
p : R[X]
⊢ Eq.{u_3 + 1} (α := A[X]) ((toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) (a ⊗ₜ[R] p) : 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)) :
      A[X])

Tactic:
toFunBilinear_apply_eq_sum R A _ _

Premises used: PolyEquivTensor.toFunBilinear_apply_eq_sum, Quotient.liftOn', AddCon.liftOn, List.foldl, FreeAddMonoid.sumAux
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
p q : A[X]
⊢ invFun R A (p + q) = HAdd.hAdd (α := A ⊗[R] R[X]) (invFun R A p) (invFun R A q)

Tactic:
simp only [invFun, eval₂_add]

Premises used: PolyEquivTensor.invFun, Polynomial.eval₂_add
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
n : ℕ
a : A
⊢ invFun R A ((monomial n : (a : A) → A[X]) a) = a ⊗ₜ[R] 1 * HPow.hPow (α := A ⊗[R] R[X]) (1 ⊗ₜ[R] X) n

Tactic:
eval₂_monomial _ _

Premises used: Polynomial.eval₂_monomial, PolyEquivTensor.invFun
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A ⊗[R] R[X]
⊢ invFun R A ((toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) x) = x

Tactic:
TensorProduct.induction_on x ?_ ?_ ?_

Premises used: TensorProduct.induction_on
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A ⊗[R] R[X]
refine_1 : Eq (α := A ⊗[R] R[X]) (invFun R A ((toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) 0)) 0
refine_2 :
  ∀ (x : A) (y : R[X]),
    Eq (α := A ⊗[R] R[X]) (invFun R A ((toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) (x ⊗ₜ[R] y))) (x ⊗ₜ[R] y)
refine_3 :
  ∀ (x y : A ⊗[R] R[X]),
    invFun R A ((toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) x) = x →
      invFun R A ((toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) y) = y →
        invFun R A ((toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) (x + y)) = x + y
⊢ invFun R A ((toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) x) = x

Tactic:
refine TensorProduct.induction_on x ?_ ?_ ?_
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A ⊗[R] R[X]
⊢ Eq (α := A ⊗[R] R[X]) (invFun R A ((toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) 0)) 0

Tactic:
simp [invFun]

Premises used: PolyEquivTensor.invFun
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
refine_2 :
  Eq (α := A ⊗[R] R[X])
    (p.sum fun (n : ℕ) (a_1 : R) ↦
      eval₂ (↑includeLeft : A →+* A ⊗[R] R[X]) (1 ⊗ₜ[R] X)
        ((monomial n : (a : A) → A[X]) (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) a_1 : A))))
    (a ⊗ₜ[R] p)
⊢ eval₂ (↑includeLeft : A →+* A ⊗[R] R[X]) (1 ⊗ₜ[R] X) ((toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) (a ⊗ₜ[R] p)) =
    a ⊗ₜ[R] p

Tactic:
rw [toFunAlgHom_apply_tmul, eval₂_sum]

Premises used: PolyEquivTensor.toFunAlgHom_apply_tmul, Polynomial.eval₂_sum
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
refine_2 : Eq (α := A ⊗[R] R[X]) (a ⊗ₜ[R] ∑ a ∈ p.support, p.coeff a • HPow.hPow (α := R[X]) X a) (a ⊗ₜ[R] p)
⊢ Eq (α := A ⊗[R] R[X])
    (p.sum fun (n : ℕ) (a_1 : R) ↦
      eval₂ (↑includeLeft : A →+* A ⊗[R] R[X]) (1 ⊗ₜ[R] X)
        ((monomial n : (a : A) → A[X]) (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) a_1 : A))))
    (a ⊗ₜ[R] p)

Tactic:
simp_rw [eval₂_monomial, AlgHom.coe_toRingHom, Algebra.TensorProduct.tmul_pow, one_pow,
      Algebra.TensorProduct.includeLeft_apply, Algebra.TensorProduct.tmul_mul_tmul, mul_one,
      one_mul, ← Algebra.commutes, ← Algebra.smul_def, smul_tmul, sum_def, ← tmul_sum]

Premises used: one_pow, AlgHom.coe_toRingHom, TensorProduct.smul_tmul, Polynomial.eval₂_monomial, Algebra.TensorProduct.includeLeft_apply, Algebra.TensorProduct.tmul_mul_tmul, TensorProduct.tmul_sum, Algebra.TensorProduct.tmul_pow, Polynomial.sum_def, Algebra.smul_def, mul_one, Algebra.commutes, one_mul
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
rw :
  a ⊗ₜ[R] p.sum fun (n : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)
| a ⊗ₜ[R] p

Tactic:
rw [← sum_C_mul_X_pow_eq p]

Premises used: Polynomial.sum_C_mul_X_pow_eq
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
refine_2 :
  Eq (α := A ⊗[R] R[X]) (a ⊗ₜ[R] ∑ a ∈ p.support, p.coeff a • HPow.hPow (α := R[X]) X a)
    (a ⊗ₜ[R]
      p.sum fun (n : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ Eq (α := A ⊗[R] R[X]) (a ⊗ₜ[R] ∑ a ∈ p.support, p.coeff a • HPow.hPow (α := R[X]) X a) (a ⊗ₜ[R] p)

Tactic:
conv_rhs => rw [← sum_C_mul_X_pow_eq p]

Premises used: Polynomial.sum_C_mul_X_pow_eq
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
refine_2 :
  Eq (α := A ⊗[R] R[X])
    (a ⊗ₜ[R]
      ∑ x ∈ p.support,
        HMul.hMul (α := R[X]) ((algebraMap R R[X] : (a : R) → R[X]) (p.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x))
    (a ⊗ₜ[R]
      p.sum fun (n : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ Eq (α := A ⊗[R] R[X]) (a ⊗ₜ[R] ∑ a ∈ p.support, p.coeff a • HPow.hPow (α := R[X]) X a)
    (a ⊗ₜ[R]
      p.sum fun (n : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))

Tactic:
simp only [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ Eq (α := A ⊗[R] R[X])
    (a ⊗ₜ[R]
      ∑ x ∈ p.support,
        HMul.hMul (α := R[X]) ((algebraMap R R[X] : (a : R) → R[X]) (p.coeff x) : R[X]) (HPow.hPow (α := R[X]) X x))
    (a ⊗ₜ[R]
      p.sum fun (n : ℕ) (a : R) ↦ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n))

Tactic:
rfl
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x p q : A ⊗[R] R[X]
hp : invFun R A ((toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) p) = p
hq : invFun R A ((toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) q) = q
⊢ invFun R A ((toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) (p + q)) = p + q

Tactic:
simp only [map_add, invFun_add, hp, hq]

Premises used: map_add, PolyEquivTensor.invFun_add
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A[X]
⊢ (toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) (invFun R A x) = x

Tactic:
Polynomial.induction_on' x ?_ ?_

Premises used: Polynomial.induction_on'
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A[X]
refine_1 :
  ∀ (p q : A[X]),
    (toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) (invFun R A p) = p →
      (toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) (invFun R A q) = q →
        (toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) (invFun R A (p + q)) = p + q
refine_2 :
  ∀ (n : ℕ) (a : A),
    Eq.{u_3 + 1} (α := A[X])
      ((toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) (invFun R A ((monomial n : (a : A) → A[X]) a)) : A[X])
      ((monomial n : (a : A) → A[X]) a : A[X])
⊢ (toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) (invFun R A x) = x

Tactic:
refine Polynomial.induction_on' x ?_ ?_
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x p q : A[X]
hp : (toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) (invFun R A p) = p
hq : (toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) (invFun R A q) = q
⊢ (toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) (invFun R A (p + q)) = p + q

Tactic:
simp only [invFun_add, map_add, hp, hq]

Premises used: map_add, PolyEquivTensor.invFun_add
-- Module: Mathlib.RingTheory.PolynomialAlgebra
Goal:
R : Type u_1
A : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
x : A[X]
n : ℕ
a : A
refine_2 :
  Eq (α := A[X]) ((monomial n : (a : A) → A[X]) (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) 1 : A)) : A[X])
    ((monomial n : (a : A) → A[X]) a : A[X])
refine_2₁ :
  Eq (α := A[X]) ((monomial n : (a : A) → A[X]) (HMul.hMul (β := A) a ((algebraMap R A : (a : R) → A) 0 : A)) : A[X])
    (0 : A[X])
⊢ Eq.{u_3 + 1} (α := A[X])
    ((toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) (invFun R A ((monomial n : (a : A) → A[X]) a)) : A[X])
    ((monomial n : (a : A) → A[X]) a : A[X])

Tactic:
rw [invFun_monomial, Algebra.TensorProduct.tmul_pow,
        one_pow, Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul, toFunAlgHom_apply_tmul,
        X_pow_eq_monomial, sum_monomial_index]

Premises used: one_pow, PolyEquivTensor.toFunAlgHom_apply_tmul, Polynomial.X_pow_eq_monomial, Polynomial.sum_monomial_index, Algebra.TensorProduct.tmul_mul_tmul, Algebra.TensorProduct.tmul_pow, PolyEquivTensor.invFun_monomial, mul_one, one_mul