-- Lean 4 proof step from Mathlib.RingTheory.Extension.Cotangent.Basis (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
σ_1 : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x : P.Ring
y : MvPolynomial ι R
z : P.Ring
⊢ HSMul.hSMul (β := S)
      (HSMul.hSMul (β := D.T) x
        ((Ideal.Quotient.mk
                (Ideal.span
                  (Set.range (ι := σ)
                    (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                      D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
              (a : MvPolynomial ι R) →
                MvPolynomial ι R ⧸
                  Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
            y :
          HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
            (Ideal.span
              (Set.range (ι := σ)
                (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                  D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))))
      ((algebraMap P.Ring S : (a : P.Ring) → S) z : S) =
    x •
      HSMul.hSMul (α := D.T) (β := S)
        ((Ideal.Quotient.mk
                (Ideal.span
                  (Set.range (ι := σ)
                    (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                      D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
              (a : MvPolynomial ι R) →
                MvPolynomial ι R ⧸
                  Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
            y :
          HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
            (Ideal.span
              (Set.range (ι := σ)
                (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                  D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
        ((algebraMap P.Ring S : (a : P.Ring) → S) z : S)
have simp : HMul.hMul (β := S)
    (HMul.hMul (α := S) (β := S)
      ((algebraMap D.T S : (a : D.T) → S) ((algebraMap P.Ring D.T : (a : P.Ring) → D.T) x : D.T) : S)
      ((algebraMap D.T S : (a : D.T) → S)
          ((Ideal.Quotient.mk
                  (Ideal.span
                    (Set.range (ι := σ)
                      (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                        D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
                (a : MvPolynomial ι R) →
                  MvPolynomial ι R ⧸
                    Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
              y :
            HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
              (Ideal.span
                (Set.range (ι := σ)
                  (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                    D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))) :
        S))
    ((aeval P.val : (a : MvPolynomial ι R) → S) z : S) =
  HMul.hMul (β := S)
    (HMul.hMul (α := S) (β := S) ((aeval P.val : (a : MvPolynomial ι R) → S) x : S)
      ((algebraMap D.T S : (a : D.T) → S)
          ((Ideal.Quotient.mk
                  (Ideal.span
                    (Set.range (ι := σ)
                      (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                        D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) :
                (a : MvPolynomial ι R) →
                  MvPolynomial ι R ⧸
                    Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))
              y :
            HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal (MvPolynomial ι R))
              (Ideal.span
                (Set.range (ι := σ)
                  (Subtype.val (p := fun (x : P.toExtension.Ring) ↦ x ∈ P.toExtension.ker) ∘
                    D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent))))) :
        S))
    ((aeval P.val : (a : MvPolynomial ι R) → S) z : S)
Tactic: simp only [Algebra.smul_def, map_mul, Generators.algebraMap_apply, ← mul_assoc]