-- 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 : Presentation R S ι σ
R₀ : Type u_5
inst_3 : CommRing R₀
inst_4 : Algebra R₀ R
inst_5 : Algebra R₀ S
inst_6 : IsScalarTower R₀ R S
inst_7 : P.HasCoeffs R₀
h :
  Function.Surjective (α := P.Ring) (β := S)
    (⇑(AlgHom.comp (↑(AlgEquiv.restrictScalars R P.quotientEquiv) : P.Quotient →ₐ[R] S) (Ideal.Quotient.mkₐ R P.ker)) :
      (a : P.Ring) → S)
hf :
  ∀ (x : ι),
    Eq.{u_2 + 1} (α := S)
      ((AlgHom.comp (B :=
              R ⊗[R₀] ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀)
              (P.tensorModelOfHasCoeffsHom R₀)
              (AlgHom.comp
                (Ideal.Quotient.liftₐ P.ker
                  (AlgHom.comp (B := R ⊗[R₀] MvPolynomial ι R₀)
                    (TensorProduct.map (AlgHom.id R R)
                        (Ideal.Quotient.mkₐ R₀
                          (Ideal.span
                            (Set.range (ι := σ)
                              (relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀)))) :
                      R ⊗[R₀] MvPolynomial ι R₀ →ₐ[R]
                        R ⊗[R₀]
                          HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
                            (Ideal.span
                              (Set.range (ι := σ)
                                (relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀))))
                    ((↑(AlgEquiv.symm (MvPolynomial.algebraTensorAlgEquiv R₀ R)) :
                        MvPolynomial ι R →ₐ[R] R ⊗[R₀] MvPolynomial ι R₀) :
                      MvPolynomial ι R →ₐ[R] R ⊗[R₀] MvPolynomial ι R₀))
                  ⋯)
                (Ideal.Quotient.mkₐ R P.ker)) :
            (a : MvPolynomial ι R) → S)
          (MvPolynomial.X x) :
        S)
      ((AlgHom.comp (↑(AlgEquiv.restrictScalars R P.quotientEquiv) : P.Quotient →ₐ[R] S) (Ideal.Quotient.mkₐ R P.ker) :
            (a : MvPolynomial ι R) → S)
          (MvPolynomial.X x) :
        S)
⊢ AlgHom.comp (B := R ⊗[R₀] ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀)
      (P.tensorModelOfHasCoeffsHom R₀)
      (AlgHom.comp
        (Ideal.Quotient.liftₐ P.ker
          (AlgHom.comp (B := R ⊗[R₀] MvPolynomial ι R₀)
            (TensorProduct.map (AlgHom.id R R)
                (Ideal.Quotient.mkₐ R₀
                  (Ideal.span
                    (Set.range (ι := σ)
                      (relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀)))) :
              R ⊗[R₀] MvPolynomial ι R₀ →ₐ[R]
                R ⊗[R₀]
                  HasQuotient.Quotient (MvPolynomial ι R₀) (B := Ideal (MvPolynomial ι R₀))
                    (Ideal.span
                      (Set.range (ι := σ)
                        (relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀))))
            ((↑(AlgEquiv.symm (MvPolynomial.algebraTensorAlgEquiv R₀ R)) :
                MvPolynomial ι R →ₐ[R] R ⊗[R₀] MvPolynomial ι R₀) :
              MvPolynomial ι R →ₐ[R] R ⊗[R₀] MvPolynomial ι R₀))
          ⋯)
        (Ideal.Quotient.mkₐ R P.ker)) =
    AlgHom.comp (↑(AlgEquiv.restrictScalars R P.quotientEquiv) : P.Quotient →ₐ[R] S) (Ideal.Quotient.mkₐ R P.ker)

Tactic:
ext x