-- 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
z : S
y : MvPolynomial ι R
obtain :
  ∀ (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)
⊢ 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))))) •
      z =
    x •
      HSMul.hSMul (α := D.T)
        ((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)))))
        z

Tactic:
obtain ⟨z, rfl⟩ := P.algebraMap_surjective z

Premises used: Algebra.Generators.algebraMap_surjective, rfl