-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Derivation (goal)
Goal:
σ : Type u_1
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid A
inst_2 : Module R A
inst_3 : Module (MvPolynomial σ R) A
inst_4 : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) 1 : A) (0 : A)
H :
  ∀ (s : σ →₀ ℕ) (i : σ),
    (D : (a : MvPolynomial σ R) → A)
        (HMul.hMul (α := MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial σ R) 1) (X i)) =
      HSMul.hSMul (α := MvPolynomial σ R) (β := A) ((monomial s : (a : R) → MvPolynomial σ R) 1)
          ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i)
          ((D : (a : MvPolynomial σ R) → A) ((monomial s : (a : R) → MvPolynomial σ R) 1) : A)
hC :
  ∀ (r : R),
    Eq.{u_3 + 1} (α := A) ((D : (a : MvPolynomial σ R) → A) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) : A)
      (0 : A)
this :
  ∀ (p : MvPolynomial σ R) (i : σ),
    (D : (a : MvPolynomial σ R) → A) (p * X i) =
      HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) p : A)
p q : MvPolynomial σ R
i : σ
hq :
  (D : (a : MvPolynomial σ R) → A) (p * q) =
    HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q : A) +
      HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) p : A)
mul_X :
  p • HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
      (p • HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) q : A) +
        HSMul.hSMul (α := MvPolynomial σ R) (X i) (HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) p : A))) =
    p • HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
      (p • HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) q : A) +
        q • HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) p : A))
⊢ p • HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
      (HSMul.hSMul (α := MvPolynomial σ R) (X i) (HSMul.hSMul (β := A) p ((D : (a : MvPolynomial σ R) → A) q : A)) +
        HSMul.hSMul (α := MvPolynomial σ R) (X i) (HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) p : A))) =
    p • HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
      (p • HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) q : A) +
        q • HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) p : A))
have mul_X₁ : p • HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
    (p • HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) q : A) +
      q • HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) p : A)) =
  p • HSMul.hSMul (β := A) q ((D : (a : MvPolynomial σ R) → A) (X i) : A) +
    (p • HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) q : A) +
      q • HSMul.hSMul (α := MvPolynomial σ R) (β := A) (X i) ((D : (a : MvPolynomial σ R) → A) p : A))
Tactic: rw [smul_comm (X i), smul_comm (X i)]