-- 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
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst_3 : Nontrivial S
this :
  Nontrivial
    (HasQuotient.Quotient (MvPolynomial ι R) (B := Ideal P.Ring)
      (Ideal.span
        (Set.range (ι := σ)
          (Subtype.val (p := fun (x : P.Ring) ↦ x ∈ P.toExtension.ker) ∘
            D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))))
h :
  (Hom.toAlgHom
          (ofComp (localizationAway S D.gbar)
            (Presentation.naive
                (fun
                    (x :
                      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))))) ↦
                  if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x)
                ⋯).toGenerators) :
        (a :
            ((localizationAway S D.gbar).comp
                (Presentation.naive
                    (fun
                        (x :
                          MvPolynomial ι R ⧸
                            Ideal.span (Set.range (Subtype.val ∘ D.f ∘ (⇑b : (a : σ) → P.toExtension.Cotangent)))) ↦
                      if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x)
                    ⋯).toGenerators).Ring) →
          (localizationAway S D.gbar).Ring)
      (HMul.hMul (α := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R) (β := MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
          ((rename Sum.inr : (a : MvPolynomial ι R) → MvPolynomial (Unit ⊕ ι) R)
              ((Presentation.naive
                    (fun
                        (x :
                          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))))) ↦
                      if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x)
                    ⋯).σ
                D.gbar) :
            MvPolynomial.{u_4, u_1} (Unit ⊕ ι) R)
          (X (Sum.inl ())) -
        1) =
    HMul.hMul (α := MvPolynomial Unit D.T) (β := MvPolynomial Unit D.T)
        ((C : (a : D.T) → MvPolynomial Unit D.T) D.gbar : MvPolynomial Unit D.T) (X ()) -
      1
h₁ :
  (Presentation.naive
          (fun
              (x :
                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))))) ↦
            if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x)
          ⋯).σ
      (-1) =
    -1
h₂ :
  (Presentation.naive
          (fun
              (x :
                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))))) ↦
            if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x)
          ⋯).σ
      0 =
    0
⊢ (Hom.toAlgHom (ofComp (localizationAway S D.gbar) D.presLeft.toGenerators) :
        (a : ((localizationAway S D.gbar).comp D.presLeft.toGenerators).Ring) → (localizationAway S D.gbar).Ring)
      (D.pres.relation (Sum.inl ())) =
    HMul.hMul (α := MvPolynomial Unit D.T) (β := MvPolynomial Unit D.T)
        ((C : (a : D.T) → MvPolynomial Unit D.T) D.gbar : MvPolynomial Unit D.T) (X ()) -
      1

Tactic:
rw [pres, presLeft, presRight, Presentation.relation_comp_localizationAway_inl]

Premises used: _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.presLeft, _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.presRight, _private.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.pres, Algebra.Presentation.relation_comp_localizationAway_inl