awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
Goal:
R : Type u_3
A : Type u_1
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
inst_7 : FaithfulSMul A M
p : R[X]
⊢ (∀ (m : AEval R M a), p • m = 0) ↔ Eq.{u_1 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
have h : (∀ (m : M), HSMul.hSMul.{u_1, u_2, u_2} (α := A) ((aeval a : (a : R[X]) → A) p : A) m = 0) ↔
  Eq.{u_1 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
Tactic: change (∀ m : M, aeval a p • m = 0) ↔ _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
Goal:
R : Type u_3
A : Type u_1
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
inst_7 : FaithfulSMul A M
⊢ Eq (α := Ideal R[X]) (Submodule.annihilator.{u_3, u_2} (M := AEval R M a) ⊤)
    (RingHom.ker (F := R[X] →ₐ[R] A) (aeval a))
have h : ∀ (p : R[X]),
  Membership.mem (γ := Ideal R[X]) (Submodule.annihilator.{u_3, u_2} (M := AEval R M a) ⊤) p ↔
    Membership.mem (γ := Ideal R[X]) (RingHom.ker (F := R[X] →ₐ[R] A) (aeval a)) p
Tactic: ext p
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
Goal:
R : Type u_3
A : Type u_1
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
inst_7 : FaithfulSMul A M
p : R[X]
⊢ Membership.mem (γ := Ideal R[X]) (Submodule.annihilator.{u_3, u_2} (M := AEval R M a) ⊤) p ↔
    Membership.mem (γ := Ideal R[X]) (RingHom.ker (F := R[X] →ₐ[R] A) (aeval a)) p
have h : (∀ (n : AEval R M a), p • n = 0) ↔ Eq.{u_1 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
Tactic: simp only [Submodule.mem_annihilator, Submodule.mem_top, forall_true_left, RingHom.mem_ker]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
Goal:
R : Type u_3
A : Type u_1
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
inst_7 : FaithfulSMul A M
p : R[X]
⊢ (∀ (n : AEval R M a), p • n = 0) ↔ Eq.{u_1 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
have h : (∀ (m : M), HSMul.hSMul.{u_1, u_2, u_2} (α := A) ((aeval a : (a : R[X]) → A) p : A) m = 0) ↔
  Eq.{u_1 + 1} (α := A) ((aeval a : (a : R[X]) → A) p : A) (0 : A)
Tactic: change (∀ m : M, aeval a p • m = 0) ↔ _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
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 : ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))
⊢ (fun (q : Submodule.{u_1, u_3} 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)
            ((OrderIso.symm (Submodule.orderIsoMapComap (of R M a)) : (a : Submodule R (AEval R M a)) → Submodule R M)
              (Submodule.restrictScalars R q))
            ⋯ :
          ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))))
      ((fun (p : ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))) ↦
          let __AddSubmonoid : AddSubmonoid (AEval R M a) :=
            AddSubmonoid.map (F := M ≃ₗ[R] AEval R M a) (of R M a) (↑p : Submodule R M).toAddSubmonoid;
          { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ : Submodule.{u_1, u_3} R[X] (AEval R M a) })
        p) =
    p
have a₁ : ∀ (x : M),
  Membership.mem (γ := Submodule R M)
      (↑((fun (q : Submodule.{u_1, u_3} 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)
                  ((OrderIso.symm (Submodule.orderIsoMapComap (of R M a)) :
                      (a : Submodule R (AEval R M a)) → Submodule R M)
                    (Submodule.restrictScalars R q))
                  sorry :
                ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))))
            ((fun (p : ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))) ↦
                let __AddSubmonoid : AddSubmonoid (AEval R M a) :=
                  AddSubmonoid.map (F := M ≃ₗ[R] AEval R M a) (of R M a) (↑p : Submodule R M).toAddSubmonoid;
                { toAddSubmonoid := __AddSubmonoid, smul_mem' := sorry : Submodule.{u_1, u_3} R[X] (AEval R M a) })
              p)) :
        Submodule R M)
      x ↔
    x ∈ (↑p : Submodule R M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
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
q : Submodule.{u_1, u_3} R[X] (AEval R M a)
⊢ (fun (p : ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))) ↦
        let __AddSubmonoid : AddSubmonoid (AEval R M a) :=
          AddSubmonoid.map (F := M ≃ₗ[R] AEval R M a) (of R M a) (↑p : Submodule R M).toAddSubmonoid;
        { toAddSubmonoid := __AddSubmonoid, smul_mem' := ⋯ : Submodule.{u_1, u_3} R[X] (AEval R M a) })
      ((fun (q : Submodule.{u_1, u_3} 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)
              ((OrderIso.symm (Submodule.orderIsoMapComap (of R M a)) : (a : Submodule R (AEval R M a)) → Submodule R M)
                (Submodule.restrictScalars R q))
              ⋯ :
            ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))))
        q) =
    q
have h : ∀ (x : AEval R M a),
  Membership.mem (γ := Submodule.{u_1, u_3} R[X] (AEval R M a))
      ((fun (p : ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))) ↦
          let __AddSubmonoid : AddSubmonoid (AEval R M a) :=
            AddSubmonoid.map (F := M ≃ₗ[R] AEval R M a) (of R M a) (↑p : Submodule R M).toAddSubmonoid;
          { toAddSubmonoid := __AddSubmonoid, smul_mem' := sorry : Submodule.{u_1, u_3} R[X] (AEval R M a) })
        ((fun (q : Submodule.{u_1, u_3} 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)
                ((OrderIso.symm (Submodule.orderIsoMapComap (of R M a)) :
                    (a : Submodule R (AEval R M a)) → Submodule R M)
                  (Submodule.restrictScalars R q))
                sorry :
              ↥(End.invtSubmodule ((Algebra.lsmul R R M : (a : A) → End R M) a))))
          q))
      x ↔
    x ∈ q
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.AEval (goal)
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))
⊢ Membership.mem (α := M) p ((LinearEquiv.symm (of R M a) : (a : AEval R M a) → M) (↑x : AEval R M a) : M)
have 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)
Tactic: obtain ⟨x, hx⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (hypothesis)
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[X] (PolynomialModule R M)
have this : 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
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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)
⊢ IsScalarTower.{u_3, u_1, u} S R[X] (PolynomialModule R M)
have smul_assoc : ∀ (x : S) (y : R[X]) (z : PolynomialModule R M), (x • y) • z = x • y • z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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
⊢ (x • y) • z = x • y • z
have smul_assoc : HSMul.hSMul (α := R) ((algebraMap S R : (a : S) → R) x : R) y • z = x • y • z
Tactic: rw [← @IsScalarTower.algebraMap_smul S R, ← @IsScalarTower.algebraMap_smul S R, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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
⊢ (x • y) • z = x • y • z
have 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)
Tactic: rw [← @IsScalarTower.algebraMap_smul S R, ← @IsScalarTower.algebraMap_smul S R, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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)
⊢ (x • y) • z = x • y • z
have 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)
Tactic: rw [← @IsScalarTower.algebraMap_smul S R, ← @IsScalarTower.algebraMap_smul S R, smul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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])
      ((single R j : (a : M) → PolynomialModule R M) m : PolynomialModule R M) =
    (single R (i + j) : (a : M) → PolynomialModule R M) (r • m)
have 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)
Tactic: simp only [Module.End.mul_apply, Polynomial.aeval_monomial, Module.End.pow_apply,
    Module.algebraMap_end_apply, smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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
      ((⇑(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)
have 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)
Tactic: rw [Function.iterate_zero, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [Function.iterate_succ, Function.comp_apply, add_assoc, ← hn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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
⊢ 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)
have 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)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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 (1 + j) : (a : M) → PolynomialModule R M) m : PolynomialModule R M)
have 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)
Tactic: rw [Nat.one_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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 (β := ℕ →₀ 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)
have 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)
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
Cleared hypotheses: i, r, j, m
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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)
⊢ 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)
have 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)
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
Cleared hypotheses: i, r, j, m
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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 : ℕ
p q : PolynomialModule R M
hp :
  (HSMul.hSMul (α := R[X]) ((monomial i : (a : R) → R[X]) r : R[X]) p : (a : ℕ) → M) n =
    if i ≤ n then HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) else 0
hq :
  (HSMul.hSMul (α := R[X]) ((monomial i : (a : R) → R[X]) r : R[X]) q : (a : ℕ) → M) n =
    if i ≤ n then HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M) else 0
⊢ (HSMul.hSMul (α := R[X]) ((monomial i : (a : R) → R[X]) r : R[X]) (p + q) : (a : ℕ) → M) n =
    if i ≤ n then HSMul.hSMul (β := M) r ((p + q : (a : ℕ) → M) (n - i) : M) else 0
have add : ((if i ≤ n then HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) else 0) +
    if i ≤ n then HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M) else 0) =
  if i ≤ n then
    HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) + HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M)
  else 0
Tactic: simp only [smul_add, add_apply, hp, hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.Basic (goal)
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 : ℕ
p q : PolynomialModule R M
hp :
  (HSMul.hSMul (α := R[X]) ((monomial i : (a : R) → R[X]) r : R[X]) p : (a : ℕ) → M) n =
    if i ≤ n then HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) else 0
hq :
  (HSMul.hSMul (α := R[X]) ((monomial i : (a : R) → R[X]) r : R[X]) q : (a : ℕ) → M) n =
    if i ≤ n then HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M) else 0
⊢ ((if i ≤ n then HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) else 0) +
      if i ≤ n then HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M) else 0) =
    if i ≤ n then
      HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) + HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M)
    else 0
have pos : i ≤ n →
  HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) + HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M) =
    HSMul.hSMul (β := M) r ((p : (a : ℕ) → M) (n - i) : M) + HSMul.hSMul (β := M) r ((q : (a : ℕ) → M) (n - i) : M)
Tactic: split_ifs