awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
ι : Type u_2
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring N
inst_4 : Algebra R N
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
h :
  ∀ (s : σ),
    Eq (α := A ⊗[R] MvPolynomial σ R)
      ((AlgHom.comp (B := A ⊗[R] MvPolynomial σ R)
              (AlgHom.restrictScalars R
                (AlgHom.comp (aeval fun (s : σ) ↦ 1 ⊗ₜ[R] X s)
                    (Algebra.TensorProduct.lift (Algebra.ofId A (MvPolynomial σ A)) (mapAlgHom (Algebra.ofId R A)) ⋯) :
                  A ⊗[R] MvPolynomial σ R →ₐ[A] A ⊗[R] MvPolynomial σ R))
              Algebra.TensorProduct.includeRight :
            (a : MvPolynomial σ R) → A ⊗[R] MvPolynomial σ R)
          (X s) :
        A ⊗[R] MvPolynomial σ R)
      ((AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] MvPolynomial σ R)))
              Algebra.TensorProduct.includeRight :
            (a : MvPolynomial σ R) → A ⊗[R] MvPolynomial σ R)
          (X s) :
        A ⊗[R] MvPolynomial σ R)
⊢ Eq (α := A ⊗[R] MvPolynomial σ R →ₐ[A] A ⊗[R] MvPolynomial σ R)
    (AlgHom.comp (aeval fun (s : σ) ↦ 1 ⊗ₜ[R] X s)
        (Algebra.TensorProduct.lift (Algebra.ofId A (MvPolynomial σ A)) (mapAlgHom (Algebra.ofId R A)) ⋯) :
      A ⊗[R] MvPolynomial σ R →ₐ[A] A ⊗[R] MvPolynomial σ R)
    (AlgHom.id A (A ⊗[R] MvPolynomial σ R) : A ⊗[R] MvPolynomial σ R →ₐ[A] A ⊗[R] MvPolynomial σ R)

Tactic:
ext s
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
ι : Type u_2
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring N
inst_4 : Algebra R N
A : Type u_4
inst_5 : CommSemiring A
inst_6 : Algebra R A
s : σ
⊢ Eq (α := A ⊗[R] MvPolynomial σ R)
    ((AlgHom.comp (B := A ⊗[R] MvPolynomial σ R)
            (AlgHom.restrictScalars R
              (AlgHom.comp (aeval fun (s : σ) ↦ 1 ⊗ₜ[R] X s)
                  (Algebra.TensorProduct.lift (Algebra.ofId A (MvPolynomial σ A)) (mapAlgHom (Algebra.ofId R A)) ⋯) :
                A ⊗[R] MvPolynomial σ R →ₐ[A] A ⊗[R] MvPolynomial σ R))
            Algebra.TensorProduct.includeRight :
          (a : MvPolynomial σ R) → A ⊗[R] MvPolynomial σ R)
        (X s) :
      A ⊗[R] MvPolynomial σ R)
    ((AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id A (A ⊗[R] MvPolynomial σ R)))
            Algebra.TensorProduct.includeRight :
          (a : MvPolynomial σ R) → A ⊗[R] MvPolynomial σ R)
        (X s) :
      A ⊗[R] MvPolynomial σ R)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
a : A
p : MvPolynomial σ R
⊢ (algebraTensorAlgEquiv R A : (a : A ⊗[R] MvPolynomial σ R) → MvPolynomial σ A) (a ⊗ₜ[R] p) =
    HSMul.hSMul (β := MvPolynomial σ A) a
      ((map (algebraMap R A) : (a : MvPolynomial σ R) → MvPolynomial σ A) p : MvPolynomial σ A)

Tactic:
simp [algebraTensorAlgEquiv, Algebra.smul_def]

Premises used: MvPolynomial.algebraTensorAlgEquiv, Algebra.smul_def
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
s : σ
⊢ Eq (α := A ⊗[R] MvPolynomial σ R)
    ((AlgEquiv.symm (algebraTensorAlgEquiv R A) : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R) (X s) :
      A ⊗[R] MvPolynomial σ R)
    (1 ⊗ₜ[R] X s : A ⊗[R] MvPolynomial σ R)

Tactic:
simp [algebraTensorAlgEquiv]

Premises used: MvPolynomial.algebraTensorAlgEquiv
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
m : σ →₀ ℕ
a : A
zero :
  Eq (α := A ⊗[R] MvPolynomial σ R)
    ((AlgEquiv.symm (algebraTensorAlgEquiv R A) : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
        ((monomial 0 : (a : A) → MvPolynomial σ A) a) :
      A ⊗[R] MvPolynomial σ R)
    (a ⊗ₜ[R] (monomial 0 : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R)
single_add :
  ∀ (a_1 : σ) (b : ℕ) (f : σ →₀ ℕ),
    a_1 ∉ f.support →
      b ≠ 0 →
        Eq (α := A ⊗[R] MvPolynomial σ R)
            ((AlgEquiv.symm (algebraTensorAlgEquiv R A) : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
                ((monomial f : (a : A) → MvPolynomial σ A) a) :
              A ⊗[R] MvPolynomial σ R)
            (a ⊗ₜ[R] (monomial f : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R) →
          Eq (α := A ⊗[R] MvPolynomial σ R)
            ((AlgEquiv.symm (algebraTensorAlgEquiv R A) : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
                ((monomial (Finsupp.single a_1 b + f) : (a : A) → MvPolynomial σ A) a) :
              A ⊗[R] MvPolynomial σ R)
            (a ⊗ₜ[R] (monomial (Finsupp.single a_1 b + f) : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R)
⊢ Eq (α := A ⊗[R] MvPolynomial σ R)
    ((AlgEquiv.symm (algebraTensorAlgEquiv R A) : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
        ((monomial m : (a : A) → MvPolynomial σ A) a) :
      A ⊗[R] MvPolynomial σ R)
    (a ⊗ₜ[R] (monomial m : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R)

Tactic:
apply @Finsupp.induction σ ℕ _ _ m

Premises used: Finsupp.induction
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
m : σ →₀ ℕ
a : A
⊢ Eq (α := A ⊗[R] MvPolynomial σ R)
    ((AlgEquiv.symm (algebraTensorAlgEquiv R A) : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
        ((monomial 0 : (a : A) → MvPolynomial σ A) a) :
      A ⊗[R] MvPolynomial σ R)
    (a ⊗ₜ[R] (monomial 0 : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R)

Tactic:
simp [algebraTensorAlgEquiv]

Premises used: MvPolynomial.algebraTensorAlgEquiv
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
m : σ →₀ ℕ
a : A
i : σ
n : ℕ
f : σ →₀ ℕ
single_add :
  i ∉ f.support →
    n ≠ 0 →
      Eq (α := A ⊗[R] MvPolynomial σ R)
          ((AlgEquiv.symm (algebraTensorAlgEquiv R A) : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
              ((monomial f : (a : A) → MvPolynomial σ A) a) :
            A ⊗[R] MvPolynomial σ R)
          (a ⊗ₜ[R] (monomial f : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R) →
        Eq (α := A ⊗[R] MvPolynomial σ R)
          ((AlgEquiv.symm (algebraTensorAlgEquiv R A) : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
              ((monomial (Finsupp.single i n + f) : (a : A) → MvPolynomial σ A) a) :
            A ⊗[R] MvPolynomial σ R)
          (a ⊗ₜ[R] (monomial (Finsupp.single i n + f) : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R)
⊢ i ∉ f.support →
    n ≠ 0 →
      Eq (α := A ⊗[R] MvPolynomial σ R)
          ((AlgEquiv.symm (algebraTensorAlgEquiv R A) : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
              ((monomial f : (a : A) → MvPolynomial σ A) a) :
            A ⊗[R] MvPolynomial σ R)
          (a ⊗ₜ[R] (monomial f : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R) →
        Eq (α := A ⊗[R] MvPolynomial σ R)
          ((AlgEquiv.symm (algebraTensorAlgEquiv R A) : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
              ((monomial (Finsupp.single i n + f) : (a : A) → MvPolynomial σ A) a) :
            A ⊗[R] MvPolynomial σ R)
          (a ⊗ₜ[R] (monomial (Finsupp.single i n + f) : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R)

Tactic:
_
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
m : σ →₀ ℕ
a : A
i : σ
n : ℕ
f : σ →₀ ℕ
h : i ∉ f.support
single_add :
  n ≠ 0 →
    Eq (α := A ⊗[R] MvPolynomial σ R)
        ((AlgEquiv.symm (algebraTensorAlgEquiv R A) : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
            ((monomial f : (a : A) → MvPolynomial σ A) a) :
          A ⊗[R] MvPolynomial σ R)
        (a ⊗ₜ[R] (monomial f : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R) →
      Eq (α := A ⊗[R] MvPolynomial σ R)
        ((AlgEquiv.symm (algebraTensorAlgEquiv R A) : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
            ((monomial (Finsupp.single i n + f) : (a : A) → MvPolynomial σ A) a) :
          A ⊗[R] MvPolynomial σ R)
        (a ⊗ₜ[R] (monomial (Finsupp.single i n + f) : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R)
⊢ n ≠ 0 →
    Eq (α := A ⊗[R] MvPolynomial σ R)
        ((AlgEquiv.symm (algebraTensorAlgEquiv R A) : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
            ((monomial f : (a : A) → MvPolynomial σ A) a) :
          A ⊗[R] MvPolynomial σ R)
        (a ⊗ₜ[R] (monomial f : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R) →
      Eq (α := A ⊗[R] MvPolynomial σ R)
        ((AlgEquiv.symm (algebraTensorAlgEquiv R A) : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
            ((monomial (Finsupp.single i n + f) : (a : A) → MvPolynomial σ A) a) :
          A ⊗[R] MvPolynomial σ R)
        (a ⊗ₜ[R] (monomial (Finsupp.single i n + f) : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R)

Tactic:
_
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
m : σ →₀ ℕ
a : A
i : σ
n : ℕ
f : σ →₀ ℕ
h : i ∉ f.support
h_1 : n ≠ 0
hfa :
  Eq (α := A ⊗[R] MvPolynomial σ R)
    ((aeval fun (s : σ) ↦ 1 ⊗ₜ[R] X s : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
        ((monomial f : (a : A) → MvPolynomial σ A) a) :
      A ⊗[R] MvPolynomial σ R)
    (a ⊗ₜ[R] (monomial f : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R)
single_add :
  HMul.hMul (α := A ⊗[R] MvPolynomial σ R) (a ⊗ₜ[R] (monomial f : (a : R) → MvPolynomial σ R) 1)
      (1 ⊗ₜ[R] HPow.hPow (α := MvPolynomial σ R) (X i) n) =
    a ⊗ₜ[R] ((monomial f : (a : R) → MvPolynomial σ R) 1 * HPow.hPow (α := MvPolynomial σ R) (X i) n)
⊢ Eq (α := A ⊗[R] MvPolynomial σ R)
    ((aeval fun (s : σ) ↦ 1 ⊗ₜ[R] X s : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
        ((monomial (Finsupp.single i n + f) : (a : A) → MvPolynomial σ A) a) :
      A ⊗[R] MvPolynomial σ R)
    (a ⊗ₜ[R] (monomial (Finsupp.single i n + f) : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R)

Tactic:
simp only [add_comm, monomial_add_single, map_mul, map_pow, aeval_X,
      Algebra.TensorProduct.tmul_pow, one_pow, hfa]

Premises used: one_pow, MvPolynomial.aeval_X, map_pow, MvPolynomial.monomial_add_single, add_comm, map_mul, Algebra.TensorProduct.tmul_pow
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
m : σ →₀ ℕ
a : A
i : σ
n : ℕ
f : σ →₀ ℕ
h : i ∉ f.support
h_1 : n ≠ 0
hfa :
  Eq (α := A ⊗[R] MvPolynomial σ R)
    ((aeval fun (s : σ) ↦ 1 ⊗ₜ[R] X s : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
        ((monomial f : (a : A) → MvPolynomial σ A) a) :
      A ⊗[R] MvPolynomial σ R)
    (a ⊗ₜ[R] (monomial f : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R)
single_add :
  HMul.hMul (α := A ⊗[R] MvPolynomial σ R) (a ⊗ₜ[R] (monomial f : (a : R) → MvPolynomial σ R) 1)
      (1 ⊗ₜ[R] HPow.hPow (α := MvPolynomial σ R) (X i) n) =
    (a * 1) ⊗ₜ[R] ((monomial f : (a : R) → MvPolynomial σ R) 1 * HPow.hPow (α := MvPolynomial σ R) (X i) n)
⊢ HMul.hMul (α := A ⊗[R] MvPolynomial σ R) (a ⊗ₜ[R] (monomial f : (a : R) → MvPolynomial σ R) 1)
      (1 ⊗ₜ[R] HPow.hPow (α := MvPolynomial σ R) (X i) n) =
    a ⊗ₜ[R] ((monomial f : (a : R) → MvPolynomial σ R) 1 * HPow.hPow (α := MvPolynomial σ R) (X i) n)

Tactic:
nth_rw 2 [← mul_one a]

Premises used: mul_one
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
m : σ →₀ ℕ
a : A
i : σ
n : ℕ
f : σ →₀ ℕ
h : i ∉ f.support
h_1 : n ≠ 0
hfa :
  Eq (α := A ⊗[R] MvPolynomial σ R)
    ((aeval fun (s : σ) ↦ 1 ⊗ₜ[R] X s : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
        ((monomial f : (a : A) → MvPolynomial σ A) a) :
      A ⊗[R] MvPolynomial σ R)
    (a ⊗ₜ[R] (monomial f : (a : R) → MvPolynomial σ R) 1 : A ⊗[R] MvPolynomial σ R)
single_add single_add₁ :
  Eq (α := A ⊗[R] MvPolynomial σ R)
    ((a * 1) ⊗ₜ[R] ((monomial f : (a : R) → MvPolynomial σ R) 1 * HPow.hPow (α := MvPolynomial σ R) (X i) n))
    ((a * 1) ⊗ₜ[R] ((monomial f : (a : R) → MvPolynomial σ R) 1 * HPow.hPow (α := MvPolynomial σ R) (X i) n))
⊢ HMul.hMul (α := A ⊗[R] MvPolynomial σ R) (a ⊗ₜ[R] (monomial f : (a : R) → MvPolynomial σ R) 1)
      (1 ⊗ₜ[R] HPow.hPow (α := MvPolynomial σ R) (X i) n) =
    (a * 1) ⊗ₜ[R] ((monomial f : (a : R) → MvPolynomial σ R) 1 * HPow.hPow (α := MvPolynomial σ R) (X i) n)

Tactic:
rw [Algebra.TensorProduct.tmul_mul_tmul]

Premises used: Algebra.TensorProduct.tmul_mul_tmul
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
hf :
  ∀ (i : σ),
    Eq (α := A ⊗[R] MvPolynomial σ R)
      ((AlgHom.comp
              (AlgHom.restrictScalars R
                (↑(AlgEquiv.symm (algebraTensorAlgEquiv R A)) : MvPolynomial σ A →ₐ[A] A ⊗[R] MvPolynomial σ R))
              (mapAlgHom (Algebra.ofId R A)) :
            (a : MvPolynomial σ R) → A ⊗[R] MvPolynomial σ R)
          (X i) :
        A ⊗[R] MvPolynomial σ R)
      ((Algebra.TensorProduct.includeRight : (a : MvPolynomial σ R) → A ⊗[R] MvPolynomial σ R) (X i) :
        A ⊗[R] MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R →ₐ[R] A ⊗[R] MvPolynomial σ R)
    (AlgHom.comp
      (AlgHom.restrictScalars R
        (↑(AlgEquiv.symm (algebraTensorAlgEquiv R A)) : MvPolynomial σ A →ₐ[A] A ⊗[R] MvPolynomial σ R))
      (mapAlgHom (Algebra.ofId R A)))
    Algebra.TensorProduct.includeRight

Tactic:
ext
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
i : σ
⊢ Eq (α := A ⊗[R] MvPolynomial σ R)
    ((AlgHom.comp
            (AlgHom.restrictScalars R
              (↑(AlgEquiv.symm (algebraTensorAlgEquiv R A)) : MvPolynomial σ A →ₐ[A] A ⊗[R] MvPolynomial σ R))
            (mapAlgHom (Algebra.ofId R A)) :
          (a : MvPolynomial σ R) → A ⊗[R] MvPolynomial σ R)
        (X i) :
      A ⊗[R] MvPolynomial σ R)
    ((Algebra.TensorProduct.includeRight : (a : MvPolynomial σ R) → A ⊗[R] MvPolynomial σ R) (X i) :
      A ⊗[R] MvPolynomial σ R)

Tactic:
simp
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
A : Type u_4
inst_1 : CommSemiring A
inst_2 : Algebra R A
x : MvPolynomial σ R
⊢ Eq (α := A ⊗[R] MvPolynomial σ R)
    ((AlgEquiv.symm (algebraTensorAlgEquiv R A) : (a : MvPolynomial σ A) → A ⊗[R] MvPolynomial σ R)
        ((map (algebraMap R A) : (a : MvPolynomial σ R) → MvPolynomial σ A) x) :
      A ⊗[R] MvPolynomial σ R)
    (1 ⊗ₜ[R] x : A ⊗[R] MvPolynomial σ R)

Tactic:
DFunLike.congr_fun (algebraTensorAlgEquiv_symm_comp_aeval R A) x

Premises used: Multiset.sum, Multiset.foldr, DFunLike.congr_fun, Finsupp.sum, MvPolynomial.eval₂, MvPolynomial.algebraTensorAlgEquiv_symm_comp_aeval, TensorProduct.tmul, AddCon.toQuotient, Finset.sum
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring N
inst_4 : Algebra R N
f : σ → S
a : R
C :
  Eq (α := N ⊗[R] S) ((algebraMap R N : (a : R) → N) a ⊗ₜ[R] 1 : N ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : N ⊗[R] S)
⊢ Eq (α := N ⊗[R] S)
    ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S)
        ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a) :
      N ⊗[R] S)
    (1 ⊗ₜ[R]
        (aeval f : (a : MvPolynomial σ R) → S) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) :
      N ⊗[R] S)

Tactic:
simp only [algHom_C, Algebra.TensorProduct.algebraMap_apply]

Premises used: Algebra.TensorProduct.algebraMap_apply, MvPolynomial.algHom_C
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring N
inst_4 : Algebra R N
f : σ → S
a : R
C :
  Eq (α := N ⊗[R] S) (HMul.hMul (α := N) (β := N) ((algebraMap R N : (a : R) → N) a : N) (1 : N) ⊗ₜ[R] 1 : N ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : N ⊗[R] S)
C₁ :
  Eq (α := N ⊗[R] S) (HSMul.hSMul (β := N) a 1 ⊗ₜ[R] 1 : N ⊗[R] S) (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : N ⊗[R] S)
C₂ : Eq (α := N ⊗[R] S) (1 ⊗ₜ[R] HSMul.hSMul (β := S) a 1) (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a)
C₃ :
  Eq (α := N ⊗[R] S) (1 ⊗ₜ[R] HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) a : S) (1 : S))
    (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a)
C₄ C₅ :
  Eq (α := N ⊗[R] S) (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : N ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : N ⊗[R] S)
⊢ Eq (α := N ⊗[R] S) ((algebraMap R N : (a : R) → N) a ⊗ₜ[R] 1 : N ⊗[R] S)
    (1 ⊗ₜ[R] (algebraMap R S : (a : R) → S) a : N ⊗[R] S)

Tactic:
rw [← mul_one ((algebraMap R N) a), ← Algebra.smul_def, smul_tmul, Algebra.smul_def, mul_one]

Premises used: TensorProduct.smul_tmul, Algebra.algebraMap, Algebra.smul_def, mul_one, DFunLike.coe
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring N
inst_4 : Algebra R N
f : σ → S
p q : MvPolynomial σ R
hp :
  Eq (α := N ⊗[R] S) ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) p : N ⊗[R] S)
    (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) p : N ⊗[R] S)
hq :
  Eq (α := N ⊗[R] S) ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) q : N ⊗[R] S)
    (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) q : N ⊗[R] S)
⊢ Eq (α := N ⊗[R] S) ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) (p + q) : N ⊗[R] S)
    (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) (p + q) : N ⊗[R] S)

Tactic:
simp [hp, hq, tmul_add]

Premises used: TensorProduct.tmul_add
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring N
inst_4 : Algebra R N
f : σ → S
p : MvPolynomial σ R
i : σ
h :
  Eq (α := N ⊗[R] S) ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) p : N ⊗[R] S)
    (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) p : N ⊗[R] S)
⊢ Eq (α := N ⊗[R] S) ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) (p * X i) : N ⊗[R] S)
    (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) (p * X i) : N ⊗[R] S)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : CommSemiring N
inst_4 : Algebra R N
f : σ → S
p : MvPolynomial σ R
C :
  ∀ (a : R),
    Eq (α := N ⊗[R] S)
      ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S)
          ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a) :
        N ⊗[R] S)
      (1 ⊗ₜ[R]
          (aeval f : (a : MvPolynomial σ R) → S) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) :
        N ⊗[R] S)
add :
  ∀ (p q : MvPolynomial σ R)
    (hp :
      Eq (α := N ⊗[R] S) ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) p : N ⊗[R] S)
        (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) p : N ⊗[R] S))
    (hq :
      Eq (α := N ⊗[R] S) ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) q : N ⊗[R] S)
        (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) q : N ⊗[R] S)),
    Eq (α := N ⊗[R] S) ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) (p + q) : N ⊗[R] S)
      (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) (p + q) : N ⊗[R] S)
mul_X :
  ∀ (p : MvPolynomial σ R) (i : σ)
    (h :
      Eq (α := N ⊗[R] S) ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) p : N ⊗[R] S)
        (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) p : N ⊗[R] S)),
    Eq (α := N ⊗[R] S) ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) (p * X i) : N ⊗[R] S)
      (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) (p * X i) : N ⊗[R] S)
⊢ Eq (α := N ⊗[R] S) ((aeval fun (x : σ) ↦ 1 ⊗ₜ[R] f x : (a : MvPolynomial σ R) → N ⊗[R] S) p : N ⊗[R] S)
    (1 ⊗ₜ[R] (aeval f : (a : MvPolynomial σ R) → S) p : N ⊗[R] S)

Tactic:
induction p using MvPolynomial.induction_on with
  | C a =>
    simp only [algHom_C, Algebra.TensorProduct.algebraMap_apply]
    rw [← mul_one ((algebraMap R N) a), ← Algebra.smul_def, smul_tmul, Algebra.smul_def, mul_one]
  | add p q hp hq => simp [hp, hq, tmul_add]
  | mul_X p i h => simp [h]

Premises used: TensorProduct.smul_tmul, Algebra.TensorProduct.algebraMap_apply, MvPolynomial.induction_on, MvPolynomial.algHom_C, TensorProduct.tmul_add, Algebra.smul_def, mul_one, Submodule.add, MvPolynomial.C
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
ι : Type u_2
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
i : σ
⊢ Eq (α := MvPolynomial (σ ⊕ ι) S)
    ((tensorEquivSum R σ ι S : (a : MvPolynomial σ S ⊗[R] MvPolynomial ι R) → MvPolynomial (σ ⊕ ι) S) (X i ⊗ₜ[R] 1) :
      MvPolynomial (σ ⊕ ι) S)
    (X (Sum.inl i) : MvPolynomial (σ ⊕ ι) S)

Tactic:
simp [tensorEquivSum]

Premises used: MvPolynomial.tensorEquivSum
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
ι : Type u_2
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : S
⊢ Eq (α := MvPolynomial (σ ⊕ ι) S)
    ((tensorEquivSum R σ ι S : (a : MvPolynomial σ S ⊗[R] MvPolynomial ι R) → MvPolynomial (σ ⊕ ι) S)
        ((C : (a : S) → MvPolynomial σ S) r ⊗ₜ[R] 1) :
      MvPolynomial (σ ⊕ ι) S)
    ((C : (a : S) → MvPolynomial (σ ⊕ ι) S) r : MvPolynomial (σ ⊕ ι) S)

Tactic:
simp [tensorEquivSum]

Premises used: MvPolynomial.tensorEquivSum
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
ι : Type u_2
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
i : ι
⊢ Eq (α := MvPolynomial (σ ⊕ ι) S)
    ((tensorEquivSum R σ ι S : (a : MvPolynomial σ S ⊗[R] MvPolynomial ι R) → MvPolynomial (σ ⊕ ι) S) (1 ⊗ₜ[R] X i) :
      MvPolynomial (σ ⊕ ι) S)
    (X (Sum.inr i) : MvPolynomial (σ ⊕ ι) S)

Tactic:
simp [tensorEquivSum]

Premises used: MvPolynomial.tensorEquivSum
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
ι : Type u_2
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
⊢ Eq (α := MvPolynomial (σ ⊕ ι) S)
    ((tensorEquivSum R σ ι S : (a : MvPolynomial σ S ⊗[R] MvPolynomial ι R) → MvPolynomial (σ ⊕ ι) S)
        (1 ⊗ₜ[R] (C : (a : R) → MvPolynomial ι R) r) :
      MvPolynomial (σ ⊕ ι) S)
    ((C : (a : S) → MvPolynomial (σ ⊕ ι) S) ((algebraMap R S : (a : R) → S) r) : MvPolynomial (σ ⊕ ι) S)

Tactic:
simp [tensorEquivSum]

Premises used: MvPolynomial.tensorEquivSum
-- Module: Mathlib.RingTheory.TensorProduct.MvPolynomial
Goal:
R : Type u
inst : CommSemiring R
σ : Type u_1
ι : Type u_2
S : Type u_3
inst_1 : CommSemiring S
inst_2 : Algebra R S
r : R
s : S
⊢ Eq (α := MvPolynomial (σ ⊕ ι) S)
    ((tensorEquivSum R σ ι S : (a : MvPolynomial σ S ⊗[R] MvPolynomial ι R) → MvPolynomial (σ ⊕ ι) S)
        ((C : (a : S) → MvPolynomial σ S) s ⊗ₜ[R] (C : (a : R) → MvPolynomial ι R) r) :
      MvPolynomial (σ ⊕ ι) S)
    ((C : (a : S) → MvPolynomial (σ ⊕ ι) S) (r • s) : MvPolynomial (σ ⊕ ι) S)

Tactic:
simp [tensorEquivSum, mul_comm (C s)]

Premises used: MvPolynomial.tensorEquivSum, mul_comm, MvPolynomial.C, DFunLike.coe