-- 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
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])
single :
  ∀ (n : ℕ) (a : R),
    (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])
⊢ (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])

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]

Premises used: Polynomial.coeff_ofFinsupp, smul_zero, PolynomialModule.single_apply, mul_ite, map_zero, Polynomial.coeff_mul, PolynomialModule.single, map_add, ite_true, Finset.sum_const_zero, MulZeroClass.mul_zero, PolynomialModule.smul_single_apply, Finset.sum_ite_of_false, Finset.HasAntidiagonal.mem_antidiagonal, mul_add, Polynomial.toFinsuppIso_symm_apply, add_tsub_cancel_right, smul_eq_mul, smul_add