awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
p : Submodule R M
hp :
  Membership.mem (γ := Sublattice (Submodule R M)) (End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a)) p
x :
  ↥((mapSubmodule R M a :
          (a_1 : ↥((Algebra.lsmul R R M : (a : A) → End R M) a).invtSubmodule) → Submodule R[X] (AEval R M a))
        (Subtype.mk (p := fun (x : Submodule R M) ↦
          Membership.mem (γ := Sublattice (Submodule R M))
            (End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a)) x)
          p hp) :
      Submodule.{u_1, u_3} R[X] (AEval R M a))
obtain :
  ∀ (x : AEval R M a)
    (hx :
      Membership.mem (γ := Submodule.{u_1, u_3} R[X] (AEval R M a))
        ((mapSubmodule R M a :
              (a_1 : ↥((Algebra.lsmul R R M : (a : A) → End R M) a).invtSubmodule) → Submodule R[X] (AEval R M a))
            (Subtype.mk (p := fun (x : Submodule R M) ↦
              Membership.mem (γ := Sublattice (Submodule R M))
                (End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a)) x)
              p hp) :
          Submodule.{u_1, u_3} R[X] (AEval R M a))
        x),
    Membership.mem (α := M) p
      ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
          (↑(Subtype.mk (p := fun (x : AEval R M a) ↦
                Membership.mem (γ := Submodule.{u_1, u_3} R[X] (AEval R M a))
                  ((mapSubmodule R M a :
                        (a_1 : ↥((Algebra.lsmul R R M : (a : A) → End R M) a).invtSubmodule) →
                          Submodule R[X] (AEval R M a))
                      (Subtype.mk (p := fun (x : Submodule R M) ↦
                        Membership.mem (γ := Sublattice (Submodule R M))
                          (End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a)) x)
                        p hp) :
                    Submodule.{u_1, u_3} R[X] (AEval R M a))
                  x)
                x hx) :
            AEval R M a) :
        M)
⊢ Membership.mem (α := M) p ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (↑x : AEval R M a) : M)

Tactic:
obtain ⟨x, hx⟩ := x
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
p : Submodule R M
hp :
  Membership.mem (γ := Sublattice (Submodule R M)) (End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a)) p
x : AEval R M a
hx :
  Membership.mem (γ := Submodule.{u_1, u_3} R[X] (AEval R M a))
    ((mapSubmodule R M a :
          (a_1 : ↥((Algebra.lsmul R R M : (a : A) → End R M) a).invtSubmodule) → Submodule R[X] (AEval R M a))
        (Subtype.mk (p := fun (x : Submodule R M) ↦
          Membership.mem (γ := Sublattice (Submodule R M))
            (End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a)) x)
          p hp) :
      Submodule.{u_1, u_3} R[X] (AEval R M a))
    x
⊢ Membership.mem (α := M) p
    ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M)
        (↑(Subtype.mk (p := fun (x : AEval R M a) ↦
              Membership.mem (γ := Submodule.{u_1, u_3} R[X] (AEval R M a))
                ((mapSubmodule R M a :
                      (a_1 : ↥((Algebra.lsmul R R M : (a : A) → End R M) a).invtSubmodule) →
                        Submodule R[X] (AEval R M a))
                    (Subtype.mk (p := fun (x : Submodule R M) ↦
                      Membership.mem (γ := Sublattice (Submodule R M))
                        (End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a)) x)
                      p hp) :
                  Submodule.{u_1, u_3} R[X] (AEval R M a))
                x)
              x hx) :
          AEval R M a) :
      M)

Tactic:
simpa using hx
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
p : Submodule R M
hp :
  Membership.mem (γ := Sublattice (Submodule R M)) (End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a)) p
x : ↥p
⊢ (equiv_mapSubmodule a p hp :
        (a_1 : ↥p) →
          ↥((mapSubmodule R M a :
                (a_2 : ↥((Algebra.lsmul R R M : (a : A) → End R M) a).invtSubmodule) → Submodule R[X] (AEval R M a))
              ⟨p, hp⟩))
      (LinearMap.restrict ((Algebra.lsmul R R M : (a : A) → End R M) a) hp • x) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := R[X]) (β :=
      ↥((mapSubmodule R M a :
              (a_1 : ↥((Algebra.lsmul R R M : (a : A) → End R M) a).invtSubmodule) → Submodule R[X] (AEval R M a))
            (Subtype.mk (p := fun (x : Submodule R M) ↦
              Membership.mem (γ := Sublattice (Submodule R M))
                (End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a)) x)
              p hp) :
          Submodule.{u_1, u_3} R[X] (AEval R M a)))
      X
      ((equiv_mapSubmodule a p hp :
            (a_1 : ↥p) →
              ↥((mapSubmodule R M a :
                    (a_2 : ↥((Algebra.lsmul R R M : (a : A) → End R M) a).invtSubmodule) → Submodule R[X] (AEval R M a))
                  ⟨p, hp⟩))
          x :
        ↥((mapSubmodule R M a :
                (a_1 : ↥((Algebra.lsmul R R M : (a : A) → End R M) a).invtSubmodule) → Submodule R[X] (AEval R M a))
              (Subtype.mk (p := fun (x : Submodule R M) ↦
                Membership.mem (γ := Sublattice (Submodule R M))
                  (End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a)) x)
                p hp) :
            Submodule.{u_1, u_3} R[X] (AEval R M a)))

Tactic:
simp [equiv_mapSubmodule, X_smul_of]

Premises used: Module.AEval.X_smul_of, Module.AEval.equiv_mapSubmodule
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_2
M : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
φ : M →ₗ[R] M
⊢ AEval' φ = AEval R M φ

Tactic:
rfl

Premises used: Module.AEval, rfl
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_2
M : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
φ : M →ₗ[R] M
m : M
⊢ HSMul.hSMul.{u_2, u_1, u_1} (α := R[X]) (β := AEval' φ) X ((of φ : (a : M) → AEval' φ) m : AEval' φ) =
    (of φ : (a : M) → AEval' φ) ((φ : (a : M) → M) m)

Tactic:
AEval.X_smul_of _ _

Premises used: Module.AEval.X_smul_of
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_2
M : Type u_1
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
φ : M →ₗ[R] M
m : M
n : ℕ
⊢ HSMul.hSMul (β := AEval' φ) (HPow.hPow (α := R[X]) X n) ((of φ : (a : M) → AEval' φ) m : AEval' φ) =
    (of φ : (a : M) → AEval' φ) (φ ^ n • m)

Tactic:
AEval.X_pow_smul_of ..

Premises used: Module.AEval.X_pow_smul_of
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
φ : M →ₗ[R] M
m : AEval' φ
⊢ Eq (α := M) (((of φ).symm : (a : AEval' φ) → M) (HSMul.hSMul.{u_1, u_2, u_2} (α := R[X]) X m) : M)
    ((φ : (a : M) → M) (((of φ).symm : (a : AEval' φ) → M) m : M) : M)

Tactic:
AEval.of_symm_X_smul _ _

Premises used: Module.AEval.of_symm_X_smul
-- Module: Mathlib.Algebra.Polynomial.Module.AEval
Goal:
R : Type u_1
A : Type ?u.283836
M : Type u_2
inst : CommSemiring R
inst_1 : Semiring A
a : A
inst_2 : Algebra R A
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
φ : M →ₗ[R] M
inst_7 : Module.Finite R M
⊢ Module.Finite.{u_1, u_2} R[X] (AEval' φ)

Tactic:
inferInstance

Premises used: inferInstance
-- 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 : ℕ
⊢ Eq.{u_2 + 1} (α := M) ((0 : (a : ℕ) → M) i : M) (0 : M)

Tactic:
Finsupp.zero_apply

Premises used: Finsupp.zero_apply
-- 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
g₁ g₂ : PolynomialModule R M
a : ℕ
⊢ (g₁ + g₂ : (a : ℕ) → M) a = HAdd.hAdd (α := M) (β := M) ((g₁ : (a : ℕ) → M) a : M) ((g₂ : (a : ℕ) → M) a : M)

Tactic:
Finsupp.add_apply g₁ g₂ a

Premises used: Finsupp.add_apply
-- 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 : ℕ
m : M
n : ℕ
⊢ (((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) : (a : ℕ) → M) n = if i = n then m else 0

Tactic:
Finsupp.single_apply

Premises used: Finsupp.single_apply
-- 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 : ℕ
m : M
n : ℕ
⊢ (((lsingle R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M) : (a : ℕ) → M) n = if i = n then m else 0

Tactic:
Finsupp.single_apply

Premises used: Finsupp.single_apply
-- 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 : ℕ
r : R
m : M
⊢ (single R i : (a : M) → PolynomialModule R M) (r • m) =
    HSMul.hSMul (β := PolynomialModule R M) r ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)

Tactic:
(lsingle R i).map_smul r m

Premises used: LinearMap.map_smul, PolynomialModule.lsingle, 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
motive : PolynomialModule R M → Prop
f : PolynomialModule R M
zero : motive 0
add : ∀ (f g : PolynomialModule R M), motive f → motive g → motive (f + g)
single : ∀ (a : ℕ) (b : M), motive ((PolynomialModule.single R a : (a : M) → PolynomialModule R M) b)
⊢ motive f

Tactic:
Finsupp.induction_linear f zero add single

Premises used: Finsupp.induction_linear
-- 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
f : R[X]
m : PolynomialModule R M
⊢ f • m =
    (((aeval (Finsupp.lmapDomain M R Nat.succ) : (a : R[X]) → (ℕ →₀ M) →ₗ[R] ℕ →₀ M) f : (ℕ →₀ M) →ₗ[R] ℕ →₀ M) :
        (a : ℕ →₀ M) → ℕ →₀ M)
      m

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M_1 : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M_1
inst_6 : IsScalarTower S R M_1
M : Type u
inst_7 : AddCommGroup M
inst_8 : Module R M
inst_9 : Module S M
inst_10 : IsScalarTower S R M
⊢ IsScalarTower.{u_3, u_1, u} S R (PolynomialModule R M)

Tactic:
Finsupp.isScalarTower _ _

Premises used: PolynomialModule, Finsupp.isScalarTower
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M_1 : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M_1
inst_6 : IsScalarTower S R M_1
M : Type u
inst_7 : AddCommGroup M
inst_8 : Module R M
inst_9 : Module S M
inst_10 : IsScalarTower S R M
⊢ IsScalarTower.{u_1, u_1, u} R R[X] (PolynomialModule R M)

Tactic:
haveI : IsScalarTower R R[X] (PolynomialModule R M) :=
    inferInstanceAs <| IsScalarTower R R[X] <| Module.AEval' <| Finsupp.lmapDomain M R Nat.succ
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M_1 : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M_1
inst_6 : IsScalarTower S R M_1
M : Type u
inst_7 : AddCommGroup M
inst_8 : Module R M
inst_9 : Module S M
inst_10 : IsScalarTower S R M
this : IsScalarTower.{u_1, u_1, u} R R[X] (PolynomialModule R M)
smul_assoc : ∀ (x : S) (y : R[X]) (z : PolynomialModule R M), (x • y) • z = x • y • z
⊢ IsScalarTower.{u_3, u_1, u} S R[X] (PolynomialModule R M)

Tactic:
constructor
-- Module: Mathlib.Algebra.Polynomial.Module.Basic
Goal:
R : Type u_1
M_1 : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M_1
inst_2 : Module R M_1
I : Ideal R
S : Type u_3
inst_3 : CommSemiring S
inst_4 : Algebra S R
inst_5 : Module S M_1
inst_6 : IsScalarTower S R M_1
M : Type u
inst_7 : AddCommGroup M
inst_8 : Module R M
inst_9 : Module S M
inst_10 : IsScalarTower S R M
this : IsScalarTower.{u_1, u_1, u} R R[X] (PolynomialModule R M)
x : S
y : R[X]
z : PolynomialModule R M
smul_assoc : HSMul.hSMul (α := R) ((algebraMap S R : (a : S) → R) x : R) y • z = x • y • z
smul_assoc₁ :
  HSMul.hSMul (α := R) ((algebraMap S R : (a : S) → R) x : R) y • z =
    HSMul.hSMul.{u_1, u, u} (α := R) ((algebraMap S R : (a : S) → R) x : R) (y • z)
smul_assoc₂ smul_assoc₃ :
  HSMul.hSMul.{u_1, u, u} (α := R) ((algebraMap S R : (a : S) → R) x : R) (y • z) =
    HSMul.hSMul.{u_1, u, u} (α := R) ((algebraMap S R : (a : S) → R) x : R) (y • z)
⊢ (x • y) • z = x • y • z

Tactic:
rw [← @IsScalarTower.algebraMap_smul S R, ← @IsScalarTower.algebraMap_smul S R, smul_assoc]

Premises used: smul_assoc, IsScalarTower.algebraMap_smul
-- 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 : ℕ
r : R
j : ℕ
m : M
simp :
  HSMul.hSMul (β := ℕ →₀ M) r
      ((⇑(Finsupp.lmapDomain M R Nat.succ) : (a : ℕ →₀ M) → ℕ →₀ M)^[i]
          ((single R j : (a : M) → PolynomialModule R M) m) :
        ℕ →₀ M) =
    (single R (i + j) : (a : M) → PolynomialModule R M) (r • m)
⊢ HSMul.hSMul (α := R[X]) (β := PolynomialModule R M) ((monomial i : (a : R) → R[X]) r : R[X])
      ((single R j : (a : M) → PolynomialModule R M) m : PolynomialModule R M) =
    (single R (i + j) : (a : M) → PolynomialModule R M) (r • m)

Tactic:
simp only [Module.End.mul_apply, Polynomial.aeval_monomial, Module.End.pow_apply,
    Module.algebraMap_end_apply, smul_def]

Premises used: PolynomialModule.smul_def, Module.End.pow_apply, Module.algebraMap_end_apply, Polynomial.aeval_monomial, Module.End.mul_apply
-- 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
j : ℕ
m : M
zero :
  HSMul.hSMul (β := ℕ →₀ M) r (id ((single R j : (a : M) → PolynomialModule R M) m) : ℕ →₀ M) =
    (single R j : (a : M) → PolynomialModule R M) (r • m)
⊢ HSMul.hSMul (β := ℕ →₀ M) r
      ((⇑(Finsupp.lmapDomain M R Nat.succ) : (a : ℕ →₀ M) → ℕ →₀ M)^[0]
          ((single R j : (a : M) → PolynomialModule R M) m) :
        ℕ →₀ M) =
    (single R (0 + j) : (a : M) → PolynomialModule R M) (r • m)

Tactic:
rw [Function.iterate_zero, zero_add]

Premises used: Function.iterate_zero, zero_add
-- 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
j : ℕ
m : M
⊢ HSMul.hSMul (β := ℕ →₀ M) r (id ((single R j : (a : M) → PolynomialModule R M) m) : ℕ →₀ M) =
    (single R j : (a : M) → PolynomialModule R M) (r • m)

Tactic:
Finsupp.smul_single r j m

Premises used: PolynomialModule, Finsupp.smul_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 : R
j : ℕ
m : M
⊢ HSMul.hSMul (β := ℕ →₀ M) r (id ((single R j : (a : M) → PolynomialModule R M) m) : ℕ →₀ M) =
    (single R j : (a : M) → PolynomialModule R M) (r • m)

Tactic:
exact Finsupp.smul_single r j m

Premises used: Finsupp.smul_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
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    HSMul.hSMul (β := ℕ →₀ M) r
        ((⇑(Finsupp.lmapDomain M R Nat.succ) : (a : ℕ →₀ M) → ℕ →₀ M)^[n]
            ((single R j : (a : M) → PolynomialModule R M) m) :
          ℕ →₀ M) =
      (single R (n + j) : (a : M) → PolynomialModule R M) (r • m)
r : R
j : ℕ
m : M
succ :
  HSMul.hSMul (β := ℕ →₀ M) r
      ((⇑(Finsupp.lmapDomain M R Nat.succ) : (a : ℕ →₀ M) → ℕ →₀ M)^[n]
          ((Finsupp.lmapDomain M R Nat.succ : (a : ℕ →₀ M) → ℕ →₀ M)
            ((single R j : (a : M) → PolynomialModule R M) m)) :
        ℕ →₀ M) =
    HSMul.hSMul (β := ℕ →₀ M) r
      ((⇑(Finsupp.lmapDomain M R Nat.succ) : (a : ℕ →₀ M) → ℕ →₀ M)^[n]
          ((single R (1 + j) : (a : M) → PolynomialModule R M) m) :
        ℕ →₀ M)
⊢ HSMul.hSMul (β := ℕ →₀ M) r
      ((⇑(Finsupp.lmapDomain M R Nat.succ) : (a : ℕ →₀ M) → ℕ →₀ M)^[n + 1]
          ((single R j : (a : M) → PolynomialModule R M) m) :
        ℕ →₀ M) =
    (single R (n + 1 + j) : (a : M) → PolynomialModule R M) (r • m)

Tactic:
rw [Function.iterate_succ, Function.comp_apply, add_assoc, ← hn]

Premises used: Function.iterate_succ, add_assoc, Function.comp_apply
-- 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
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    HSMul.hSMul (β := ℕ →₀ M) r
        ((⇑(Finsupp.lmapDomain M R Nat.succ) : (a : ℕ →₀ M) → ℕ →₀ M)^[n]
            ((single R j : (a : M) → PolynomialModule R M) m) :
          ℕ →₀ M) =
      (single R (n + j) : (a : M) → PolynomialModule R M) (r • m)
r : R
j : ℕ
m : M
succ :
  Eq (α := ℕ →₀ M)
    ((Finsupp.lmapDomain M R Nat.succ : (a : ℕ →₀ M) → ℕ →₀ M) ((single R j : (a : M) → PolynomialModule R M) m) :
      ℕ →₀ M)
    ((single R (1 + j) : (a : M) → PolynomialModule R M) m : PolynomialModule R M)
⊢ HSMul.hSMul (β := ℕ →₀ M) r
      ((⇑(Finsupp.lmapDomain M R Nat.succ) : (a : ℕ →₀ M) → ℕ →₀ M)^[n]
          ((Finsupp.lmapDomain M R Nat.succ : (a : ℕ →₀ M) → ℕ →₀ M)
            ((single R j : (a : M) → PolynomialModule R M) m)) :
        ℕ →₀ M) =
    HSMul.hSMul (β := ℕ →₀ M) r
      ((⇑(Finsupp.lmapDomain M R Nat.succ) : (a : ℕ →₀ M) → ℕ →₀ M)^[n]
          ((single R (1 + j) : (a : M) → PolynomialModule R M) m) :
        ℕ →₀ M)

Tactic:
congr 2
-- 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
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    HSMul.hSMul (β := ℕ →₀ M) r
        ((⇑(Finsupp.lmapDomain M R Nat.succ) : (a : ℕ →₀ M) → ℕ →₀ M)^[n]
            ((single R j : (a : M) → PolynomialModule R M) m) :
          ℕ →₀ M) =
      (single R (n + j) : (a : M) → PolynomialModule R M) (r • m)
r : R
j : ℕ
m : M
succ :
  Eq (α := ℕ →₀ M)
    ((Finsupp.lmapDomain M R Nat.succ : (a : ℕ →₀ M) → ℕ →₀ M) ((single R j : (a : M) → PolynomialModule R M) m) :
      ℕ →₀ M)
    ((single R j.succ : (a : M) → PolynomialModule R M) m : PolynomialModule R M)
⊢ Eq (α := ℕ →₀ M)
    ((Finsupp.lmapDomain M R Nat.succ : (a : ℕ →₀ M) → ℕ →₀ M) ((single R j : (a : M) → PolynomialModule R M) m) :
      ℕ →₀ M)
    ((single R (1 + j) : (a : M) → PolynomialModule R M) m : PolynomialModule R M)

Tactic:
rw [Nat.one_add]

Premises used: Nat.one_add
-- 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
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    HSMul.hSMul (β := ℕ →₀ M) r
        ((⇑(Finsupp.lmapDomain M R Nat.succ) : (a : ℕ →₀ M) → ℕ →₀ M)^[n]
            ((single R j : (a : M) → PolynomialModule R M) m) :
          ℕ →₀ M) =
      (single R (n + j) : (a : M) → PolynomialModule R M) (r • m)
r : R
j : ℕ
m : M
⊢ Eq (α := ℕ →₀ M)
    ((Finsupp.lmapDomain M R Nat.succ : (a : ℕ →₀ M) → ℕ →₀ M) ((single R j : (a : M) → PolynomialModule R M) m) :
      ℕ →₀ M)
    ((single R j.succ : (a : M) → PolynomialModule R M) m : PolynomialModule R M)

Tactic:
Finsupp.mapDomain_single

Premises used: Multiset.sum, Multiset.foldr, Finsupp.mapDomain, Finsupp.sum, Finsupp.mapDomain_single, Finset.sum, 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
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    HSMul.hSMul (β := ℕ →₀ M) r
        ((⇑(Finsupp.lmapDomain M R Nat.succ) : (a : ℕ →₀ M) → ℕ →₀ M)^[n]
            ((single R j : (a : M) → PolynomialModule R M) m) :
          ℕ →₀ M) =
      (single R (n + j) : (a : M) → PolynomialModule R M) (r • m)
r : R
j : ℕ
m : M
⊢ Eq (α := ℕ →₀ M)
    ((Finsupp.lmapDomain M R Nat.succ : (a : ℕ →₀ M) → ℕ →₀ M) ((single R j : (a : M) → PolynomialModule R M) m) :
      ℕ →₀ M)
    ((single R j.succ : (a : M) → PolynomialModule R M) m : PolynomialModule R M)

Tactic:
exact Finsupp.mapDomain_single

Premises used: Finsupp.mapDomain_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 : ℕ
r : R
j : ℕ
m : M
zero :
  ∀ (r : R) (j : ℕ) (m : M),
    HSMul.hSMul (β := ℕ →₀ M) r
        ((⇑(Finsupp.lmapDomain M R Nat.succ) : (a : ℕ →₀ M) → ℕ →₀ M)^[0]
            ((single R j : (a : M) → PolynomialModule R M) m) :
          ℕ →₀ M) =
      (single R (0 + j) : (a : M) → PolynomialModule R M) (r • m)
succ :
  ∀ (n : ℕ)
    (hn :
      ∀ (r : R) (j : ℕ) (m : M),
        HSMul.hSMul (β := ℕ →₀ M) r
            ((⇑(Finsupp.lmapDomain M R Nat.succ) : (a : ℕ →₀ M) → ℕ →₀ M)^[n]
                ((single R j : (a : M) → PolynomialModule R M) m) :
              ℕ →₀ M) =
          (single R (n + j) : (a : M) → PolynomialModule R M) (r • m))
    (r : R) (j : ℕ) (m : M),
    HSMul.hSMul (β := ℕ →₀ M) r
        ((⇑(Finsupp.lmapDomain M R Nat.succ) : (a : ℕ →₀ M) → ℕ →₀ M)^[n + 1]
            ((single R j : (a : M) → PolynomialModule R M) m) :
          ℕ →₀ M) =
      (single R (n + 1 + j) : (a : M) → PolynomialModule R M) (r • m)
⊢ HSMul.hSMul (β := ℕ →₀ M) r
      ((⇑(Finsupp.lmapDomain M R Nat.succ) : (a : ℕ →₀ M) → ℕ →₀ M)^[i]
          ((single R j : (a : M) → PolynomialModule R M) m) :
        ℕ →₀ M) =
    (single R (i + j) : (a : M) → PolynomialModule R M) (r • m)

Tactic:
induction i generalizing r j m with
  | zero =>
    rw [Function.iterate_zero, zero_add]
    exact Finsupp.smul_single r j m
  | succ n hn =>
    rw [Function.iterate_succ, Function.comp_apply, add_assoc, ← hn]
    congr 2
    rw [Nat.one_add]
    exact Finsupp.mapDomain_single

Premises used: Function.iterate_succ, add_assoc, Function.iterate_zero, Finsupp.mapDomain_single, zero_add, Function.comp_apply, Nat.one_add, Finsupp.smul_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 : ℕ
r : R
j : ℕ
m : M
⊢ HSMul.hSMul (α := R[X]) (β := PolynomialModule R M) ((monomial i : (a : R) → R[X]) r : R[X])
      ((lsingle R j : (a : M) → PolynomialModule R M) m : PolynomialModule R M) =
    (lsingle R (i + j) : (a : M) → PolynomialModule R M) (r • m)

Tactic:
monomial_smul_single ..

Premises used: PolynomialModule.monomial_smul_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
i : ℕ
r : R
n : ℕ
⊢ (HSMul.hSMul (α := R[X]) (β := PolynomialModule R M) ((monomial i : (a : R) → R[X]) r : R[X]) 0 : (a : ℕ) → M) n =
    if i ≤ n then HSMul.hSMul (β := M) r ((0 : (a : ℕ) → M) (n - i) : M) else 0

Tactic:
simp only [smul_zero, zero_apply, ite_self]

Premises used: ite_self, smul_zero, PolynomialModule.zero_apply