awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
r : R[X]
x : PolynomialModule R R
dsimp :
  (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • x) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) x : R[X])
⊢ Equiv.toFun (RingEquiv.toEquiv (RingEquiv.symm (toFinsuppIso R))) (r • x) =
    HSMul.hSMul (α := R[X]) ((RingHom.id R[X] : (a : R[X]) → R[X]) r : R[X])
      (Equiv.toFun (RingEquiv.toEquiv (RingEquiv.symm (toFinsuppIso R))) x)

Tactic:
dsimp only [RingEquiv.toEquiv_eq_coe, RingEquiv.coe_toEquiv_symm, Equiv.toFun_as_coe,
        RingHom.id_apply, smul_eq_mul, RingEquiv.coe_coe_toEquiv_symm]

Premises used: RingHom.id_apply, Equiv.toFun_as_coe, RingEquiv.toEquiv_eq_coe, RingEquiv.coe_toEquiv_symm, RingEquiv.coe_coe_toEquiv_symm, smul_eq_mul
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
r : R[X]
zero :
  (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) 0 =
    r * (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) 0
zero₁ : 0 = r * 0
zero₂ zero₃ : Eq.{u_1 + 1} (α := R[X]) 0 0
⊢ (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (HSMul.hSMul (β := PolynomialModule R R) r 0) =
    r * (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) 0

Tactic:
rw [smul_zero, map_zero, mul_zero]

Premises used: smul_zero, map_zero, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
r : R[X]
n : ℕ
a : R
single :
  ∀ (i : ℕ),
    coeff
        ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X])
          (HSMul.hSMul (β := PolynomialModule R R) r
            ((PolynomialModule.single R n : (a : R) → PolynomialModule R R) a : PolynomialModule R R)))
        i =
      (HMul.hMul (β := R[X]) r
            ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X])
                ((PolynomialModule.single R n : (a : R) → PolynomialModule R R) a) :
              R[X])).coeff
        i
⊢ (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X])
      (HSMul.hSMul (β := PolynomialModule R R) r
        ((PolynomialModule.single R n : (a : R) → PolynomialModule R R) a : PolynomialModule R R)) =
    HMul.hMul (β := R[X]) r
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X])
          ((PolynomialModule.single R n : (a : R) → PolynomialModule R R) a) :
        R[X])

Tactic:
ext i
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
r : R[X]
n : ℕ
a : R
i : ℕ
single :
  (if n ≤ i then r.coeff (i - n) * a else 0) =
    ∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, if n = x.2 then r.coeff x.1 * a else 0
⊢ coeff
      ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X])
        (HSMul.hSMul (β := PolynomialModule R R) r
          ((PolynomialModule.single R n : (a : R) → PolynomialModule R R) a : PolynomialModule R R)))
      i =
    (HMul.hMul (β := R[X]) r
          ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X])
              ((PolynomialModule.single R n : (a : R) → PolynomialModule R R) a) :
            R[X])).coeff
      i

Tactic:
simp_rw [toFinsuppIso_symm_apply, coeff_ofFinsupp, coeff_mul, smul_single_apply,
          smul_eq_mul, coeff_ofFinsupp, single_apply, mul_ite, mul_zero]

Premises used: Polynomial.coeff_ofFinsupp, PolynomialModule.single_apply, mul_ite, Polynomial.coeff_mul, MulZeroClass.mul_zero, PolynomialModule.smul_single_apply, Polynomial.toFinsuppIso_symm_apply, smul_eq_mul
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
r : R[X]
n : ℕ
a : R
i : ℕ
pos :
  ∀ (hn : n ≤ i),
    r.coeff (i - n) * a = ∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, if n = x.2 then r.coeff x.1 * a else 0
neg :
  ∀ (hn : ¬n ≤ i),
    Eq.{u_1 + 1} (α := R) 0 (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, if n = x.2 then r.coeff x.1 * a else 0)
⊢ (if n ≤ i then r.coeff (i - n) * a else 0) =
    ∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, if n = x.2 then r.coeff x.1 * a else 0

Tactic:
split_ifs with hn
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
pos : r.coeff (i - n) * a = if n = (i - n, n).2 then r.coeff (i - n, n).1 * a else 0
pos₁ : ∀ b ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, b ≠ (i - n, n) → (if n = b.2 then r.coeff b.1 * a else 0) = 0
pos₂ :
  (i - n, n) ∉ @Finset.antidiagonal _ Nat.instAddMonoid _ i →
    (if n = (i - n, n).2 then r.coeff (i - n, n).1 * a else 0) = 0
⊢ r.coeff (i - n) * a = ∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, if n = x.2 then r.coeff x.1 * a else 0

Tactic:
rw [Finset.sum_eq_single (i - n, n)]

Premises used: HSub.hSub, Prod.mk, Finset.sum_eq_single
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
⊢ r.coeff (i - n) * a = if n = (i - n, n).2 then r.coeff (i - n, n).1 * a else 0

Tactic:
simp only [ite_true]

Premises used: ite_true
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i
hpq2 : (p, q) ≠ (i - n, n)
⊢ (p, q).1 + (p, q).2 = i

Tactic:
rw [Finset.mem_antidiagonal] at hpq1

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i
hpq2 : (p, q) ≠ (i - n, n)
hpq1₁ : (p, q).1 + (p, q).2 = i
⊢ (p, q) ≠ (i - n, n)

Tactic:
rw [Finset.mem_antidiagonal] at hpq1

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).1 + (p, q).2 = i
hpq2 : (p, q) ≠ (i - n, n)
pos : ∀ (H : n = (p, q).2), r.coeff (p, q).1 * a = 0
neg : ∀ (H : ¬n = (p, q).2), Eq.{u_1 + 1} (α := R) 0 0
⊢ (if n = (p, q).2 then r.coeff (p, q).1 * a else 0) = 0

Tactic:
split_ifs with H
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).1 + (p, q).2 = i
hpq2 : (p, q) ≠ (i - n, n)
H : n = q
pos : False
⊢ r.coeff (p, q).1 * a = 0

Tactic:
exfalso
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).1 + (p, q).2 = i
hpq2 : (p, q) ≠ (i - n, n)
H : n = q
pos : (p, q) = (i - n, n)
⊢ False

Tactic:
apply hpq2
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).1 + (p, q).2 = i
hpq2 : (p, q) ≠ (i - n, n)
H : n = q
pos : (p, q) = ((p, q).1 + (p, q).2 - q, q)
⊢ (p, q) = (i - n, n)

Tactic:
rw [← hpq1, H]
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).1 + (p, q).2 = i
hpq2 : (p, q) ≠ (i - n, n)
H : n = q
⊢ (p, q) = ((p, q).1 + (p, q).2 - q, q)

Tactic:
simp only [add_tsub_cancel_right]

Premises used: add_tsub_cancel_right
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).1 + (p, q).2 = i
hpq2 : (p, q) ≠ (i - n, n)
H : ¬n = (p, q).2
⊢ Eq.{u_1 + 1} (α := R) 0 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
H : (i - n, n) ∉ @Finset.antidiagonal _ Nat.instAddMonoid _ i
pos : False
⊢ (if n = (i - n, n).2 then r.coeff (i - n, n).1 * a else 0) = 0

Tactic:
exfalso
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
H : (i - n, n) ∉ @Finset.antidiagonal _ Nat.instAddMonoid _ i
pos : (i - n, n) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i
⊢ False

Tactic:
apply H
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
H : (i - n, n) ∉ @Finset.antidiagonal _ Nat.instAddMonoid _ i
pos : (i - n, n).1 + (i - n, n).2 = i
pos₁ pos₂ : i = i
⊢ (i - n, n) ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i

Tactic:
rw [Finset.mem_antidiagonal, tsub_add_cancel_of_le hn]

Premises used: tsub_add_cancel_of_le, Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
r : R[X]
n : ℕ
a : R
i : ℕ
hn : ¬n ≤ i
neg :
  Eq.{u_1 + 1} (α := R) (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, if n = x.2 then r.coeff x.1 * a else 0) 0
⊢ Eq.{u_1 + 1} (α := R) 0 (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, if n = x.2 then r.coeff x.1 * a else 0)

Tactic:
symm
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
r : R[X]
n : ℕ
a : R
i : ℕ
hn : ¬n ≤ i
neg : ∀ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, ¬n = x.2
⊢ Eq.{u_1 + 1} (α := R) (∑ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, if n = x.2 then r.coeff x.1 * a else 0) 0

Tactic:
rw [Finset.sum_ite_of_false, Finset.sum_const_zero]

Premises used: Finset.sum_const_zero, Finset.sum_ite_of_false
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
r : R[X]
n : ℕ
a : R
i : ℕ
hn : ¬n ≤ i
⊢ ∀ x ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ i, ¬n = x.2

Tactic:
grind [Finset.mem_antidiagonal]

Premises used: Finset.HasAntidiagonal.mem_antidiagonal
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
inst : CommRing R
p : PolynomialModule R R
⊢ Eq (α := R[X]) ((equivPolynomialSelf : (a : PolynomialModule R R) → R[X]) p : R[X])
    ((equivPolynomial : (a : PolynomialModule R R) → R[X]) p : R[X])

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
inst : CommRing R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
n : ℕ
x : S
⊢ Eq (α := S[X])
    ((equivPolynomial : (a : PolynomialModule R S) → S[X]) ((single R n : (a : S) → PolynomialModule R S) x) : S[X])
    ((monomial n : (a : S) → S[X]) x : S[X])

Tactic:
rfl

Premises used: rfl, Finsupp.single
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
M' : Type u_5
inst_3 : AddCommGroup M'
inst_4 : Module R M'
f g : LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) (PolynomialModule R M) M'
h : ∀ (a : ℕ), f ∘ₗ lsingle R a = g ∘ₗ lsingle R a
⊢ f = g

Tactic:
Finsupp.lhom_ext' h

Premises used: Finsupp.lhom_ext', PolynomialModule
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
R' : Type u_4
M' : Type u_5
inst_3 : CommRing R'
inst_4 : AddCommGroup M'
inst_5 : Module R' M'
inst_6 : Module R M'
f : M →ₗ[R] M'
i : ℕ
m : M
⊢ Eq (α := PolynomialModule R' M')
    (((map R' f : LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) (PolynomialModule R M) (PolynomialModule R' M')) :
          (a : PolynomialModule R M) → PolynomialModule R' M')
        ((single R i : (a : M) → PolynomialModule R M) m) :
      PolynomialModule R' M')
    ((single R' i : (a : M') → PolynomialModule R' M') ((f : (a : M) → M') m) : PolynomialModule R' M')

Tactic:
Finsupp.mapRange_single (hf := f.map_zero)

Premises used: PolynomialModule, Finsupp.onFinset, Finsupp.mapRange, Finsupp.mapRange_single, Finsupp.single
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
R' : Type u_4
M' : Type u_5
inst_3 : CommRing R'
inst_4 : AddCommGroup M'
inst_5 : Module R' M'
inst_6 : Module R M'
f : M →ₗ[R] M'
i : ℕ
m : M
⊢ Eq (α := PolynomialModule R' M')
    (((map R' f : LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) (PolynomialModule R M) (PolynomialModule R' M')) :
          (a : PolynomialModule R M) → PolynomialModule R' M')
        ((lsingle R i : (a : M) → PolynomialModule R M) m) :
      PolynomialModule R' M')
    ((lsingle R' i : (a : M') → PolynomialModule R' M') ((f : (a : M) → M') m) : PolynomialModule R' M')

Tactic:
map_single ..

Premises used: PolynomialModule.map_single, Finsupp.single
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
R' : Type u_4
M' : Type u_5
inst_3 : CommRing R'
inst_4 : AddCommGroup M'
inst_5 : Module R' M'
inst_6 : Module R M'
inst_7 : Algebra R R'
inst_8 : IsScalarTower R R' M'
f : M →ₗ[R] M'
p : R[X]
zero :
  ((map R' f : LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) (PolynomialModule R M) (PolynomialModule R' M')) :
        (a : PolynomialModule R M) → PolynomialModule R' M')
      0 =
    HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p)
      (((map R' f : LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) (PolynomialModule R M) (PolynomialModule R' M')) :
          (a : PolynomialModule R M) → PolynomialModule R' M')
        0)
zero₁ : 0 = HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p) 0
zero₂ zero₃ : Eq.{u_5 + 1} (α := PolynomialModule R' M') 0 0
⊢ ((map R' f : LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) (PolynomialModule R M) (PolynomialModule R' M')) :
        (a : PolynomialModule R M) → PolynomialModule R' M')
      (HSMul.hSMul (β := PolynomialModule R M) p 0) =
    HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p)
      (((map R' f : LinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) (PolynomialModule R M) (PolynomialModule R' M')) :
          (a : PolynomialModule R M) → PolynomialModule R' M')
        0)

Tactic:
rw [smul_zero, map_zero, smul_zero]

Premises used: smul_zero, map_zero
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst_7 : CommRing R'
inst_8 : AddCommGroup M'
inst_9 : Module R' M'
inst_10 : Module R M'
inst_11 : Algebra R R'
inst_12 : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ (Finsupp.sum (s • m) fun (i : ℕ) (m : M) ↦ r ^ i • m) =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) s : R) (Finsupp.sum m fun (i : ℕ) (m : M) ↦ r ^ i • m)

Tactic:
(Finsupp.sum_smul_index' ?_).trans ?_

Premises used: Finsupp.sum_smul_index', Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst_7 : CommRing R'
inst_8 : AddCommGroup M'
inst_9 : Module R' M'
inst_10 : Module R M'
inst_11 : Algebra R R'
inst_12 : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
refine_1 : ∀ (i : ℕ), HSMul.hSMul (β := M) (r ^ i) 0 = 0
refine_2 :
  (Finsupp.sum m fun (i : ℕ) (c : M) ↦ r ^ i • s • c) =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) s : R) (Finsupp.sum m fun (i : ℕ) (m : M) ↦ r ^ i • m)
⊢ (Finsupp.sum (s • m) fun (i : ℕ) (m : M) ↦ r ^ i • m) =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) s : R) (Finsupp.sum m fun (i : ℕ) (m : M) ↦ r ^ i • m)

Tactic:
refine (Finsupp.sum_smul_index' ?_).trans ?_

Premises used: Finsupp.sum_smul_index', Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst_7 : CommRing R'
inst_8 : AddCommGroup M'
inst_9 : Module R' M'
inst_10 : Module R M'
inst_11 : Algebra R R'
inst_12 : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ ∀ (i : ℕ), HSMul.hSMul (β := M) (r ^ i) 0 = 0

Tactic:
fun i => smul_zero _

Premises used: smul_zero, HPow.hPow
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst_7 : CommRing R'
inst_8 : AddCommGroup M'
inst_9 : Module R' M'
inst_10 : Module R M'
inst_11 : Algebra R R'
inst_12 : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ ∀ (i : ℕ), HSMul.hSMul (β := M) (r ^ i) 0 = 0

Tactic:
exact fun i => smul_zero _

Premises used: smul_zero
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst_7 : CommRing R'
inst_8 : AddCommGroup M'
inst_9 : Module R' M'
inst_10 : Module R M'
inst_11 : Algebra R R'
inst_12 : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
refine_2 :
  Eq (α := M) (Finsupp.sum m fun (i : ℕ) (c : M) ↦ r ^ i • s • c) (Finsupp.sum m fun (a : ℕ) (b : M) ↦ s • r ^ a • b)
⊢ (Finsupp.sum m fun (i : ℕ) (c : M) ↦ r ^ i • s • c) =
    HSMul.hSMul (α := R) (β := M) ((RingHom.id R : (a : R) → R) s : R) (Finsupp.sum m fun (i : ℕ) (m : M) ↦ r ^ i • m)

Tactic:
simp_rw [RingHom.id_apply, Finsupp.smul_sum]

Premises used: RingHom.id_apply, Finsupp.smul_sum
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst_7 : CommRing R'
inst_8 : AddCommGroup M'
inst_9 : Module R' M'
inst_10 : Module R M'
inst_11 : Algebra R R'
inst_12 : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
refine_2 : Eq.{u_2 + 1} (α := ℕ → M → M) (fun (i : ℕ) (c : M) ↦ r ^ i • s • c) fun (a : ℕ) (b : M) ↦ s • r ^ a • b
⊢ Eq (α := M) (Finsupp.sum m fun (i : ℕ) (c : M) ↦ r ^ i • s • c) (Finsupp.sum m fun (a : ℕ) (b : M) ↦ s • r ^ a • b)

Tactic:
congr
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst_7 : CommRing R'
inst_8 : AddCommGroup M'
inst_9 : Module R' M'
inst_10 : Module R M'
inst_11 : Algebra R R'
inst_12 : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
refine_2 : ∀ (i : ℕ) (c : M), r ^ i • s • c = s • r ^ i • c
⊢ Eq.{u_2 + 1} (α := ℕ → M → M) (fun (i : ℕ) (c : M) ↦ r ^ i • s • c) fun (a : ℕ) (b : M) ↦ s • r ^ a • b

Tactic:
ext i c
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M
inst_6 : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst_7 : CommRing R'
inst_8 : AddCommGroup M'
inst_9 : Module R' M'
inst_10 : Module R M'
inst_11 : Algebra R R'
inst_12 : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
i : ℕ
c : M
refine_2 refine_2₁ : s • r ^ i • c = s • r ^ i • c
⊢ r ^ i • s • c = s • r ^ i • c

Tactic:
rw [smul_comm]

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
i : ℕ
m : M
⊢ (eval r : (a : PolynomialModule R M) → M) ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) =
    r ^ i • m

Tactic:
Finsupp.sum_single_index (smul_zero _)

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum_single_index, Finsupp.sum, smul_zero, Finset.sum
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
r : R
i : ℕ
m : M
⊢ (eval r : (a : PolynomialModule R M) → M) ((lsingle R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) =
    r ^ i • m

Tactic:
eval_single r i m

Premises used: Finsupp.single, PolynomialModule.eval_single