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
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
⊢ 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₁ : HSMul.hSMul (α := A) (β := A[X]) 1 ((aeval X : (a : R[X]) → A[X]) 1) = 1
Tactic: rw [toFunLinear_tmul_apply, toFunBilinear_apply_apply, Polynomial.aeval_one, one_smul]
-- 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
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
⊢ 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₂ : HSMul.hSMul (α := A) (β := A[X]) 1 1 = 1
Tactic: rw [toFunLinear_tmul_apply, toFunBilinear_apply_apply, Polynomial.aeval_one, one_smul]
-- 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
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
⊢ 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]) 1 1
Tactic: rw [toFunLinear_tmul_apply, toFunBilinear_apply_apply, Polynomial.aeval_one, one_smul]
-- 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
x : A ⊗[R] R[X]
⊢ invFun R A ((toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) x) = x
have refine_1 : Eq (α := A ⊗[R] R[X]) (invFun R A ((toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) 0)) 0
Tactic: refine TensorProduct.induction_on x ?_ ?_ ?_
-- 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
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
⊢ invFun R A ((toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) x) = x
have 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)
Tactic: refine TensorProduct.induction_on x ?_ ?_ ?_
-- 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
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)
⊢ invFun R A ((toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) x) = x
have 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
Tactic: refine TensorProduct.induction_on x ?_ ?_ ?_
-- 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
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ 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
have 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)
Tactic: rw [toFunAlgHom_apply_tmul, eval₂_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
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ 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)
have refine_2 : Eq (α := A ⊗[R] R[X]) (a ⊗ₜ[R] ∑ a ∈ p.support, p.coeff a • HPow.hPow (α := R[X]) X 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]
-- 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
x : A ⊗[R] R[X]
a : A
p : R[X]
| a ⊗ₜ[R] p
have 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)
Tactic: rw [← sum_C_mul_X_pow_eq 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
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ Eq (α := A ⊗[R] R[X]) (a ⊗ₜ[R] ∑ a ∈ p.support, p.coeff a • HPow.hPow (α := R[X]) X a) (a ⊗ₜ[R] p)
have 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))
Tactic: conv_rhs => rw [← sum_C_mul_X_pow_eq 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
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ 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))
have 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))
Tactic: simp only [Algebra.smul_def]
-- 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
x : A[X]
⊢ (toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) (invFun R A x) = x
have 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
Tactic: refine Polynomial.induction_on' x ?_ ?_
-- 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
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
⊢ (toFunAlgHom R A : (a : A ⊗[R] R[X]) → A[X]) (invFun R A x) = x
have 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])
Tactic: refine Polynomial.induction_on' x ?_ ?_
-- 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
x : A[X]
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])
have 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])
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]
-- 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
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])
⊢ 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])
have 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])
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]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialAlgebra (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
x : R[X]
x_1 : A[X]
⊢ HMul.hMul (α := A[X]) (((mapRingHom (algebraMap R A) : RingHom.{u_1, u_3} R[X] A[X]) : (a : R[X]) → A[X]) x : A[X])
      x_1 =
    HMul.hMul (β := A[X]) x_1
      (((mapRingHom (algebraMap R A) : RingHom.{u_1, u_3} R[X] A[X]) : (a : R[X]) → A[X]) x : A[X])
have a : ∀ (n : ℕ),
  (HMul.hMul (α := A[X]) (((mapRingHom (algebraMap R A) : RingHom.{u_1, u_3} R[X] A[X]) : (a : R[X]) → A[X]) x : A[X])
          x_1).coeff
      n =
    (HMul.hMul (β := A[X]) x_1
          (((mapRingHom (algebraMap R A) : RingHom.{u_1, u_3} R[X] A[X]) : (a : R[X]) → A[X]) x : A[X])).coeff
      n
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialAlgebra (goal)
Goal:
R : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : Algebra R S
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
x : R[X]
x_1 : A[X]
n : ℕ
⊢ (HMul.hMul (α := A[X]) (((mapRingHom (algebraMap R A) : RingHom.{u_1, u_3} R[X] A[X]) : (a : R[X]) → A[X]) x : A[X])
          x_1).coeff
      n =
    (HMul.hMul (β := A[X]) x_1
          (((mapRingHom (algebraMap R A) : RingHom.{u_1, u_3} R[X] A[X]) : (a : R[X]) → A[X]) x : A[X])).coeff
      n
have a : Eq.{u_3 + 1} (α := A)
  (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
    coeff (((mapRingHom (algebraMap R A) : RingHom.{u_1, u_3} R[X] A[X]) : (a : R[X]) → A[X]) x) p.swap.1 *
      x_1.coeff p.swap.2)
  (∑ x_2 ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
    x_1.coeff x_2.1 *
      coeff (((mapRingHom (algebraMap R A) : RingHom.{u_1, u_3} R[X] A[X]) : (a : R[X]) → A[X]) x) x_2.2)
Tactic: rw [coeff_mul, ← Finset.Nat.sum_antidiagonal_swap, coeff_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
a b : R
f : M →ₚₗ[R] N
⊢ (a + b) • f = a • f + b • f
have toFun' : ∀ (x : Type u) (x_1 : CommSemiring x) (x_2 : Algebra R x) (x_3 : x ⊗[R] M),
  ((a + b) • f).toFun' x x_3 = (a • f + b • f).toFun' x x_3
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
⊢ HSMul.hSMul (α := R) 0 f = 0
have toFun' : ∀ (S : Type u) (x : CommSemiring S) (x_1 : Algebra R S) (x_2 : S ⊗[R] M),
  (HSMul.hSMul (α := R) 0 f).toFun' S x_2 = toFun' 0 S x_2
Tactic: ext S
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
⊢ HSMul.hSMul (α := R) 1 f = f
have toFun' : ∀ (S : Type u) (x : CommSemiring S) (x_1 : Algebra R S) (x_2 : S ⊗[R] M),
  (HSMul.hSMul (α := R) 1 f).toFun' S x_2 = f.toFun' S x_2
Tactic: ext S
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
r a_1 b_1 : R
f_1 g : M →ₚₗ[R] N
a b : R
f : M →ₚₗ[R] N
⊢ (a * b) • f = a • b • f
have toFun' : ∀ (x : Type u) (x_1 : CommSemiring x) (x_2 : Algebra R x) (x_3 : x ⊗[R] M),
  ((a * b) • f).toFun' x x_3 = (a • b • f).toFun' x x_3
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
r a b : R
f_1 g_1 f g h : M →ₚₗ[R] N
⊢ f + g + h = f + (g + h)
have toFun' : ∀ (x : Type u) (x_1 : CommSemiring x) (x_2 : Algebra R x) (x_3 : x ⊗[R] M),
  (f + g + h).toFun' x x_3 = (f + (g + h)).toFun' x x_3
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
r a b : R
f_1 g f : M →ₚₗ[R] N
⊢ 0 + f = f
have toFun' : ∀ (x : Type u) (x_1 : CommSemiring x) (x_2 : Algebra R x) (x_3 : x ⊗[R] M), (0 + f).toFun' x x_3 = f.toFun' x x_3
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
r a b : R
f_1 g f : M →ₚₗ[R] N
⊢ f + 0 = f
have toFun' : ∀ (x : Type u) (x_1 : CommSemiring x) (x_2 : Algebra R x) (x_3 : x ⊗[R] M), (f + 0).toFun' x x_3 = f.toFun' x x_3
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
r a b : R
f_1 g_1 f g : M →ₚₗ[R] N
⊢ f + g = g + f
have toFun' : ∀ (x : Type u) (x_1 : CommSemiring x) (x_2 : Algebra R x) (x_3 : x ⊗[R] M), (f + g).toFun' x x_3 = (g + f).toFun' x x_3
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
r a_1 b : R
f_1 g_1 : M →ₚₗ[R] N
a : R
f g : M →ₚₗ[R] N
⊢ a • (f + g) = a • f + a • g
have toFun' : ∀ (x : Type u) (x_1 : CommSemiring x) (x_2 : Algebra R x) (x_3 : x ⊗[R] M),
  (a • (f + g)).toFun' x x_3 = (a • f + a • g).toFun' x x_3
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommGroup N
inst_4 : Module R N
f_1 : M →ₚₗ[R] N
n : ℕ
f : M →ₚₗ[R] N
⊢ HSMul.hSMul (α := R) (↑(Int.negSucc n) : R) f = -HSMul.hSMul (α := R) (↑(↑n.succ : ℤ) : R) f
have toFun' : ∀ (S : Type u) (x : CommSemiring S) (x_1 : Algebra R S) (m : S ⊗[R] M),
  (HSMul.hSMul (α := R) (↑(Int.negSucc n) : R) f).toFun' S m = (-HSMul.hSMul (α := R) (↑(↑n.succ : ℤ) : R) f).toFun' S m
Tactic: ext S _ _ m
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommGroup N
inst_4 : Module R N
f_1 : M →ₚₗ[R] N
n : ℕ
f : M →ₚₗ[R] N
S : Type u
x : CommSemiring S
x_1 : Algebra R S
m : S ⊗[R] M
⊢ (HSMul.hSMul (α := R) (↑(Int.negSucc n) : R) f).toFun' S m =
    HSMul.hSMul (α := R) (β := S ⊗[R] M → S ⊗[R] N) (-1) ((HSMul.hSMul (α := R) (↑(↑n.succ : ℤ) : R) f).toFun' S) m
have toFun' : HSMul.hSMul (α := R) (-1) (f.toFun' S m) + HSMul.hSMul (α := R) (-(↑n : R)) (f.toFun' S m) =
  HSMul.hSMul (α := R) (-(↑n : R)) (f.toFun' S m) + HSMul.hSMul (α := R) (-1) (f.toFun' S m)
Tactic: simp only [Int.cast_negSucc, Nat.cast_add, Nat.cast_one, neg_add_rev, _root_.add_smul,
      add_def_apply, smul_def_apply, Nat.succ_eq_add_one, Int.cast_add, Int.cast_natCast,
      Int.cast_one, _root_.one_smul, add_def, smul_def, Pi.smul_apply, Pi.add_apply, smul_add,
      smul_smul, neg_mul, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommGroup N
inst_4 : Module R N
f_1 : M →ₚₗ[R] N
n : ℕ
f : M →ₚₗ[R] N
S : Type u
x : CommSemiring S
x_1 : Algebra R S
m : S ⊗[R] M
⊢ HSMul.hSMul (α := R) (-1) (f.toFun' S m) + HSMul.hSMul (α := R) (-(↑n : R)) (f.toFun' S m) =
    HSMul.hSMul (α := R) (-(↑n : R)) (f.toFun' S m) + HSMul.hSMul (α := R) (-1) (f.toFun' S m)
have toFun' : HSMul.hSMul (α := R) (-(↑n : R)) (f.toFun' S m) + HSMul.hSMul (α := R) (-1) (f.toFun' S m) =
  HSMul.hSMul (α := R) (-(↑n : R)) (f.toFun' S m) + HSMul.hSMul (α := R) (-1) (f.toFun' S m)
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommGroup N
inst_4 : Module R N
f_1 f : M →ₚₗ[R] N
S : Type u
x : CommSemiring S
x_1 : Algebra R S
m : S ⊗[R] M
⊢ HSMul.hSMul (α := R) (-1) (f.toFun' S m) + f.toFun' S m = 0
have toFun' : HSMul.hSMul (α := R) (-1) (f.toFun' S m) + HSMul.hSMul (α := R) 1 (f.toFun' S m) = 0
Tactic: nth_rewrite 2 [← _root_.one_smul (M := R) (b := f.toFun' S m)]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommGroup N
inst_4 : Module R N
f_1 f : M →ₚₗ[R] N
S : Type u
x : CommSemiring S
x_1 : Algebra R S
m : S ⊗[R] M
⊢ HSMul.hSMul (α := R) (-1) (f.toFun' S m) + HSMul.hSMul (α := R) 1 (f.toFun' S m) = 0
have toFun' : HAdd.hAdd (α := R) (-1) 1 • f.toFun' S m = 0
Tactic: rw [← _root_.add_smul]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommRing R
M : Type u_1
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommGroup N
inst_4 : Module R N
f_1 f g : M →ₚₗ[R] N
⊢ f + g = g + f
have toFun' : ∀ (x : Type u) (x_1 : CommSemiring x) (x_2 : Algebra R x) (x_3 : x ⊗[R] M), (f + g).toFun' x x_3 = (g + f).toFun' x x_3
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
⊢ Eq (α := S ⊗[R] N) (1 ⊗ₜ[R] f.ground x) (f.toFun' S (1 ⊗ₜ[R] x))
have rw : Eq (α := S ⊗[R] N) (1 ⊗ₜ[R] (TensorProduct.lid R N : (a : R ⊗[R] N) → N) (f.toFun' R (1 ⊗ₜ[R] x)) : S ⊗[R] N)
  (f.toFun' S (1 ⊗ₜ[R] x) : S ⊗[R] N)
Tactic: rw [ground_apply]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
⊢ Eq (α := S ⊗[R] N) (1 ⊗ₜ[R] (TensorProduct.lid R N : (a : R ⊗[R] N) → N) (f.toFun' R (1 ⊗ₜ[R] x)) : S ⊗[R] N)
    (f.toFun' S (1 ⊗ₜ[R] x) : S ⊗[R] N)
have h : Eq (α := S ⊗[R] N) (1 ⊗ₜ[R] (TensorProduct.lid R N : (a : R ⊗[R] N) → N) (f.toFun' R (1 ⊗ₜ[R] x)) : S ⊗[R] N)
  ((rTensor N (toLinearMap (Algebra.algHom R R S)) : (a : R ⊗[R] N) → S ⊗[R] N) (f.toFun' R (1 ⊗ₜ[R] x)) : S ⊗[R] N)
Tactic: convert! f.isCompat_apply' (Algebra.algHom R R S) (1 ⊗ₜ[R] x)
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
h :
  Eq (α := S ⊗[R] N) (1 ⊗ₜ[R] (TensorProduct.lid R N : (a : R ⊗[R] N) → N) (f.toFun' R (1 ⊗ₜ[R] x)) : S ⊗[R] N)
    ((rTensor N (toLinearMap (Algebra.algHom R R S)) : (a : R ⊗[R] N) → S ⊗[R] N) (f.toFun' R (1 ⊗ₜ[R] x)) : S ⊗[R] N)
⊢ Eq (α := S ⊗[R] N) (1 ⊗ₜ[R] (TensorProduct.lid R N : (a : R ⊗[R] N) → N) (f.toFun' R (1 ⊗ₜ[R] x)) : S ⊗[R] N)
    (f.toFun' S (1 ⊗ₜ[R] x) : S ⊗[R] N)
have h₁ : Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x)
  ((rTensor M (toLinearMap (Algebra.algHom R R S)) : (a : R ⊗[R] M) → S ⊗[R] M) (1 ⊗ₜ[R] x))
Tactic: convert! f.isCompat_apply' (Algebra.algHom R R S) (1 ⊗ₜ[R] x)
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
⊢ Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x)
    ((rTensor M (toLinearMap (Algebra.algHom R R S)) : (a : R ⊗[R] M) → S ⊗[R] M) (1 ⊗ₜ[R] x))
have h : Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x : S ⊗[R] M) ((toLinearMap (Algebra.algHom R R S) : (a : R) → S) 1 ⊗ₜ[R] x : S ⊗[R] M)
Tactic: rw [rTensor_tmul, toLinearMap_apply, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
h : Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x : S ⊗[R] M) ((toLinearMap (Algebra.algHom R R S) : (a : R) → S) 1 ⊗ₜ[R] x : S ⊗[R] M)
⊢ Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x)
    ((rTensor M (toLinearMap (Algebra.algHom R R S)) : (a : R ⊗[R] M) → S ⊗[R] M) (1 ⊗ₜ[R] x))
have h₁ : Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x : S ⊗[R] M) ((Algebra.algHom R R S : (a : R) → S) 1 ⊗ₜ[R] x : S ⊗[R] M)
Tactic: rw [rTensor_tmul, toLinearMap_apply, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
S : Type u
inst_5 : CommSemiring S
inst_6 : Algebra R S
x : M
h : Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x : S ⊗[R] M) ((toLinearMap (Algebra.algHom R R S) : (a : R) → S) 1 ⊗ₜ[R] x : S ⊗[R] M)
h₁ : Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x : S ⊗[R] M) ((Algebra.algHom R R S : (a : R) → S) 1 ⊗ₜ[R] x : S ⊗[R] M)
⊢ Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x)
    ((rTensor M (toLinearMap (Algebra.algHom R R S)) : (a : R ⊗[R] M) → S ⊗[R] M) (1 ⊗ₜ[R] x))
have h₂ : Eq (α := S ⊗[R] M) (1 ⊗ₜ[R] x) (1 ⊗ₜ[R] x)
Tactic: rw [rTensor_tmul, toLinearMap_apply, map_one]
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f x y : M →ₚₗ[R] N
⊢ (x + y).ground = x.ground + y.ground
have h : ∀ (m : M), (x + y).ground m = (x.ground + y.ground) m
Tactic: ext m
-- Lean 4 proof step from Mathlib.RingTheory.PolynomialLaw.Basic (goal)
Goal:
R : Type u
inst : CommSemiring R
M : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_2
inst_3 : AddCommMonoid N
inst_4 : Module R N
f : M →ₚₗ[R] N
r : R
x : M →ₚₗ[R] N
⊢ (r • x).ground = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) x.ground
have h : ∀ (m : M), (r • x).ground m = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) x.ground m
Tactic: ext m