-- 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₀
i : σ
simp :
  Eq (α :=
    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₀))))
    (((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₀)))) :
          (a : R ⊗[R₀] MvPolynomial ι R₀) →
            R ⊗[R₀] (MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (relationOfHasCoeffs R₀))))
        (1 ⊗ₜ[R₀] relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀ i) :
      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₀))))
    (0 :
      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₀))))
⊢ P.relation i ∈
    (↑(RingHom.ker (F :=
          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₀))))
          (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₀) :
            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₀))))) :
      Set P.Ring)

Tactic:
simp only [SetLike.mem_coe, RingHom.mem_ker, AlgHom.coe_comp,
      AlgEquiv.coe_algHom, Function.comp_apply, algebraTensorAlgEquiv_symm_relation]

Premises used: RingHom.mem_ker, AlgHom.coe_comp, AlgEquiv.coe_algHom, SetLike.mem_coe, Algebra.Presentation.algebraTensorAlgEquiv_symm_relation, Function.comp_apply