awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
inst_1 : DecidableEq σ
inst_2 : AddCommMonoid N
inst_3 : Module R N
e : σ →₀ ℕ
r : R
n : N
d : σ →₀ ℕ
rw :
  HSMul.hSMul.{u, v, v} (α := R) (coeff d ((monomial e : (a : R) → MvPolynomial σ R) r)) n = if e = d then r • n else 0
rw₁ : (if e = d then r else 0) • n = if e = d then r • n else 0
rw₂ : (if e = d then r • n else HSMul.hSMul.{u, v, v} (α := R) 0 n) = if e = d then r • n else 0
⊢ (((scalarRTensor : (a : MvPolynomial σ R ⊗[R] N) → (σ →₀ ℕ) →₀ N)
            ((monomial e : (a : R) → MvPolynomial σ R) r ⊗ₜ[R] n) :
          Finsupp.{u_1, v} (σ →₀ ℕ) N) :
        (a : σ →₀ ℕ) → N)
      d =
    if e = d then r • n else 0
have rw₃ : (if e = d then r • n else 0) = if e = d then r • n else 0
Tactic: rw [scalarRTensor_apply_tmul_apply, coeff_monomial, ite_smul, zero_smul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
inst_1 : DecidableEq σ
inst_2 : AddCommMonoid N
inst_3 : Module R N
s : σ
n : N
d : σ →₀ ℕ
⊢ (((scalarRTensor : (a : MvPolynomial σ R ⊗[R] N) → (σ →₀ ℕ) →₀ N) (X s ⊗ₜ[R] n) : Finsupp.{u_1, v} (σ →₀ ℕ) N) :
        (a : σ →₀ ℕ) → N)
      d =
    if Finsupp.single s 1 = d then n else 0
have rw : HSMul.hSMul.{u, v, v} (α := R) (coeff d (X s)) n = if Finsupp.single s 1 = d then n else 0
Tactic: rw [scalarRTensor_apply_tmul_apply, coeff_X', ite_smul, one_smul, zero_smul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
inst_1 : DecidableEq σ
inst_2 : AddCommMonoid N
inst_3 : Module R N
s : σ
n : N
d : σ →₀ ℕ
rw : HSMul.hSMul.{u, v, v} (α := R) (coeff d (X s)) n = if Finsupp.single s 1 = d then n else 0
⊢ (((scalarRTensor : (a : MvPolynomial σ R ⊗[R] N) → (σ →₀ ℕ) →₀ N) (X s ⊗ₜ[R] n) : Finsupp.{u_1, v} (σ →₀ ℕ) N) :
        (a : σ →₀ ℕ) → N)
      d =
    if Finsupp.single s 1 = d then n else 0
have rw₁ : HSMul.hSMul.{u, v, v} (α := R) (if Finsupp.single s 1 = d then 1 else 0) n = if Finsupp.single s 1 = d then n else 0
Tactic: rw [scalarRTensor_apply_tmul_apply, coeff_X', ite_smul, one_smul, zero_smul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
inst_1 : DecidableEq σ
inst_2 : AddCommMonoid N
inst_3 : Module R N
s : σ
n : N
d : σ →₀ ℕ
rw : HSMul.hSMul.{u, v, v} (α := R) (coeff d (X s)) n = if Finsupp.single s 1 = d then n else 0
rw₁ :
  HSMul.hSMul.{u, v, v} (α := R) (if Finsupp.single s 1 = d then 1 else 0) n = if Finsupp.single s 1 = d then n else 0
⊢ (((scalarRTensor : (a : MvPolynomial σ R ⊗[R] N) → (σ →₀ ℕ) →₀ N) (X s ⊗ₜ[R] n) : Finsupp.{u_1, v} (σ →₀ ℕ) N) :
        (a : σ →₀ ℕ) → N)
      d =
    if Finsupp.single s 1 = d then n else 0
have rw₂ : (if Finsupp.single s 1 = d then HSMul.hSMul.{u, v, v} (α := R) 1 n else HSMul.hSMul.{u, v, v} (α := R) 0 n) =
  if Finsupp.single s 1 = d then n else 0
Tactic: rw [scalarRTensor_apply_tmul_apply, coeff_X', ite_smul, one_smul, zero_smul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
inst_1 : DecidableEq σ
inst_2 : AddCommMonoid N
inst_3 : Module R N
s : σ
n : N
d : σ →₀ ℕ
rw : HSMul.hSMul.{u, v, v} (α := R) (coeff d (X s)) n = if Finsupp.single s 1 = d then n else 0
rw₁ :
  HSMul.hSMul.{u, v, v} (α := R) (if Finsupp.single s 1 = d then 1 else 0) n = if Finsupp.single s 1 = d then n else 0
rw₂ :
  (if Finsupp.single s 1 = d then HSMul.hSMul.{u, v, v} (α := R) 1 n else HSMul.hSMul.{u, v, v} (α := R) 0 n) =
    if Finsupp.single s 1 = d then n else 0
⊢ (((scalarRTensor : (a : MvPolynomial σ R ⊗[R] N) → (σ →₀ ℕ) →₀ N) (X s ⊗ₜ[R] n) : Finsupp.{u_1, v} (σ →₀ ℕ) N) :
        (a : σ →₀ ℕ) → N)
      d =
    if Finsupp.single s 1 = d then n else 0
have rw₃ : (if Finsupp.single s 1 = d then n else HSMul.hSMul.{u, v, v} (α := R) 0 n) = if Finsupp.single s 1 = d then n else 0
Tactic: rw [scalarRTensor_apply_tmul_apply, coeff_X', ite_smul, one_smul, zero_smul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
Goal:
R : Type u
N : Type v
inst : CommSemiring R
σ : Type u_1
inst_1 : DecidableEq σ
inst_2 : AddCommMonoid N
inst_3 : Module R N
s : σ
n : N
d : σ →₀ ℕ
rw : HSMul.hSMul.{u, v, v} (α := R) (coeff d (X s)) n = if Finsupp.single s 1 = d then n else 0
rw₁ :
  HSMul.hSMul.{u, v, v} (α := R) (if Finsupp.single s 1 = d then 1 else 0) n = if Finsupp.single s 1 = d then n else 0
rw₂ :
  (if Finsupp.single s 1 = d then HSMul.hSMul.{u, v, v} (α := R) 1 n else HSMul.hSMul.{u, v, v} (α := R) 0 n) =
    if Finsupp.single s 1 = d then n else 0
rw₃ :
  (if Finsupp.single s 1 = d then n else HSMul.hSMul.{u, v, v} (α := R) 0 n) = if Finsupp.single s 1 = d then n else 0
⊢ (((scalarRTensor : (a : MvPolynomial σ R ⊗[R] N) → (σ →₀ ℕ) →₀ N) (X s ⊗ₜ[R] n) : Finsupp.{u_1, v} (σ →₀ ℕ) N) :
        (a : σ →₀ ℕ) → N)
      d =
    if Finsupp.single s 1 = d then n else 0
have rw₄ : (if Finsupp.single s 1 = d then n else 0) = if Finsupp.single s 1 = d then n else 0
Tactic: rw [scalarRTensor_apply_tmul_apply, coeff_X', ite_smul, one_smul, zero_smul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
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
p : MvPolynomial σ S
n : N
d : σ →₀ ℕ
⊢ Eq (α := S ⊗[R] N) (coeff d ((rTensorAlgHom : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) (p ⊗ₜ[R] n)))
    (coeff d p ⊗ₜ[R] n)
have rw : coeff d
    (HMul.hMul (α := MvPolynomial σ (S ⊗[R] N)) (β := MvPolynomial σ (S ⊗[R] N))
      ((mapAlgHom Algebra.TensorProduct.includeLeft : (a : MvPolynomial σ S) → MvPolynomial σ (S ⊗[R] N)) p :
        MvPolynomial σ (S ⊗[R] N))
      ((AlgHom.comp (B := S ⊗[R] N) (IsScalarTower.toAlgHom R (S ⊗[R] N) (MvPolynomial σ (S ⊗[R] N)))
              Algebra.TensorProduct.includeRight :
            (a : N) → MvPolynomial σ (S ⊗[R] N))
          n :
        MvPolynomial σ (S ⊗[R] N))) =
  coeff d p ⊗ₜ[R] n
Tactic: rw [rTensorAlgHom, Algebra.TensorProduct.lift_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
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
p : MvPolynomial σ S
n : N
d : σ →₀ ℕ
⊢ coeff d
      (HMul.hMul (α := MvPolynomial σ (S ⊗[R] N)) (β := MvPolynomial σ (S ⊗[R] N))
        ((mapAlgHom Algebra.TensorProduct.includeLeft : (a : MvPolynomial σ S) → MvPolynomial σ (S ⊗[R] N)) p :
          MvPolynomial σ (S ⊗[R] N))
        ((algebraMap (S ⊗[R] N) (MvPolynomial σ (S ⊗[R] N)) : (a : S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) (1 ⊗ₜ[R] n) :
          MvPolynomial σ (S ⊗[R] N))) =
    coeff d p ⊗ₜ[R] n
have rw : HMul.hMul (α := S ⊗[R] N) (1 ⊗ₜ[R] n)
    (coeff d ((mapAlgHom Algebra.TensorProduct.includeLeft : (a : MvPolynomial σ S) → MvPolynomial σ (S ⊗[R] N)) p)) =
  coeff d p ⊗ₜ[R] n
Tactic: rw [algebraMap_eq, mul_comm, coeff_C_mul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
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
inst_5 : DecidableEq σ
⊢ Eq (α := MvPolynomial σ S ⊗[R] N →ₗ[S] MvPolynomial σ (S ⊗[R] N)) (AlgHom.toLinearMap rTensorAlgHom)
    (↑rTensor : MvPolynomial σ S ⊗[R] N →ₗ[S] (σ →₀ ℕ) →₀ S ⊗[R] N)
have a : ∀ (d : σ →₀ ℕ) (n : N) (e : σ →₀ ℕ),
  Eq (α := S ⊗[R] N)
    (coeff e
      ((((AlgebraTensorModule.curry (AlgHom.toLinearMap rTensorAlgHom) ∘ₗ AddMonoidAlgebra.lsingle d :
                S →ₗ[S] N →ₗ[R] MvPolynomial σ (S ⊗[R] N)) :
              (a : S) → N →ₗ[R] MvPolynomial σ (S ⊗[R] N))
            1 :
          (a : N) → MvPolynomial σ (S ⊗[R] N))
        n))
    (coeff e
      ((((AlgebraTensorModule.curry (↑rTensor : MvPolynomial σ S ⊗[R] N →ₗ[S] (σ →₀ ℕ) →₀ S ⊗[R] N) ∘ₗ
                  AddMonoidAlgebra.lsingle d :
                S →ₗ[S] N →ₗ[R] MvPolynomial σ (S ⊗[R] N)) :
              (a : S) → N →ₗ[R] MvPolynomial σ (S ⊗[R] N))
            1 :
          (a : N) → MvPolynomial σ (S ⊗[R] N))
        n))
Tactic: ext d n e
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
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
inst_5 : DecidableEq σ
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ Eq (α := S ⊗[R] N)
    (coeff e
      ((((AlgebraTensorModule.curry (AlgHom.toLinearMap rTensorAlgHom) ∘ₗ AddMonoidAlgebra.lsingle d :
                S →ₗ[S] N →ₗ[R] MvPolynomial σ (S ⊗[R] N)) :
              (a : S) → N →ₗ[R] MvPolynomial σ (S ⊗[R] N))
            1 :
          (a : N) → MvPolynomial σ (S ⊗[R] N))
        n))
    (coeff e
      ((((AlgebraTensorModule.curry (↑rTensor : MvPolynomial σ S ⊗[R] N →ₗ[S] (σ →₀ ℕ) →₀ S ⊗[R] N) ∘ₗ
                  AddMonoidAlgebra.lsingle d :
                S →ₗ[S] N →ₗ[R] MvPolynomial σ (S ⊗[R] N)) :
              (a : S) → N →ₗ[R] MvPolynomial σ (S ⊗[R] N))
            1 :
          (a : N) → MvPolynomial σ (S ⊗[R] N))
        n))
have a : Eq (α := S ⊗[R] N)
  (coeff e
    ((rTensorAlgHom : (a : AddMonoidAlgebra S (σ →₀ ℕ) ⊗[R] N) → MvPolynomial σ (S ⊗[R] N))
      ((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1 ⊗ₜ[R] n)))
  (coeff e
    (((↑rTensor : MvPolynomial σ S ⊗[R] N →ₗ[S] (σ →₀ ℕ) →₀ S ⊗[R] N) :
        (a : AddMonoidAlgebra S (σ →₀ ℕ) ⊗[R] N) → MvPolynomial σ (S ⊗[R] N))
      ((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1 ⊗ₜ[R] n)))
Tactic: simp only [coe_comp, Function.comp_apply, AlgebraTensorModule.curry_apply, curry_apply,
    LinearMap.coe_restrictScalars, AlgHom.toLinearMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
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
inst_5 : DecidableEq σ
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ Eq (α := S ⊗[R] N)
    (coeff e
      ((rTensorAlgHom : (a : AddMonoidAlgebra S (σ →₀ ℕ) ⊗[R] N) → MvPolynomial σ (S ⊗[R] N))
        ((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1 ⊗ₜ[R] n)))
    (coeff e
      (((↑rTensor : MvPolynomial σ S ⊗[R] N →ₗ[S] (σ →₀ ℕ) →₀ S ⊗[R] N) :
          (a : AddMonoidAlgebra S (σ →₀ ℕ) ⊗[R] N) → MvPolynomial σ (S ⊗[R] N))
        ((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1 ⊗ₜ[R] n)))
have a : Eq (α := S ⊗[R] N) (coeff e ((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1) ⊗ₜ[R] n)
  (coeff e
    (((↑rTensor : MvPolynomial σ S ⊗[R] N →ₗ[S] (σ →₀ ℕ) →₀ S ⊗[R] N) :
        (a : AddMonoidAlgebra S (σ →₀ ℕ) ⊗[R] N) → MvPolynomial σ (S ⊗[R] N))
      ((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1 ⊗ₜ[R] n)))
Tactic: rw [coeff_rTensorAlgHom_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
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
inst_5 : DecidableEq σ
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ Eq (α := S ⊗[R] N) (coeff e ((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1) ⊗ₜ[R] n)
    (coeff e
      (((↑rTensor : MvPolynomial σ S ⊗[R] N →ₗ[S] (σ →₀ ℕ) →₀ S ⊗[R] N) :
          (a : AddMonoidAlgebra S (σ →₀ ℕ) ⊗[R] N) → MvPolynomial σ (S ⊗[R] N))
        ((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1 ⊗ₜ[R] n)))
have a : Eq (α := S ⊗[R] N)
  (((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1 : (a : σ →₀ ℕ) → S) e ⊗ₜ[R] n : S ⊗[R] N)
  (((((↑rTensor : MvPolynomial σ S ⊗[R] N →ₗ[S] (σ →₀ ℕ) →₀ S ⊗[R] N) :
              (a : AddMonoidAlgebra S (σ →₀ ℕ) ⊗[R] N) → MvPolynomial σ (S ⊗[R] N))
            ((AddMonoidAlgebra.lsingle d : (a : S) → AddMonoidAlgebra S (σ →₀ ℕ)) 1 ⊗ₜ[R] n) :
          MvPolynomial σ (S ⊗[R] N)) :
        (a : σ →₀ ℕ) → S ⊗[R] N)
      e :
    S ⊗[R] N)
Tactic: simp only [coeff]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
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
inst_5 : DecidableEq σ
p : MvPolynomial σ S ⊗[R] N
⊢ Eq (α := MvPolynomial σ (S ⊗[R] N))
    ((rTensorAlgHom : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) p : MvPolynomial σ (S ⊗[R] N))
    ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → (σ →₀ ℕ) →₀ S ⊗[R] N) p : (σ →₀ ℕ) →₀ S ⊗[R] N)
have rw : Eq (α := MvPolynomial σ (S ⊗[R] N))
  (((↑rTensor : MvPolynomial σ S ⊗[R] N →ₗ[S] (σ →₀ ℕ) →₀ S ⊗[R] N) :
        (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N))
      p :
    MvPolynomial σ (S ⊗[R] N))
  ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → (σ →₀ ℕ) →₀ S ⊗[R] N) p : (σ →₀ ℕ) →₀ S ⊗[R] N)
Tactic: rw [← AlgHom.toLinearMap_apply, rTensorAlgHom_toLinearMap]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
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
inst_5 : DecidableEq σ
⊢ MvPolynomial σ S ⊗[R] N ≃ₐ[S] MvPolynomial σ (S ⊗[R] N)
have map_one : Eq (α := MvPolynomial σ (S ⊗[R] N)) ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) 1) 1
Tactic: apply AlgEquiv.ofLinearEquiv rTensor
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
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
inst_5 : DecidableEq σ
map_one :
  Eq (α := MvPolynomial σ (S ⊗[R] N)) ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) 1) 1
⊢ MvPolynomial σ S ⊗[R] N ≃ₐ[S] MvPolynomial σ (S ⊗[R] N)
have map_mul : ∀ (x y : MvPolynomial σ S ⊗[R] N),
  (rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) (x * y) =
    HMul.hMul (α := MvPolynomial σ (S ⊗[R] N)) (β := MvPolynomial σ (S ⊗[R] N))
      ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) x : MvPolynomial σ (S ⊗[R] N))
      ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) y : MvPolynomial σ (S ⊗[R] N))
Tactic: apply AlgEquiv.ofLinearEquiv rTensor
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
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
inst_5 : DecidableEq σ
⊢ Eq (α := MvPolynomial σ (S ⊗[R] N))
    ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) (1 ⊗ₜ[R] 1) : MvPolynomial σ (S ⊗[R] N))
    (1 : MvPolynomial σ (S ⊗[R] N))
have map_one : Eq (α := MvPolynomial σ (S ⊗[R] N)) (1 : MvPolynomial σ (S ⊗[R] N))
  ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) (1 ⊗ₜ[R] 1) : MvPolynomial σ (S ⊗[R] N))
Tactic: apply symm
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
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
inst_5 : DecidableEq σ
⊢ Eq (α := MvPolynomial σ (S ⊗[R] N)) (1 : MvPolynomial σ (S ⊗[R] N))
    ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) (1 ⊗ₜ[R] 1) : MvPolynomial σ (S ⊗[R] N))
have map_one : Eq (α := MvPolynomial σ S ⊗[R] N)
  ((LinearEquiv.symm rTensor : (a : MvPolynomial σ (S ⊗[R] N)) → MvPolynomial σ S ⊗[R] N) 1) (1 ⊗ₜ[R] 1)
Tactic: rw [← LinearEquiv.symm_apply_eq]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
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
inst_5 : DecidableEq σ
x y : MvPolynomial σ S ⊗[R] N
⊢ (rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) (x * y) =
    HMul.hMul (α := MvPolynomial σ (S ⊗[R] N)) (β := MvPolynomial σ (S ⊗[R] N))
      ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) x : MvPolynomial σ (S ⊗[R] N))
      ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) y : MvPolynomial σ (S ⊗[R] N))
have map_mul : (rTensorAlgHom : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) (x * y) =
  HMul.hMul (α := MvPolynomial σ (S ⊗[R] N)) (β := MvPolynomial σ (S ⊗[R] N))
    ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) x : MvPolynomial σ (S ⊗[R] N))
    ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) y : MvPolynomial σ (S ⊗[R] N))
Tactic: erw [← rTensorAlgHom_apply_eq (S := S)]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
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
inst_5 : DecidableEq σ
x y : MvPolynomial σ S ⊗[R] N
⊢ (rTensorAlgHom : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) (x * y) =
    HMul.hMul (α := MvPolynomial σ (S ⊗[R] N)) (β := MvPolynomial σ (S ⊗[R] N))
      ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) x : MvPolynomial σ (S ⊗[R] N))
      ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) y : MvPolynomial σ (S ⊗[R] N))
have map_mul : HMul.hMul (α := MvPolynomial σ (S ⊗[R] N)) (β := MvPolynomial σ (S ⊗[R] N))
    ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → (σ →₀ ℕ) →₀ S ⊗[R] N) x : (σ →₀ ℕ) →₀ S ⊗[R] N)
    ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → (σ →₀ ℕ) →₀ S ⊗[R] N) y : (σ →₀ ℕ) →₀ S ⊗[R] N) =
  HMul.hMul (α := MvPolynomial σ (S ⊗[R] N)) (β := MvPolynomial σ (S ⊗[R] N))
    ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) x : MvPolynomial σ (S ⊗[R] N))
    ((rTensor : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) y : MvPolynomial σ (S ⊗[R] N))
Tactic: simp only [map_mul, rTensorAlgHom_apply_eq]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
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
inst_5 : DecidableEq σ
x : MvPolynomial σ S ⊗[R] N
⊢ Eq (α := MvPolynomial σ (S ⊗[R] N))
    (((↑rTensorAlgEquiv : MvPolynomial σ S ⊗[R] N →ₐ[S] MvPolynomial σ (S ⊗[R] N)) :
          (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N))
        x :
      MvPolynomial σ (S ⊗[R] N))
    ((rTensorAlgHom : (a : MvPolynomial σ S ⊗[R] N) → MvPolynomial σ (S ⊗[R] N)) x : MvPolynomial σ (S ⊗[R] N))
have e_a : (↑rTensorAlgEquiv : MvPolynomial σ S ⊗[R] N →ₐ[S] MvPolynomial σ (S ⊗[R] N)) = rTensorAlgHom
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
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
inst_5 : DecidableEq σ
x : MvPolynomial σ S ⊗[R] N
⊢ (↑rTensorAlgEquiv : MvPolynomial σ S ⊗[R] N →ₐ[S] MvPolynomial σ (S ⊗[R] N)) = rTensorAlgHom
have e_a : ∀ (i : σ) (d : σ →₀ ℕ),
  Eq (α := S ⊗[R] N)
    (coeff d
      ((AlgHom.comp (↑rTensorAlgEquiv : MvPolynomial σ S ⊗[R] N →ₐ[S] MvPolynomial σ (S ⊗[R] N))
            Algebra.TensorProduct.includeLeft :
          (a : MvPolynomial σ S) → MvPolynomial σ (S ⊗[R] N))
        (X i)))
    (coeff d
      ((AlgHom.comp rTensorAlgHom Algebra.TensorProduct.includeLeft :
          (a : MvPolynomial σ S) → MvPolynomial σ (S ⊗[R] N))
        (X i)))
Tactic: ext _ d
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
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
inst_5 : DecidableEq σ
x : MvPolynomial σ S ⊗[R] N
e_a :
  ∀ (i : σ) (d : σ →₀ ℕ),
    Eq (α := S ⊗[R] N)
      (coeff d
        ((AlgHom.comp (↑rTensorAlgEquiv : MvPolynomial σ S ⊗[R] N →ₐ[S] MvPolynomial σ (S ⊗[R] N))
              Algebra.TensorProduct.includeLeft :
            (a : MvPolynomial σ S) → MvPolynomial σ (S ⊗[R] N))
          (X i)))
      (coeff d
        ((AlgHom.comp rTensorAlgHom Algebra.TensorProduct.includeLeft :
            (a : MvPolynomial σ S) → MvPolynomial σ (S ⊗[R] N))
          (X i)))
⊢ (↑rTensorAlgEquiv : MvPolynomial σ S ⊗[R] N →ₐ[S] MvPolynomial σ (S ⊗[R] N)) = rTensorAlgHom
have e_a₁ : ∀ (x : N) (d : σ →₀ ℕ),
  Eq (α := S ⊗[R] N)
    (coeff d
      ((AlgHom.comp
            (AlgHom.restrictScalars R (↑rTensorAlgEquiv : MvPolynomial σ S ⊗[R] N →ₐ[S] MvPolynomial σ (S ⊗[R] N)))
            Algebra.TensorProduct.includeRight :
          (a : N) → MvPolynomial σ (S ⊗[R] N))
        x))
    (coeff d
      ((AlgHom.comp (AlgHom.restrictScalars R rTensorAlgHom) Algebra.TensorProduct.includeRight :
          (a : N) → MvPolynomial σ (S ⊗[R] N))
        x))
Tactic: ext _ d
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
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
⊢ Eq (α := MvPolynomial σ A →ₐ[A] MvPolynomial σ A)
    (AlgHom.comp (B := A ⊗[R] MvPolynomial σ R)
      (Algebra.TensorProduct.lift (Algebra.ofId A (MvPolynomial σ A)) (mapAlgHom (Algebra.ofId R A)) ⋯ :
        A ⊗[R] MvPolynomial σ R →ₐ[A] MvPolynomial σ A)
      (aeval fun (s : σ) ↦ 1 ⊗ₜ[R] X s : MvPolynomial σ A →ₐ[A] A ⊗[R] MvPolynomial σ R))
    (AlgHom.id A (MvPolynomial σ A))
have hf : ∀ (s : σ) (m : σ →₀ ℕ),
  Eq.{u_4 + 1} (α := A)
    (coeff m
      ((AlgHom.comp (B := A ⊗[R] MvPolynomial σ R)
            (Algebra.TensorProduct.lift (Algebra.ofId A (MvPolynomial σ A)) (mapAlgHom (Algebra.ofId R A)) sorry :
              A ⊗[R] MvPolynomial σ R →ₐ[A] MvPolynomial σ A)
            (aeval fun (s : σ) ↦ 1 ⊗ₜ[R] X s : MvPolynomial σ A →ₐ[A] A ⊗[R] MvPolynomial σ R) :
          (a : MvPolynomial σ A) → MvPolynomial σ A)
        (X s)))
    (coeff m ((AlgHom.id A (MvPolynomial σ A) : (a : MvPolynomial σ A) → MvPolynomial σ A) (X s)))
Tactic: ext s
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.MvPolynomial (goal)
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
⊢ 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)
have 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)) sorry) :
                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: ext s