-- Module: Mathlib.RingTheory.Extension.Presentation.Core
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P_1 : Presentation R S ι σ
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
R₀ : Type u_5
inst_4 : CommRing R₀
inst_5 : Algebra R₀ R
inst_6 : Algebra R₀ S
inst_7 : IsScalarTower R₀ R S
inst_8 : P.HasCoeffs R₀
inst_9 : FaithfulSMul R₀ R
let let₁ let₂ :
  IsUnit (M :=
    Presentation.ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P.toPresentation)
      R₀)
    (PreSubmersivePresentation.jacobian (P.ofHasCoeffs R₀))
let₃ :
  let this := Fintype.ofFinite σ;
  ∀
    (this :
      Eq (α :=
        HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
          (Ideal.span
            (Set.range (ι := σ)
              (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                R₀))))
        ((Ideal.Quotient.mk
                (Ideal.span
                  (Set.range (ι := σ)
                    (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P :=
                      P.toPresentation) R₀))) :
              (a : MvPolynomial ι R₀) →
                MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))
            (∑ i : σ,
              HMul.hMul (α := MvPolynomial ι R₀) (P.jacobianRelationsOfHasCoeffs R₀ i)
                (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation) R₀
                  i)) :
          HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
            (Ideal.span
              (Set.range (ι := σ)
                (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                  R₀))))
        ((Ideal.Quotient.mk
                (Ideal.span
                  (Set.range (ι := σ)
                    (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P :=
                      P.toPresentation) R₀))) :
              (a : MvPolynomial ι R₀) →
                MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))
            (HMul.hMul (α := MvPolynomial ι R₀) (P.jacobianOfHasCoeffs R₀) (P.invJacobianOfHasCoeffs R₀) - 1) :
          HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
            (Ideal.span
              (Set.range (ι := σ)
                (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                  R₀))))),
    IsUnit (M :=
      Presentation.ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P :=
        P.toPresentation) R₀)
      (PreSubmersivePresentation.jacobian (P.ofHasCoeffs R₀))
let₄ :
  ∀
    (this :
      HMul.hMul (α :=
          HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
            (Ideal.span
              (Set.range (ι := σ)
                (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                  R₀))))
          (β :=
          HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
            (Ideal.span
              (Set.range (ι := σ)
                (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                  R₀))))
          ((Ideal.Quotient.mk
                  (Ideal.span
                    (Set.range (ι := σ)
                      (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P :=
                        P.toPresentation) R₀))) :
                (a : MvPolynomial ι R₀) →
                  MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))
              (P.jacobianOfHasCoeffs R₀) :
            HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
              (Ideal.span
                (Set.range (ι := σ)
                  (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                    R₀))))
          ((Ideal.Quotient.mk
                  (Ideal.span
                    (Set.range (ι := σ)
                      (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P :=
                        P.toPresentation) R₀))) :
                (a : MvPolynomial ι R₀) →
                  MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))
              (P.invJacobianOfHasCoeffs R₀) :
            HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
              (Ideal.span
                (Set.range (ι := σ)
                  (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                    R₀)))) =
        1),
    IsUnit (M :=
      Presentation.ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P :=
        P.toPresentation) R₀)
      (PreSubmersivePresentation.jacobian (P.ofHasCoeffs R₀))
h :
  ∀
    (this :
      HMul.hMul (α :=
          HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
            (Ideal.span
              (Set.range (ι := σ)
                (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                  R₀))))
          (β :=
          HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
            (Ideal.span
              (Set.range (ι := σ)
                (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                  R₀))))
          ((Ideal.Quotient.mk
                  (Ideal.span
                    (Set.range (ι := σ)
                      (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P :=
                        P.toPresentation) R₀))) :
                (a : MvPolynomial ι R₀) →
                  MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))
              (P.jacobianOfHasCoeffs R₀) :
            HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
              (Ideal.span
                (Set.range (ι := σ)
                  (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                    R₀))))
          ((Ideal.Quotient.mk
                  (Ideal.span
                    (Set.range (ι := σ)
                      (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P :=
                        P.toPresentation) R₀))) :
                (a : MvPolynomial ι R₀) →
                  MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))
              (P.invJacobianOfHasCoeffs R₀) :
            HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
              (Ideal.span
                (Set.range (ι := σ)
                  (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                    R₀)))) =
        1),
    Eq (α :=
      Presentation.ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P :=
        P.toPresentation) R₀)
      (PreSubmersivePresentation.jacobian (P.ofHasCoeffs R₀))
      ((Ideal.Quotient.mk
            (Ideal.span
              (Set.range (ι := σ)
                (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                  R₀))) :
          (a : MvPolynomial ι R₀) → MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))
        (P.jacobianOfHasCoeffs R₀))
h₁ :
  let this := Fintype.ofFinite σ;
  ∀
    (this_1 :
      HMul.hMul (α :=
          HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
            (Ideal.span
              (Set.range (ι := σ)
                (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                  R₀))))
          (β :=
          HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
            (Ideal.span
              (Set.range (ι := σ)
                (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                  R₀))))
          ((Ideal.Quotient.mk
                  (Ideal.span
                    (Set.range (ι := σ)
                      (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P :=
                        P.toPresentation) R₀))) :
                (a : MvPolynomial ι R₀) →
                  MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))
              (P.jacobianOfHasCoeffs R₀) :
            HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
              (Ideal.span
                (Set.range (ι := σ)
                  (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                    R₀))))
          ((Ideal.Quotient.mk
                  (Ideal.span
                    (Set.range (ι := σ)
                      (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P :=
                        P.toPresentation) R₀))) :
                (a : MvPolynomial ι R₀) →
                  MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))
              (P.invJacobianOfHasCoeffs R₀) :
            HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
              (Ideal.span
                (Set.range (ι := σ)
                  (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                    R₀)))) =
        1),
    Eq (α :=
      Presentation.ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P :=
        P.toPresentation) R₀)
      ((algebraMap
              (Generators.Ring (S :=
                Presentation.ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P :=
                  P.toPresentation) R₀)
                (Presentation.toGenerators (PreSubmersivePresentation.toPresentation (P.ofHasCoeffs R₀))))
              (Presentation.ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P :=
                P.toPresentation) R₀) :
            (a : (P.ofHasCoeffs R₀).Ring) → Presentation.ModelOfHasCoeffs R₀)
          (Matrix.det (PreSubmersivePresentation.jacobiMatrix (P.ofHasCoeffs R₀))) :
        Presentation.ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P :=
          P.toPresentation) R₀)
      ((Ideal.Quotient.mk
              (Ideal.span
                (Set.range (ι := σ)
                  (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                    R₀))) :
            (a : MvPolynomial ι R₀) → MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (Presentation.relationOfHasCoeffs R₀)))
          (P.jacobianOfHasCoeffs R₀) :
        HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
          (Ideal.span
            (Set.range (ι := σ)
              (Presentation.relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P.toPresentation)
                R₀))))
⊢ IsUnit (M :=
    Presentation.ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P.toPresentation)
      R₀)
    (PreSubmersivePresentation.jacobian (P.ofHasCoeffs R₀))

Tactic:
classical
    let : Fintype σ := Fintype.ofFinite _
    have := congr((Ideal.Quotient.mk _ : _ →+* P.ModelOfHasCoeffs R₀)
      $(P.sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs R₀))
    simp only [map_sum, map_mul, Ideal.Quotient.mk_span_range, mul_zero, Finset.sum_const_zero,
      map_sub, map_one, @eq_comm (P.ModelOfHasCoeffs R₀) 0, sub_eq_zero] at this
    convert! IsUnit.of_mul_eq_one _ this
    rw [PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det]
    simp [jacobianOfHasCoeffs]

Premises used: map_sub, sub_eq_zero, Ideal.Quotient.mk_span_range, map_sum, eq_comm, Finset.sum_const_zero, MulZeroClass.mul_zero, map_mul, map_one, Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det, Algebra.SubmersivePresentation.jacobianOfHasCoeffs