awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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
⊢ (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])
have zero : (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: induction x using induction_linear with
      | zero => rw [smul_zero, map_zero, mul_zero]
      | add _ _ hp hq => rw [smul_add, map_add, map_add, mul_add, hp, hq]
      | single n a =>
        ext i
        simp_rw [toFinsuppIso_symm_apply, coeff_ofFinsupp, coeff_mul, smul_single_apply,
          smul_eq_mul, coeff_ofFinsupp, single_apply, mul_ite, mul_zero]
        split_ifs with hn
        · rw [Finset.sum_eq_single (i - n, n)]
          · simp only [ite_true]
          · rintro ⟨p, q⟩ hpq1 hpq2
            rw [Finset.mem_antidiagonal] at hpq1
            split_ifs with H
            · dsimp at H
              exfalso
              apply hpq2
              rw [← hpq1, H]
              simp only [add_tsub_cancel_right]
            · rfl
          · intro H
            exfalso
            apply H
            rw [Finset.mem_antidiagonal, tsub_add_cancel_of_le hn]
        · symm
          rw [Finset.sum_ite_of_false, Finset.sum_const_zero]
          grind [Finset.mem_antidiagonal]
Cleared hypotheses: x
-- 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 : 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
zero :
  (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
⊢ (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])
have add : ∀ (f g : PolynomialModule R R)
  (hp :
    (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f) =
      HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) f : R[X]))
  (hq :
    (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • g) =
      HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) g : R[X])),
  (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • (f + g)) =
    HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (f + g) : R[X])
Tactic: induction x using induction_linear with
      | zero => rw [smul_zero, map_zero, mul_zero]
      | add _ _ hp hq => rw [smul_add, map_add, map_add, mul_add, hp, hq]
      | single n a =>
        ext i
        simp_rw [toFinsuppIso_symm_apply, coeff_ofFinsupp, coeff_mul, smul_single_apply,
          smul_eq_mul, coeff_ofFinsupp, single_apply, mul_ite, mul_zero]
        split_ifs with hn
        · rw [Finset.sum_eq_single (i - n, n)]
          · simp only [ite_true]
          · rintro ⟨p, q⟩ hpq1 hpq2
            rw [Finset.mem_antidiagonal] at hpq1
            split_ifs with H
            · dsimp at H
              exfalso
              apply hpq2
              rw [← hpq1, H]
              simp only [add_tsub_cancel_right]
            · rfl
          · intro H
            exfalso
            apply H
            rw [Finset.mem_antidiagonal, tsub_add_cancel_of_le hn]
        · symm
          rw [Finset.sum_ite_of_false, Finset.sum_const_zero]
          grind [Finset.mem_antidiagonal]
Cleared hypotheses: x
-- 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 : 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
zero :
  (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
add :
  ∀ (f g : PolynomialModule R R)
    (hp :
      (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • f) =
        HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) f : R[X]))
    (hq :
      (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • g) =
        HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) g : R[X])),
    (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (r • (f + g)) =
      HMul.hMul (β := R[X]) r ((RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X]) (f + g) : R[X])
⊢ (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])
have single : ∀ (n : ℕ) (a : R),
  (RingEquiv.symm (toFinsuppIso R) : (a : AddMonoidAlgebra R ℕ) → R[X])
      (HSMul.hSMul (β := PolynomialModule R R) r
        ((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])
          ((single R n : (a : R) → PolynomialModule R R) a) :
        R[X])
Tactic: induction x using induction_linear with
      | zero => rw [smul_zero, map_zero, mul_zero]
      | add _ _ hp hq => rw [smul_add, map_add, map_add, mul_add, hp, hq]
      | single n a =>
        ext i
        simp_rw [toFinsuppIso_symm_apply, coeff_ofFinsupp, coeff_mul, smul_single_apply,
          smul_eq_mul, coeff_ofFinsupp, single_apply, mul_ite, mul_zero]
        split_ifs with hn
        · rw [Finset.sum_eq_single (i - n, n)]
          · simp only [ite_true]
          · rintro ⟨p, q⟩ hpq1 hpq2
            rw [Finset.mem_antidiagonal] at hpq1
            split_ifs with H
            · dsimp at H
              exfalso
              apply hpq2
              rw [← hpq1, H]
              simp only [add_tsub_cancel_right]
            · rfl
          · intro H
            exfalso
            apply H
            rw [Finset.mem_antidiagonal, tsub_add_cancel_of_le hn]
        · symm
          rw [Finset.sum_ite_of_false, Finset.sum_const_zero]
          grind [Finset.mem_antidiagonal]
Cleared hypotheses: x
-- 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' : 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]
⊢ ((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)
have 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)
Tactic: rw [smul_zero, map_zero, smul_zero]
-- 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' : 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)
⊢ ((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)
have zero₁ : 0 = HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p) 0
Tactic: rw [smul_zero, map_zero, smul_zero]
-- 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' : 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
⊢ ((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)
have zero₂ : Eq.{u_5 + 1} (α := PolynomialModule R' M') 0 0
Tactic: rw [smul_zero, map_zero, smul_zero]
-- 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' : 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_1 : M →ₗ[R] M'
p : R[X]
f g : PolynomialModule R M
e₁ :
  ((map R' f_1 : 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')
      (p • f) =
    HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p)
      (((map R' f_1 : 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')
          f :
        PolynomialModule R' M')
e₂ :
  ((map R' f_1 : 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')
      (p • g) =
    HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p)
      (((map R' f_1 : 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')
          g :
        PolynomialModule R' M')
⊢ ((map R' f_1 : 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')
      (p • (f + g)) =
    HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p)
      (((map R' f_1 : 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')
          (f + g) :
        PolynomialModule R' M')
have add : ((map R' f_1 : 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')
    (p • f + p • g) =
  HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M') (Polynomial.map (algebraMap R R') p)
    (((map R' f_1 : 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')
        (f + g) :
      PolynomialModule R' M')
Tactic: rw [smul_add, map_add, e₁, e₂, map_add, smul_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
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'
i : ℕ
m : M
n : ℕ
a : R
⊢ ((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 (α := R[X]) (β := PolynomialModule R M) ((monomial n : (a : R) → R[X]) a : R[X])
        ((single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
    HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M')
      (Polynomial.map (algebraMap R R') ((monomial n : (a : R) → R[X]) a))
      (((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')
have single : ((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 (n + i) : (a : M) → PolynomialModule R M) (a • m)) =
  HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M')
    (Polynomial.map (algebraMap R R') ((monomial n : (a : R) → R[X]) a))
    (((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')
Tactic: rw [monomial_smul_single, map_single, Polynomial.map_monomial, map_single,
        monomial_smul_single, f.map_smul, algebraMap_smul]
-- 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' : 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'
i : ℕ
m : M
n : ℕ
a : R
single :
  ((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')
      ((PolynomialModule.single R (n + i) : (a : M) → PolynomialModule R M) (a • m)) =
    HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M')
      (Polynomial.map (algebraMap R R') ((monomial n : (a : R) → R[X]) a))
      (((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')
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m) :
        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')
      (HSMul.hSMul (α := R[X]) (β := PolynomialModule R M) ((monomial n : (a : R) → R[X]) a : R[X])
        ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
    HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M')
      (Polynomial.map (algebraMap R R') ((monomial n : (a : R) → R[X]) a))
      (((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')
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m) :
        PolynomialModule R' M')
have single₁ : (PolynomialModule.single R' (n + i) : (a : M') → PolynomialModule R' M') ((f : (a : M) → M') (a • m)) =
  HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M')
    (Polynomial.map (algebraMap R R') ((monomial n : (a : R) → R[X]) a))
    (((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')
        ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m) :
      PolynomialModule R' M')
Tactic: rw [monomial_smul_single, map_single, Polynomial.map_monomial, map_single,
        monomial_smul_single, f.map_smul, algebraMap_smul]
-- 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' : 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'
i : ℕ
m : M
n : ℕ
a : R
single :
  ((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')
      ((PolynomialModule.single R (n + i) : (a : M) → PolynomialModule R M) (a • m)) =
    HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M')
      (Polynomial.map (algebraMap R R') ((monomial n : (a : R) → R[X]) a))
      (((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')
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m) :
        PolynomialModule R' M')
single₁ :
  (PolynomialModule.single R' (n + i) : (a : M') → PolynomialModule R' M') ((f : (a : M) → M') (a • m)) =
    HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M')
      (Polynomial.map (algebraMap R R') ((monomial n : (a : R) → R[X]) a))
      (((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')
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m) :
        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')
      (HSMul.hSMul (α := R[X]) (β := PolynomialModule R M) ((monomial n : (a : R) → R[X]) a : R[X])
        ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m : PolynomialModule R M)) =
    HSMul.hSMul (α := R'[X]) (β := PolynomialModule R' M')
      (Polynomial.map (algebraMap R R') ((monomial n : (a : R) → R[X]) a))
      (((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')
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m) :
        PolynomialModule R' M')
have single₂ : (PolynomialModule.single R' (n + i) : (a : M') → PolynomialModule R' M') ((f : (a : M) → M') (a • m)) =
  HSMul.hSMul.{u_4, u_5, u_5} (α := R'[X]) (β := PolynomialModule R' M')
    ((monomial n : (a : R') → R'[X]) ((algebraMap R R' : (a : R) → R') a) : R'[X])
    (((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')
        ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m) :
      PolynomialModule R' M')
Tactic: rw [monomial_smul_single, map_single, Polynomial.map_monomial, map_single,
        monomial_smul_single, f.map_smul, algebraMap_smul]
-- 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' : 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]
q : 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')
      (p • q) =
    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')
          q :
        PolynomialModule R' M')
have 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')
    (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: induction q using induction_linear with
  | zero => rw [smul_zero, map_zero, smul_zero]
  | add f g e₁ e₂ => rw [smul_add, map_add, e₁, e₂, map_add, smul_add]
  | single i m =>
    induction p using Polynomial.induction_on' with
    | add _ _ e₁ e₂ => rw [add_smul, map_add, e₁, e₂, Polynomial.map_add, add_smul]
    | monomial => rw [monomial_smul_single, map_single, Polynomial.map_monomial, map_single,
        monomial_smul_single, f.map_smul, algebraMap_smul]
Cleared hypotheses: q
-- 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 : 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)
have refine_1 : ∀ (i : ℕ), HSMul.hSMul (β := M) (r ^ i) 0 = 0
Tactic: refine (Finsupp.sum_smul_index' ?_).trans ?_