-- Module: Mathlib.RingTheory.Extension.Cotangent.Basis
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
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)
⊢ 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)

Tactic:
simp only [Algebra.smul_def, map_mul, Generators.algebraMap_apply, ← mul_assoc]

Premises used: Algebra.Generators.algebraMap_apply, mul_assoc, map_mul, Algebra.smul_def