-- Module: Mathlib.RingTheory.MvPolynomial.EulerIdentity
Goal:
R : Type u_1
σ : Type u_2
inst : CommSemiring R
φ : MvPolynomial σ R
inst_1 : Fintype σ
n : ℕ
w : σ → ℕ
h :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) φ
p q : MvPolynomial σ R
h_1 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) p
h_2 :
  Membership.mem (γ := Submodule R (MvPolynomial σ R))
    (Submodule.span R ((fun (i : σ →₀ ℕ) ↦ single i 1) '' {d : σ →₀ ℕ | (weight w : (a : σ →₀ ℕ) → ℕ) d = n})) q
hp :
  ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) =
    n • p
hq :
  ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R) =
    n • q
refine_3 :
  ∑ x : σ,
      w x •
        (X x *
          HAdd.hAdd (α := MvPolynomial σ R) (β := MvPolynomial σ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R)) =
    n • (p + q)
refine_3₁ :
  ∑ x : σ,
      w x •
        (HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) +
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R)) =
    n • (p + q)
refine_3₂ :
  ∑ x : σ,
      (w x •
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) +
        w x •
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R)) =
    n • p + n • q
refine_3₃ :
  HAdd.hAdd (α := MvPolynomial σ R)
      (∑ x : σ,
        w x •
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R))
      (∑ x : σ,
        w x •
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R)) =
    n • p + n • q
refine_3₄ :
  n • p +
      ∑ x : σ,
        w x •
          HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X x)
            ((pderiv x : (a : MvPolynomial σ R) → MvPolynomial σ R) q : MvPolynomial σ R) =
    n • p + n • q
⊢ ∑ i : σ,
      w i •
        HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R) (X i)
          ((pderiv i : (a : MvPolynomial σ R) → MvPolynomial σ R) (p + q) : MvPolynomial σ R) =
    n • (p + q)

Tactic:
simp_rw [map_add, left_distrib, smul_add, sum_add_distrib, hp, hq]

Premises used: Finset.sum_add_distrib, map_add, smul_add, left_distrib