-- 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]
i : ℕ
m : M
single :
  ∀ (p q : R[X])
    (e₁ :
      ((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
            ((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') 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')
              ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m) :
            PolynomialModule R' M'))
    (e₂ :
      ((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) q
            ((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') q)
          (((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 (β := PolynomialModule R M) (p + q)
          ((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') (p + q))
        (((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₁ :
  ∀ (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])
          ((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')
⊢ ((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
        ((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') 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')
          ((PolynomialModule.single R i : (a : M) → PolynomialModule R M) m) :
        PolynomialModule R' M')

Tactic:
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]

Premises used: PolynomialModule.monomial_smul_single, Polynomial.map_monomial, Polynomial.map_add, map_add, Polynomial.monomial, algebraMap_smul, add_smul, LinearMap.map_smul, PolynomialModule.map_single