awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
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 : σ
⊢ 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₀)
have 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₀)
Tactic: rw [← map_relationOfHasCoeffs R₀, MvPolynomial.algebraTensorAlgEquiv_symm_map]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
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₀)
⊢ 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₀)
have 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)
Tactic: rw [← map_relationOfHasCoeffs R₀, MvPolynomial.algebraTensorAlgEquiv_symm_map]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
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 σ
⊢ FinitePresentation R₀ (ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀)
have intro : ∀ (val : Fintype σ),
  FinitePresentation R₀ (ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀)
Tactic: cases nonempty_fintype σ
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
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 σ
⊢ FinitePresentation R₀ (ModelOfHasCoeffs.{u_1, u_2, u_3, u_4, u_5} (R := R) (S := S) (ι := ι) (σ := σ) (P := P) R₀)
have intro : ∀ (val : Fintype σ),
  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⟩
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
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₀
⊢ ∀ (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)
have 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₀))
Tactic: simp_rw [← RingHom.mem_ker, ← SetLike.le_def, Ideal.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
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₀)
        ((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₀))))
have 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₀))))
Tactic: rw [← MvPolynomial.aeval_map_algebraMap R, ← Generators.algebraMap_apply, ← quotientEquiv_mk]
-- 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 : 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₀
⊢ 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
have 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)
Tactic: have h : Function.Surjective
      ((P.quotientEquiv.restrictScalars R).toAlgHom.comp (Ideal.Quotient.mkₐ _ _)) :=
    (P.quotientEquiv.restrictScalars R).surjective.comp Ideal.Quotient.mk_surjective
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
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)
⊢ 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
have 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₀))
          sorry)
        (↑(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))
Tactic: simp only [← AlgHom.cancel_right h, tensorModelOfHasCoeffsInv, AlgHom.id_comp]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
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₀
⊢ 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₀))
have 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₀)
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
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₀
⊢ 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₀)
have 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₀)
Tactic: obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
Cleared hypotheses: x
-- 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
inst_3 : Finite σ
P : SubmersivePresentation R S ι σ
inst_4 : DecidableEq σ
inst_5 : Fintype σ
⊢ ∃ (v : σ → MvPolynomial ι R), ∑ i : σ, v i * P.relation i = P.jacobiMatrix.det * P.σ (↑⋯.unit⁻¹ : S) - 1
have H : P.jacobiMatrix.det * P.σ (↑sorry.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]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
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
⊢ ∃ (v : σ → MvPolynomial ι R), ∑ i : σ, v i * P.relation i = P.jacobiMatrix.det * P.σ (↑⋯.unit⁻¹ : S) - 1
have rwa : ∀
  (H :
    Membership.mem (γ := Ideal P.Ring) (Ideal.span (Set.range P.relation))
      (P.jacobiMatrix.det * P.σ (↑sorry.unit⁻¹ : S) - 1)),
  ∃ (v : σ → MvPolynomial ι R), ∑ i : σ, v i * P.relation i = P.jacobiMatrix.det * P.σ (↑sorry.unit⁻¹ : S) - 1
Tactic: rwa [← P.span_range_relation_eq_ker, Ideal.mem_span_range_iff_exists_fun] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
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
⊢ ∃ (v : σ → MvPolynomial ι R), ∑ i : σ, v i * P.relation i = P.jacobiMatrix.det * P.σ (↑⋯.unit⁻¹ : S) - 1
have rwa₁ : ∀ (H : ∃ (c : σ → P.Ring), ∑ i : σ, c i * P.relation i = P.jacobiMatrix.det * P.σ (↑sorry.unit⁻¹ : S) - 1),
  ∃ (v : σ → MvPolynomial ι R), ∑ i : σ, v i * P.relation i = P.jacobiMatrix.det * P.σ (↑sorry.unit⁻¹ : S) - 1
Tactic: rwa [← P.span_range_relation_eq_ker, Ideal.mem_span_range_iff_exists_fun] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
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 σ
⊢ (MvPolynomial.map (algebraMap R₀ R) : (a : MvPolynomial ι R₀) → MvPolynomial ι R) (P.jacobianOfHasCoeffs R₀) =
    P.jacobiMatrix.det
have 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
Tactic: rw [jacobianOfHasCoeffs, @RingHom.map_det]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
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 σ
⊢ 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
have h : (RingHom.mapMatrix (MvPolynomial.map (algebraMap R₀ R)) :
      (a : Matrix σ σ (MvPolynomial ι R₀)) → Matrix σ σ (MvPolynomial ι R))
    (PreSubmersivePresentation.jacobiMatrix (P.ofHasCoeffs R₀)) =
  P.jacobiMatrix
Tactic: congr! 1
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
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 σ
⊢ (RingHom.mapMatrix (MvPolynomial.map (algebraMap R₀ R)) :
        (a : Matrix σ σ (MvPolynomial ι R₀)) → Matrix σ σ (MvPolynomial ι R))
      (PreSubmersivePresentation.jacobiMatrix (P.ofHasCoeffs R₀)) =
    P.jacobiMatrix
have 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
Tactic: ext1 i j
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
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 σ
⊢ (MvPolynomial.aeval P.val : (a : MvPolynomial ι R₀) → S) (P.jacobianOfHasCoeffs R₀) = P.jacobian
have 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
Tactic: rw [← MvPolynomial.aeval_map_algebraMap R, map_jacobianOfHasCoeffs,
    P.jacobian_eq_jacobiMatrix_det, Generators.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
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
⊢ (MvPolynomial.aeval P.val : (a : MvPolynomial ι R₀) → S) (P.jacobianOfHasCoeffs R₀) = P.jacobian
have rw₁ : (MvPolynomial.aeval P.val : (a : MvPolynomial ι R) → S) P.jacobiMatrix.det = P.jacobian
Tactic: rw [← MvPolynomial.aeval_map_algebraMap R, map_jacobianOfHasCoeffs,
    P.jacobian_eq_jacobiMatrix_det, Generators.algebraMap_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Extension.Presentation.Core (goal)
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
⊢ (MvPolynomial.aeval P.val : (a : MvPolynomial ι R₀) → S) (P.jacobianOfHasCoeffs R₀) = P.jacobian
have 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)
Tactic: rw [← MvPolynomial.aeval_map_algebraMap R, map_jacobianOfHasCoeffs,
    P.jacobian_eq_jacobiMatrix_det, Generators.algebraMap_apply]