awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₀
x : σ
⊢ (↑(MvPolynomial.coeffs (P.relation x)) : Set R) ⊆
    Set.range.{u_1, u_5 + 1} (ι := R₀) (⇑(algebraMap R₀ R) : (a : R₀) → R)

Tactic:
HasCoeffs.coeffs_relation_mem_range R₀ x

Premises used: Algebra.Presentation.HasCoeffs.coeffs_relation_mem_range
-- 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₀
x : σ
⊢ (↑(MvPolynomial.coeffs (P.relation x)) : Set R) ⊆
    Set.range.{u_1, u_5 + 1} (ι := R₀) (⇑(algebraMap R₀ R) : (a : R₀) → R)

Tactic:
exact HasCoeffs.coeffs_relation_mem_range R₀ x

Premises used: Algebra.Presentation.HasCoeffs.coeffs_relation_mem_range
-- 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₀
r : σ
⊢ (MvPolynomial.map (algebraMap R₀ R) : (a : MvPolynomial ι R₀) → MvPolynomial ι R)
      (relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀ r) =
    P.relation r

Tactic:
(HasCoeffs.relation_mem_range_map R₀ r).choose_spec

Premises used: Algebra.Presentation.relationOfHasCoeffs, Exists.choose_spec, Algebra.Presentation.HasCoeffs.relation_mem_range_map
-- 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₀
r : σ
rw :
  Eq.{u_2 + 1} (α := S)
    ((MvPolynomial.aeval P.val : (a : MvPolynomial ι R) → S)
        ((MvPolynomial.map (algebraMap R₀ R) : (a : MvPolynomial ι R₀) → MvPolynomial ι R)
            (relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀ r) :
          MvPolynomial ι R) :
      S)
    (0 : S)
rw₁ : Eq.{u_2 + 1} (α := S) ((MvPolynomial.aeval P.val : (a : MvPolynomial ι R) → S) (P.relation r) : S) (0 : S)
rw₂ rw₃ : Eq.{u_2 + 1} (α := S) 0 0
⊢ Eq.{u_2 + 1} (α := S)
    ((MvPolynomial.aeval P.val : (a : MvPolynomial ι R₀) → S)
        (relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀ r) :
      S)
    (0 : S)

Tactic:
rw [← MvPolynomial.aeval_map_algebraMap R, map_relationOfHasCoeffs, aeval_val_relation]

Premises used: Algebra.Presentation.map_relationOfHasCoeffs, Algebra.Presentation.aeval_val_relation, MvPolynomial.aeval_map_algebraMap
-- 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₀
r : σ
rw :
  Eq (α := R ⊗[R₀] MvPolynomial ι R₀)
    ((AlgEquiv.symm (MvPolynomial.algebraTensorAlgEquiv R₀ R) : (a : MvPolynomial ι R) → R ⊗[R₀] MvPolynomial ι R₀)
        ((MvPolynomial.map (algebraMap R₀ R) : (a : MvPolynomial ι R₀) → MvPolynomial ι R)
          (relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀ r)) :
      R ⊗[R₀] MvPolynomial ι R₀)
    (1 ⊗ₜ[R₀] relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀ r : R ⊗[R₀] MvPolynomial ι R₀)
rw₁ rw₂ :
  Eq (α := R ⊗[R₀] MvPolynomial ι R₀)
    (1 ⊗ₜ[R₀] relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀ r)
    (1 ⊗ₜ[R₀] relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀ r)
⊢ Eq (α := R ⊗[R₀] MvPolynomial ι R₀)
    ((AlgEquiv.symm (MvPolynomial.algebraTensorAlgEquiv R₀ R) : (a : MvPolynomial ι R) → R ⊗[R₀] MvPolynomial ι R₀)
        (P.relation r) :
      R ⊗[R₀] MvPolynomial ι R₀)
    (1 ⊗ₜ[R₀] relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀ r : R ⊗[R₀] MvPolynomial ι R₀)

Tactic:
rw [← map_relationOfHasCoeffs R₀, MvPolynomial.algebraTensorAlgEquiv_symm_map]

Premises used: Algebra.Presentation.map_relationOfHasCoeffs, MvPolynomial.algebraTensorAlgEquiv_symm_map
-- 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₀
inst_8 : Finite ι
inst_9 : Finite σ
intro :
  ∀ (val : Fintype σ),
    FinitePresentation R₀ (ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀)
⊢ FinitePresentation R₀ (ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀)

Tactic:
cases nonempty_fintype σ

Premises used: nonempty_fintype
-- 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₀
inst_8 : Finite ι
inst_9 : Finite σ
val : Fintype σ
⊢ Eq (α := Ideal (MvPolynomial ι R₀))
    (Ideal.span
      (↑(Finset.image (α := σ) (relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀)
            Finset.univ) :
        Set (MvPolynomial ι R₀)))
    (Ideal.span (Set.range (ι := σ) (relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀)))

Tactic:
simp
-- 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₀
inst_8 : Finite ι
inst_9 : Finite σ
val : Fintype σ
⊢ FinitePresentation R₀ (ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀)

Tactic:
exact .quotient ⟨Finset.image (P.relationOfHasCoeffs R₀) .univ, by simp⟩
-- 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₀
inst_8 : Finite ι
inst_9 : Finite σ
intro :
  ∀ (val : Fintype σ),
    FinitePresentation R₀ (ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀)
⊢ FinitePresentation R₀ (ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀)

Tactic:
classical
  cases nonempty_fintype σ
  exact .quotient ⟨Finset.image (P.relationOfHasCoeffs R₀) .univ, by simp⟩

Premises used: nonempty_fintype
-- 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₀
simp_rw :
  Set.range (ι := σ) (relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀) ⊆
    (↑(RingHom.ker (F := MvPolynomial ι R₀ →ₐ[R₀] S) (MvPolynomial.aeval P.val)) : Set (MvPolynomial ι R₀))
⊢ ∀ (a : MvPolynomial ι R₀),
    Membership.mem (γ := 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 →
      Eq.{u_2 + 1} (α := S) ((MvPolynomial.aeval P.val : (a : MvPolynomial ι R₀) → S) a : S) (0 : S)

Tactic:
simp_rw [← RingHom.mem_ker, ← SetLike.le_def, Ideal.span_le]

Premises used: Ideal.span_le, RingHom.mem_ker, SetLike.le_def
-- 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 : σ
⊢ relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀ i ∈
    (↑(RingHom.ker (F := MvPolynomial ι R₀ →ₐ[R₀] S) (MvPolynomial.aeval P.val)) : Set (MvPolynomial ι R₀))

Tactic:
simp
-- 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₀
x : R
y : MvPolynomial ι R₀
⊢ (P.tensorModelOfHasCoeffsHom R₀ : (a : R ⊗[R₀] ModelOfHasCoeffs R₀) → S)
      (x ⊗ₜ[R₀]
          (Ideal.Quotient.mk
                (Ideal.span
                  (Set.range (ι := σ) (relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀))) :
              (a : MvPolynomial ι R₀) → MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (relationOfHasCoeffs R₀)))
            y :
        R ⊗[R₀] ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀) =
    HMul.hMul (α := S) (β := S) ((algebraMap R S : (a : R) → S) x : S)
      ((MvPolynomial.aeval P.val : (a : MvPolynomial ι R₀) → S) y : S)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Quotient.liftOn', AddCon.liftOn, Finsupp.sum, MvPolynomial.eval₂, List.foldl, FreeAddMonoid.sumAux, Finset.sum, rfl
-- 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 : σ
⊢ 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₀))))

Tactic:
simp only [TensorProduct.map_tmul, AlgHom.coe_id, id_eq, Ideal.Quotient.mkₐ_eq_mk,
      Ideal.Quotient.mk_span_range, tmul_zero]

Premises used: AlgHom.coe_id, Algebra.TensorProduct.map_tmul, TensorProduct.tmul_zero, Ideal.Quotient.mk_span_range, Ideal.Quotient.mkₐ_eq_mk, id_eq
-- 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₀
x : MvPolynomial ι R₀
rw :
  Eq (α := R ⊗[R₀] ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀)
    ((P.tensorModelOfHasCoeffsInv R₀ : (a : S) → R ⊗[R₀] ModelOfHasCoeffs R₀)
        ((P.quotientEquiv : (a : P.Quotient) → S)
          ((Ideal.Quotient.mk P.ker : (a : P.Ring) → P.Ring ⧸ P.ker)
              ((MvPolynomial.map (algebraMap R₀ R) : (a : MvPolynomial ι R₀) → MvPolynomial ι R) x) :
            P.Ring ⧸ P.ker)) :
      R ⊗[R₀] ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀)
    (1 ⊗ₜ[R₀]
        (Ideal.Quotient.mk
              (Ideal.span
                (Set.range (ι := σ) (relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀))) :
            (a : MvPolynomial ι R₀) → MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (relationOfHasCoeffs R₀)))
          x :
      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₀))))
⊢ Eq (α := R ⊗[R₀] ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀)
    ((P.tensorModelOfHasCoeffsInv R₀ : (a : S) → R ⊗[R₀] ModelOfHasCoeffs R₀)
        ((MvPolynomial.aeval P.val : (a : MvPolynomial ι R₀) → S) x) :
      R ⊗[R₀] ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀)
    (1 ⊗ₜ[R₀]
        (Ideal.Quotient.mk
              (Ideal.span
                (Set.range (ι := σ) (relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀))) :
            (a : MvPolynomial ι R₀) → MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (relationOfHasCoeffs R₀)))
          x :
      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₀))))

Tactic:
rw [← MvPolynomial.aeval_map_algebraMap R, ← Generators.algebraMap_apply, ← quotientEquiv_mk]

Premises used: Algebra.Generators.algebraMap_apply, MvPolynomial.aeval_map_algebraMap, Algebra.Presentation.quotientEquiv_mk
-- 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₀
x : MvPolynomial ι R₀
⊢ Eq (α := R ⊗[R₀] ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀)
    ((P.tensorModelOfHasCoeffsInv R₀ : (a : S) → R ⊗[R₀] ModelOfHasCoeffs R₀)
        ((P.quotientEquiv : (a : P.Quotient) → S)
          ((Ideal.Quotient.mk P.ker : (a : P.Ring) → P.Ring ⧸ P.ker)
              ((MvPolynomial.map (algebraMap R₀ R) : (a : MvPolynomial ι R₀) → MvPolynomial ι R) x) :
            P.Ring ⧸ P.ker)) :
      R ⊗[R₀] ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀)
    (1 ⊗ₜ[R₀]
        (Ideal.Quotient.mk
              (Ideal.span
                (Set.range (ι := σ) (relationOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (P := P) R₀))) :
            (a : MvPolynomial ι R₀) → MvPolynomial ι R₀ ⧸ Ideal.span (Set.range (relationOfHasCoeffs R₀)))
          x :
      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₀))))

Tactic:
simp [tensorModelOfHasCoeffsInv, -quotientEquiv_symm, -quotientEquiv_mk]

Premises used: Algebra.Presentation.tensorModelOfHasCoeffsInv, Algebra.Presentation.quotientEquiv_symm, Algebra.Presentation.quotientEquiv_mk
-- 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₀
⊢ 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)

Tactic:
have h : Function.Surjective
      ((P.quotientEquiv.restrictScalars R).toAlgHom.comp (Ideal.Quotient.mkₐ _ _)) :=
    (P.quotientEquiv.restrictScalars R).surjective.comp Ideal.Quotient.mk_surjective
-- 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)
simp :
  Eq (α := P.Ring →ₐ[R] S)
    (AlgHom.comp
      (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₀))
            ⋯)
          (↑(AlgEquiv.symm (AlgEquiv.restrictScalars R P.quotientEquiv)) : S →ₐ[R] P.Quotient)))
      (AlgHom.comp (↑(AlgEquiv.restrictScalars R P.quotientEquiv) : P.Quotient →ₐ[R] S) (Ideal.Quotient.mkₐ R P.ker)))
    (AlgHom.comp (↑(AlgEquiv.restrictScalars R P.quotientEquiv) : P.Quotient →ₐ[R] S) (Ideal.Quotient.mkₐ R P.ker))
⊢ 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₀) (P.tensorModelOfHasCoeffsInv R₀) =
    AlgHom.id R S

Tactic:
simp only [← AlgHom.cancel_right h, tensorModelOfHasCoeffsInv, AlgHom.id_comp]

Premises used: Algebra.Presentation.tensorModelOfHasCoeffsInv, AlgHom.id_comp, AlgHom.cancel_right
-- 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)
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)

Tactic:
simp
-- 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 :
  ∀ (x : ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀),
    Eq (α := R ⊗[R₀] ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀)
      ((AlgHom.comp
              (AlgHom.restrictScalars R₀
                (AlgHom.comp (P.tensorModelOfHasCoeffsInv R₀) (P.tensorModelOfHasCoeffsHom R₀)))
              TensorProduct.includeRight :
            (a : ModelOfHasCoeffs R₀) → R ⊗[R₀] ModelOfHasCoeffs R₀)
          x :
        R ⊗[R₀] ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀)
      ((AlgHom.comp
              (AlgHom.restrictScalars R₀
                (AlgHom.id R
                  (R ⊗[R₀] ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀)))
              TensorProduct.includeRight :
            (a : ModelOfHasCoeffs R₀) → R ⊗[R₀] ModelOfHasCoeffs R₀)
          x :
        R ⊗[R₀] ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀)
⊢ Eq (α :=
    R ⊗[R₀] ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀ →ₐ[R]
      R ⊗[R₀] ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀)
    (AlgHom.comp (P.tensorModelOfHasCoeffsInv R₀) (P.tensorModelOfHasCoeffsHom R₀))
    (AlgHom.id R (R ⊗[R₀] ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀))

Tactic:
ext x