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 : ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀
h :
  ∀ (x : MvPolynomial ι 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₀)
          ((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₀] 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₀)
          ((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₀] 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₀)

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x

Premises used: Ideal.Quotient.mk_surjective, 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₀
x : MvPolynomial ι 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₀)
        ((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₀] 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₀)
        ((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₀] ModelOfHasCoeffs.{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₀
x : R
y : MvPolynomial ι R₀
⊢ (tensorModelOfHasCoeffsEquiv 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₀
x : MvPolynomial ι R₀
⊢ Eq (α := R ⊗[R₀] ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀)
    ((AlgEquiv.symm (tensorModelOfHasCoeffsEquiv 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:
tensorModelOfHasCoeffsInv_aeval_val _ x

Premises used: Quotient.liftOn', AddCon.liftOn, Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val
-- 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
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
inst_4 : DecidableEq σ
inst_5 : Fintype σ
⊢ P.jacobiMatrix.det * P.σ (↑⋯.unit⁻¹ : S) - 1 ∈ P.ker

Tactic:
simp [PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det]

Premises used: Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det
-- 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
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
inst_4 : DecidableEq σ
inst_5 : Fintype σ
⊢ P.jacobiMatrix.det * P.σ (↑⋯.unit⁻¹ : S) - 1 ∈ P.ker

Tactic:
have H : P.jacobiMatrix.det * P.σ ↑(P.jacobian_isUnit.unit⁻¹) - 1 ∈ P.ker := by
    simp [PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det]
-- 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
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
inst_4 : DecidableEq σ
inst_5 : Fintype σ
H : P.jacobiMatrix.det * P.σ (↑⋯.unit⁻¹ : S) - 1 ∈ P.ker
rwa :
  ∀
    (H :
      Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation))
        (P.jacobiMatrix.det * P.σ (↑⋯.unit⁻¹ : S) - 1)),
    ∃ (v : σ → MvPolynomial ι R), ∑ i : σ, v i * P.relation i = P.jacobiMatrix.det * P.σ (↑⋯.unit⁻¹ : S) - 1
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (H : ∃ (c : σ → P.Ring), ∑ i : σ, c i * P.relation i = P.jacobiMatrix.det * P.σ (↑⋯.unit⁻¹ : S) - 1),
    ∃ (v : σ → MvPolynomial ι R), ∑ i : σ, v i * P.relation i = P.jacobiMatrix.det * P.σ (↑⋯.unit⁻¹ : S) - 1
⊢ ∃ (v : σ → MvPolynomial ι R), ∑ i : σ, v i * P.relation i = P.jacobiMatrix.det * P.σ (↑⋯.unit⁻¹ : S) - 1

Tactic:
rwa [← P.span_range_relation_eq_ker, Ideal.mem_span_range_iff_exists_fun] at H

Premises used: Algebra.SubmersivePresentation.toPreSubmersivePresentation, Algebra.PreSubmersivePresentation.toPresentation, Algebra.Presentation.span_range_relation_eq_ker, Ideal.mem_span_range_iff_exists_fun
-- 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
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
inst_4 : DecidableEq σ
inst_5 : Fintype σ
⊢ ∑ i : σ,
      Exists.choose (p := fun (v : σ → MvPolynomial ι R) ↦
          ∑ i : σ, v i * P.relation i = P.jacobiMatrix.det * P.σ (↑⋯.unit⁻¹ : S) - 1) ⋯ i *
        P.relation i =
    P.jacobiMatrix.det * P.σ (↑⋯.unit⁻¹ : S) - 1

Tactic:
P.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one.choose_spec

Premises used: Exists.choose_spec, Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one
-- 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
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
inst_4 : DecidableEq σ
inst_5 : Fintype σ
⊢ ∑ i : σ,
      ⋯.choose (p := fun (v : σ → MvPolynomial ι R) ↦
          ∑ i : σ, v i * P.relation i = P.jacobiMatrix.det * P.σ (↑⋯.unit⁻¹ : S) - 1) i *
        P.relation i =
    P.jacobiMatrix.det * P.σ (↑⋯.unit⁻¹ : S) - 1

Tactic:
convert! P.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one.choose_spec

Premises used: Exists.choose_spec, Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one
-- 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
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
⊢ (↑(MvPolynomial.coeffs (P.σ (↑⋯.unit⁻¹ : S))) : Set R).Finite

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
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
⊢ ∀ (i : σ), Membership.mem (γ := Set σ) Set.univ i → (↑(P.jacobianRelations i).coeffs : Set R).Finite

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
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
⊢ ∀ i ∉ Set.univ, (↑(P.jacobianRelations i).coeffs : Set 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
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
⊢ P.coeffs ⊆ P.coeffs

Tactic:
Set.subset_union_left.trans Set.subset_union_left

Premises used: HasSubset.Subset.trans, Set.subset_union_left
-- 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
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 : Fintype σ
inst_10 : DecidableEq σ
rw :
  Matrix.det (n := σ)
      ((RingHom.mapMatrix (MvPolynomial.map (algebraMap R₀ R)) :
          (a : Matrix σ σ (MvPolynomial ι R₀)) → Matrix σ σ (MvPolynomial ι R))
        (PreSubmersivePresentation.jacobiMatrix (P.ofHasCoeffs R₀))) =
    P.jacobiMatrix.det
⊢ (MvPolynomial.map (algebraMap R₀ R) : (a : MvPolynomial ι R₀) → MvPolynomial ι R) (P.jacobianOfHasCoeffs R₀) =
    P.jacobiMatrix.det

Tactic:
rw [jacobianOfHasCoeffs, @RingHom.map_det]

Premises used: RingHom.map_det, Algebra.SubmersivePresentation.jacobianOfHasCoeffs
-- 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
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 : Fintype σ
inst_10 : DecidableEq σ
h :
  (RingHom.mapMatrix (MvPolynomial.map (algebraMap R₀ R)) :
        (a : Matrix σ σ (MvPolynomial ι R₀)) → Matrix σ σ (MvPolynomial ι R))
      (PreSubmersivePresentation.jacobiMatrix (P.ofHasCoeffs R₀)) =
    P.jacobiMatrix
⊢ Matrix.det (n := σ)
      ((RingHom.mapMatrix (MvPolynomial.map (algebraMap R₀ R)) :
          (a : Matrix σ σ (MvPolynomial ι R₀)) → Matrix σ σ (MvPolynomial ι R))
        (PreSubmersivePresentation.jacobiMatrix (P.ofHasCoeffs R₀))) =
    P.jacobiMatrix.det

Tactic:
congr! 1
-- 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
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 : Fintype σ
inst_10 : DecidableEq σ
h :
  ∀ (i j : σ),
    (RingHom.mapMatrix (MvPolynomial.map (algebraMap R₀ R)) :
          (a : Matrix σ σ (MvPolynomial ι R₀)) → Matrix σ σ (MvPolynomial ι R))
        (PreSubmersivePresentation.jacobiMatrix (P.ofHasCoeffs R₀)) i j =
      P.jacobiMatrix i j
⊢ (RingHom.mapMatrix (MvPolynomial.map (algebraMap R₀ R)) :
        (a : Matrix σ σ (MvPolynomial ι R₀)) → Matrix σ σ (MvPolynomial ι R))
      (PreSubmersivePresentation.jacobiMatrix (P.ofHasCoeffs R₀)) =
    P.jacobiMatrix

Tactic:
ext1 i j
-- 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
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 : Fintype σ
inst_10 : DecidableEq σ
i j : σ
⊢ (RingHom.mapMatrix (MvPolynomial.map (algebraMap R₀ R)) :
        (a : Matrix σ σ (MvPolynomial ι R₀)) → Matrix σ σ (MvPolynomial ι R))
      (PreSubmersivePresentation.jacobiMatrix (P.ofHasCoeffs R₀)) i j =
    P.jacobiMatrix i j

Tactic:
simp [Presentation.map_relationOfHasCoeffs, ← MvPolynomial.pderiv_map,
    PreSubmersivePresentation.jacobiMatrix_apply]

Premises used: Algebra.Presentation.map_relationOfHasCoeffs, Algebra.PreSubmersivePresentation.jacobiMatrix_apply, MvPolynomial.pderiv_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
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₀
this : Fintype σ := Fintype.ofFinite σ
rw :
  (MvPolynomial.aeval P.val : (a : MvPolynomial ι R) → S)
      ((MvPolynomial.map (algebraMap R₀ R) : (a : MvPolynomial ι R₀) → MvPolynomial ι R) (P.jacobianOfHasCoeffs R₀) :
        MvPolynomial ι R) =
    P.jacobian
rw₁ : (MvPolynomial.aeval P.val : (a : MvPolynomial ι R) → S) P.jacobiMatrix.det = P.jacobian
rw₂ :
  Eq.{u_2 + 1} (α := S) ((MvPolynomial.aeval P.val : (a : MvPolynomial ι R) → S) P.jacobiMatrix.det : S)
    ((algebraMap P.Ring S : (a : P.Ring) → S) P.jacobiMatrix.det : S)
rw₃ rw₄ :
  Eq.{u_2 + 1} (α := S) ((MvPolynomial.aeval P.val : (a : MvPolynomial ι R) → S) P.jacobiMatrix.det : S)
    ((MvPolynomial.aeval P.val : (a : MvPolynomial ι R) → S) P.jacobiMatrix.det : S)
⊢ (MvPolynomial.aeval P.val : (a : MvPolynomial ι R₀) → S) (P.jacobianOfHasCoeffs R₀) = P.jacobian

Tactic:
rw [← MvPolynomial.aeval_map_algebraMap R, map_jacobianOfHasCoeffs,
    P.jacobian_eq_jacobiMatrix_det, Generators.algebraMap_apply]

Premises used: Algebra.SubmersivePresentation.map_jacobianOfHasCoeffs, Algebra.SubmersivePresentation.toPreSubmersivePresentation, Algebra.Generators.algebraMap_apply, MvPolynomial.aeval_map_algebraMap, Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det
-- 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
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₀
let let₁ let₂ : (MvPolynomial.aeval P.val : (a : MvPolynomial ι R₀) → S) (P.jacobianOfHasCoeffs R₀) = P.jacobian
⊢ (MvPolynomial.aeval P.val : (a : MvPolynomial ι R₀) → S) (P.jacobianOfHasCoeffs R₀) = P.jacobian

Tactic:
classical
  let : Fintype σ := Fintype.ofFinite _
  rw [← MvPolynomial.aeval_map_algebraMap R, map_jacobianOfHasCoeffs,
    P.jacobian_eq_jacobiMatrix_det, Generators.algebraMap_apply]

Premises used: Algebra.SubmersivePresentation.map_jacobianOfHasCoeffs, Algebra.Generators.algebraMap_apply, 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
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₀
⊢ (MvPolynomial.map (algebraMap R₀ R) : (a : MvPolynomial ι R₀) → MvPolynomial ι R) (P.invJacobianOfHasCoeffs R₀) =
    P.σ (↑⋯.unit⁻¹ : S)

Tactic:
(MvPolynomial.mem_range_map_iff_coeffs_subset.mpr
    ((Set.subset_union_right.trans Set.subset_union_left).trans
      (HasCoeffs.coeffs_subset_range (P := P)))).choose_spec

Premises used: Iff.mpr, Exists.choose_spec, MvPolynomial.mem_range_map_iff_coeffs_subset, Set.subset_union_right, Algebra.SubmersivePresentation.HasCoeffs.coeffs_subset_range, HasSubset.Subset.trans, Set.subset_union_left, Algebra.SubmersivePresentation.invJacobianOfHasCoeffs
-- 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
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₀
⊢ (MvPolynomial.aeval P.val : (a : MvPolynomial ι R₀) → S) (P.invJacobianOfHasCoeffs R₀) = (↑⋯.unit⁻¹ : S)

Tactic:
simpa [-map_invJacobianOfHasCoeffs, MvPolynomial.aeval_map_algebraMap] using
    congr(MvPolynomial.aeval P.val $(P.map_invJacobianOfHasCoeffs R₀))

Premises used: Algebra.SubmersivePresentation.map_invJacobianOfHasCoeffs, 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
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₀
i : σ
⊢ (MvPolynomial.map (algebraMap R₀ R) : (a : MvPolynomial ι R₀) → MvPolynomial ι R)
      (P.jacobianRelationsOfHasCoeffs R₀ i) =
    P.jacobianRelations i

Tactic:
(MvPolynomial.mem_range_map_iff_coeffs_subset.mpr
    ((Set.subset_iUnion _ i).trans (Set.subset_union_right.trans
      (HasCoeffs.coeffs_subset_range (P := P))))).choose_spec

Premises used: Iff.mpr, Exists.choose_spec, MvPolynomial.mem_range_map_iff_coeffs_subset, Set.subset_union_right, Algebra.SubmersivePresentation.HasCoeffs.coeffs_subset_range, HasSubset.Subset.trans, Set.subset_iUnion, Algebra.SubmersivePresentation.jacobianRelationsOfHasCoeffs
-- 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
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
inst_10 : Fintype σ
a :
  Eq (α := MvPolynomial ι R)
    ((MvPolynomial.map (algebraMap R₀ R) : (a : MvPolynomial ι R₀) → MvPolynomial ι 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)) :
      MvPolynomial ι R)
    ((MvPolynomial.map (algebraMap R₀ R) : (a : MvPolynomial ι R₀) → MvPolynomial ι R)
        (HMul.hMul (α := MvPolynomial ι R₀) (P.jacobianOfHasCoeffs R₀) (P.invJacobianOfHasCoeffs R₀) - 1) :
      MvPolynomial ι 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) =
    HMul.hMul (α := MvPolynomial ι R₀) (P.jacobianOfHasCoeffs R₀) (P.invJacobianOfHasCoeffs R₀) - 1

Tactic:
apply MvPolynomial.map_injective _ (FaithfulSMul.algebraMap_injective R₀ R)

Premises used: MvPolynomial.map_injective, FaithfulSMul.algebraMap_injective
-- 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
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
inst_10 : Fintype σ
⊢ Eq (α := MvPolynomial ι R)
    ((MvPolynomial.map (algebraMap R₀ R) : (a : MvPolynomial ι R₀) → MvPolynomial ι 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)) :
      MvPolynomial ι R)
    ((MvPolynomial.map (algebraMap R₀ R) : (a : MvPolynomial ι R₀) → MvPolynomial ι R)
        (HMul.hMul (α := MvPolynomial ι R₀) (P.jacobianOfHasCoeffs R₀) (P.invJacobianOfHasCoeffs R₀) - 1) :
      MvPolynomial ι R)

Tactic:
simp [P.map_relationOfHasCoeffs, jacobianRelations_spec]

Premises used: Algebra.Presentation.map_relationOfHasCoeffs, Algebra.SubmersivePresentation.jacobianRelations_spec