-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (hypothesis)
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
this_1 : Fintype σ := 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₀))
have 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
Tactic: 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
Cleared hypotheses: this