awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsStandardSmoothOfRelativeDimension n R S
this_1 : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w : _root_.Finite σ
w_1 : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e_1 : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι :=
  Equiv.trans ((Equiv.ofInjective P.map ⋯).sumCongr (Equiv.symm (Finite.equivFinOfCardEq ⋯)))
    (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  AlgEquiv.trans (AlgEquiv.symm (MvPolynomial.sumAlgEquiv R σ (Fin n))) (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e : MvPolynomial σ (MvPolynomial (Fin n) R) →ₐ[R] P.Ring).comp
    (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
algInst : Algebra (MvPolynomial (Fin n) R) P.Ring := φ.toAlgebra
algInst_1 : Algebra.{u, v} (MvPolynomial (Fin n) R) S := toAlgebra (comp (algebraMap P.Ring S) φ.toRingHom)
scalarTowerInst : IsScalarTower.{u, u, v} (MvPolynomial (Fin n) R) P.Ring S := ⋯
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
H :
  Eq (α := RingHom.{u, v} (MvPolynomial σ (MvPolynomial (Fin n) R)) S)
    (AlgHom.toRingHom
      (MvPolynomial.aeval fun (x : σ) ↦
        (algebraMap P.Ring S : (a : P.Ring) → S)
          ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring) (MvPolynomial.X x) : P.Ring)))
    (comp (algebraMap P.Ring S) e.toRingEquiv.toRingHom)
P' : Algebra.PreSubmersivePresentation.{0, 0, u, v} (MvPolynomial (Fin n) R) S σ σ :=
  let __Generators : Algebra.Generators.{0, u, v} (MvPolynomial (Fin n) R) S σ :=
    Algebra.Generators.ofSurjective
      (fun (x : σ) ↦
        (algebraMap P.Ring S : (a : P.Ring) → S)
          ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring) (MvPolynomial.X x) : P.Ring))
      ⋯;
  { toGenerators := __Generators,
    relation := (⇑e.symm : (a : P.Ring) → MvPolynomial σ (MvPolynomial (Fin n) R)) ∘ P.relation,
    span_range_relation_eq_ker := ⋯, map := _root_.id, map_inj := ⋯ }
h : P'.jacobian = P.jacobian
⊢ IsUnit P'.jacobian

Tactic:
convert! P.jacobian_isUnit using 1

Premises used: Algebra.SubmersivePresentation.jacobian_isUnit
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsStandardSmoothOfRelativeDimension n R S
this_1 : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w : _root_.Finite σ
w_1 : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e_1 : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι :=
  Equiv.trans ((Equiv.ofInjective P.map ⋯).sumCongr (Equiv.symm (Finite.equivFinOfCardEq ⋯)))
    (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  AlgEquiv.trans (AlgEquiv.symm (MvPolynomial.sumAlgEquiv R σ (Fin n))) (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e : MvPolynomial σ (MvPolynomial (Fin n) R) →ₐ[R] P.Ring).comp
    (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
algInst : Algebra (MvPolynomial (Fin n) R) P.Ring := φ.toAlgebra
algInst_1 : Algebra.{u, v} (MvPolynomial (Fin n) R) S := toAlgebra (comp (algebraMap P.Ring S) φ.toRingHom)
scalarTowerInst : IsScalarTower.{u, u, v} (MvPolynomial (Fin n) R) P.Ring S := ⋯
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
H :
  Eq (α := RingHom.{u, v} (MvPolynomial σ (MvPolynomial (Fin n) R)) S)
    (AlgHom.toRingHom
      (MvPolynomial.aeval fun (x : σ) ↦
        (algebraMap P.Ring S : (a : P.Ring) → S)
          ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring) (MvPolynomial.X x) : P.Ring)))
    (comp (algebraMap P.Ring S) e.toRingEquiv.toRingHom)
P' : Algebra.PreSubmersivePresentation.{0, 0, u, v} (MvPolynomial (Fin n) R) S σ σ :=
  let __Generators : Algebra.Generators.{0, u, v} (MvPolynomial (Fin n) R) S σ :=
    Algebra.Generators.ofSurjective
      (fun (x : σ) ↦
        (algebraMap P.Ring S : (a : P.Ring) → S)
          ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring) (MvPolynomial.X x) : P.Ring))
      ⋯;
  { toGenerators := __Generators,
    relation := (⇑e.symm : (a : P.Ring) → MvPolynomial σ (MvPolynomial (Fin n) R)) ∘ P.relation,
    span_range_relation_eq_ker := ⋯, map := _root_.id, map_inj := ⋯ }
h :
  Eq.{v + 1} (α := S)
    (Matrix.det (n := σ) ((mapMatrix (algebraMap P'.Ring S) : (a : Matrix σ σ P'.Ring) → Matrix σ σ S) P'.jacobiMatrix))
    (Matrix.det (n := σ) ((mapMatrix (algebraMap P.Ring S) : (a : Matrix σ σ P.Ring) → Matrix σ σ S) P.jacobiMatrix))
⊢ P'.jacobian = P.jacobian

Tactic:
simp_rw [Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det, map_det]

Premises used: RingHom.map_det, Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsStandardSmoothOfRelativeDimension n R S
this_1 : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w : _root_.Finite σ
w_1 : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e_1 : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι :=
  Equiv.trans ((Equiv.ofInjective P.map ⋯).sumCongr (Equiv.symm (Finite.equivFinOfCardEq ⋯)))
    (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  AlgEquiv.trans (AlgEquiv.symm (MvPolynomial.sumAlgEquiv R σ (Fin n))) (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e : MvPolynomial σ (MvPolynomial (Fin n) R) →ₐ[R] P.Ring).comp
    (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
algInst : Algebra (MvPolynomial (Fin n) R) P.Ring := φ.toAlgebra
algInst_1 : Algebra.{u, v} (MvPolynomial (Fin n) R) S := toAlgebra (comp (algebraMap P.Ring S) φ.toRingHom)
scalarTowerInst : IsScalarTower.{u, u, v} (MvPolynomial (Fin n) R) P.Ring S := ⋯
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
H :
  Eq (α := RingHom.{u, v} (MvPolynomial σ (MvPolynomial (Fin n) R)) S)
    (AlgHom.toRingHom
      (MvPolynomial.aeval fun (x : σ) ↦
        (algebraMap P.Ring S : (a : P.Ring) → S)
          ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring) (MvPolynomial.X x) : P.Ring)))
    (comp (algebraMap P.Ring S) e.toRingEquiv.toRingHom)
P' : Algebra.PreSubmersivePresentation.{0, 0, u, v} (MvPolynomial (Fin n) R) S σ σ :=
  let __Generators : Algebra.Generators.{0, u, v} (MvPolynomial (Fin n) R) S σ :=
    Algebra.Generators.ofSurjective
      (fun (x : σ) ↦
        (algebraMap P.Ring S : (a : P.Ring) → S)
          ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring) (MvPolynomial.X x) : P.Ring))
      ⋯;
  { toGenerators := __Generators,
    relation := (⇑e.symm : (a : P.Ring) → MvPolynomial σ (MvPolynomial (Fin n) R)) ∘ P.relation,
    span_range_relation_eq_ker := ⋯, map := _root_.id, map_inj := ⋯ }
h :
  Eq.{v + 1} (α := Matrix σ σ S)
    ((mapMatrix (algebraMap P'.Ring S) : (a : Matrix σ σ P'.Ring) → Matrix σ σ S) P'.jacobiMatrix : Matrix σ σ S)
    ((mapMatrix (algebraMap P.Ring S) : (a : Matrix σ σ P.Ring) → Matrix σ σ S) P.jacobiMatrix : Matrix σ σ S)
⊢ Eq.{v + 1} (α := S)
    (Matrix.det (n := σ) ((mapMatrix (algebraMap P'.Ring S) : (a : Matrix σ σ P'.Ring) → Matrix σ σ S) P'.jacobiMatrix))
    (Matrix.det (n := σ) ((mapMatrix (algebraMap P.Ring S) : (a : Matrix σ σ P.Ring) → Matrix σ σ S) P.jacobiMatrix))

Tactic:
congr 1
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsStandardSmoothOfRelativeDimension n R S
this_1 : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w : _root_.Finite σ
w_1 : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e_1 : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι :=
  Equiv.trans ((Equiv.ofInjective P.map ⋯).sumCongr (Equiv.symm (Finite.equivFinOfCardEq ⋯)))
    (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  AlgEquiv.trans (AlgEquiv.symm (MvPolynomial.sumAlgEquiv R σ (Fin n))) (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e : MvPolynomial σ (MvPolynomial (Fin n) R) →ₐ[R] P.Ring).comp
    (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
algInst : Algebra (MvPolynomial (Fin n) R) P.Ring := φ.toAlgebra
algInst_1 : Algebra.{u, v} (MvPolynomial (Fin n) R) S := toAlgebra (comp (algebraMap P.Ring S) φ.toRingHom)
scalarTowerInst : IsScalarTower.{u, u, v} (MvPolynomial (Fin n) R) P.Ring S := ⋯
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
H :
  Eq (α := RingHom.{u, v} (MvPolynomial σ (MvPolynomial (Fin n) R)) S)
    (AlgHom.toRingHom
      (MvPolynomial.aeval fun (x : σ) ↦
        (algebraMap P.Ring S : (a : P.Ring) → S)
          ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring) (MvPolynomial.X x) : P.Ring)))
    (comp (algebraMap P.Ring S) e.toRingEquiv.toRingHom)
P' : Algebra.PreSubmersivePresentation.{0, 0, u, v} (MvPolynomial (Fin n) R) S σ σ :=
  let __Generators : Algebra.Generators.{0, u, v} (MvPolynomial (Fin n) R) S σ :=
    Algebra.Generators.ofSurjective
      (fun (x : σ) ↦
        (algebraMap P.Ring S : (a : P.Ring) → S)
          ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring) (MvPolynomial.X x) : P.Ring))
      ⋯;
  { toGenerators := __Generators,
    relation := (⇑e.symm : (a : P.Ring) → MvPolynomial σ (MvPolynomial (Fin n) R)) ∘ P.relation,
    span_range_relation_eq_ker := ⋯, map := _root_.id, map_inj := ⋯ }
h :
  ∀ (i j : σ),
    Eq.{v + 1} (α := S)
      ((mapMatrix (algebraMap P'.Ring S) : (a : Matrix σ σ P'.Ring) → Matrix σ σ S) P'.jacobiMatrix i j : S)
      ((mapMatrix (algebraMap P.Ring S) : (a : Matrix σ σ P.Ring) → Matrix σ σ S) P.jacobiMatrix i j : S)
⊢ Eq.{v + 1} (α := Matrix σ σ S)
    ((mapMatrix (algebraMap P'.Ring S) : (a : Matrix σ σ P'.Ring) → Matrix σ σ S) P'.jacobiMatrix : Matrix σ σ S)
    ((mapMatrix (algebraMap P.Ring S) : (a : Matrix σ σ P.Ring) → Matrix σ σ S) P.jacobiMatrix : Matrix σ σ S)

Tactic:
ext i j
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsStandardSmoothOfRelativeDimension n R S
this_1 : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w : _root_.Finite σ
w_1 : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e_1 : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι :=
  Equiv.trans ((Equiv.ofInjective P.map ⋯).sumCongr (Equiv.symm (Finite.equivFinOfCardEq ⋯)))
    (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  AlgEquiv.trans (AlgEquiv.symm (MvPolynomial.sumAlgEquiv R σ (Fin n))) (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e : MvPolynomial σ (MvPolynomial (Fin n) R) →ₐ[R] P.Ring).comp
    (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
algInst : Algebra (MvPolynomial (Fin n) R) P.Ring := φ.toAlgebra
algInst_1 : Algebra.{u, v} (MvPolynomial (Fin n) R) S := toAlgebra (comp (algebraMap P.Ring S) φ.toRingHom)
scalarTowerInst : IsScalarTower.{u, u, v} (MvPolynomial (Fin n) R) P.Ring S := ⋯
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
H :
  Eq (α := RingHom.{u, v} (MvPolynomial σ (MvPolynomial (Fin n) R)) S)
    (AlgHom.toRingHom
      (MvPolynomial.aeval fun (x : σ) ↦
        (algebraMap P.Ring S : (a : P.Ring) → S)
          ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring) (MvPolynomial.X x) : P.Ring)))
    (comp (algebraMap P.Ring S) e.toRingEquiv.toRingHom)
P' : Algebra.PreSubmersivePresentation.{0, 0, u, v} (MvPolynomial (Fin n) R) S σ σ :=
  let __Generators : Algebra.Generators.{0, u, v} (MvPolynomial (Fin n) R) S σ :=
    Algebra.Generators.ofSurjective
      (fun (x : σ) ↦
        (algebraMap P.Ring S : (a : P.Ring) → S)
          ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring) (MvPolynomial.X x) : P.Ring))
      ⋯;
  { toGenerators := __Generators,
    relation := (⇑e.symm : (a : P.Ring) → MvPolynomial σ (MvPolynomial (Fin n) R)) ∘ P.relation,
    span_range_relation_eq_ker := ⋯, map := _root_.id, map_inj := ⋯ }
i j : σ
⊢ Eq.{v + 1} (α := S)
    ((mapMatrix (algebraMap P'.Ring S) : (a : Matrix σ σ P'.Ring) → Matrix σ σ S) P'.jacobiMatrix i j : S)
    ((algebraMap P.Ring S : (a : P.Ring) → S)
        ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring)
            ((MvPolynomial.pderiv i :
                (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → MvPolynomial σ (MvPolynomial (Fin n) R))
              ((e.symm : (a : P.Ring) → MvPolynomial σ (MvPolynomial (Fin n) R)) (P.relation j))) :
          P.Ring) :
      S)

Tactic:
simpa [Algebra.PreSubmersivePresentation.jacobiMatrix_apply, P',
          Algebra.Generators.ofSurjective] using congr($H _)

Premises used: Algebra.Generators.ofSurjective, Algebra.PreSubmersivePresentation.jacobiMatrix_apply
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsStandardSmoothOfRelativeDimension n R S
this_1 : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w : _root_.Finite σ
w_1 : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e_1 : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι :=
  Equiv.trans ((Equiv.ofInjective P.map ⋯).sumCongr (Equiv.symm (Finite.equivFinOfCardEq ⋯)))
    (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  AlgEquiv.trans (AlgEquiv.symm (MvPolynomial.sumAlgEquiv R σ (Fin n))) (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e : MvPolynomial σ (MvPolynomial (Fin n) R) →ₐ[R] P.Ring).comp
    (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
algInst : Algebra (MvPolynomial (Fin n) R) P.Ring := φ.toAlgebra
algInst_1 : Algebra.{u, v} (MvPolynomial (Fin n) R) S := toAlgebra (comp (algebraMap P.Ring S) φ.toRingHom)
scalarTowerInst : IsScalarTower.{u, u, v} (MvPolynomial (Fin n) R) P.Ring S := ⋯
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
H :
  Eq (α := RingHom.{u, v} (MvPolynomial σ (MvPolynomial (Fin n) R)) S)
    (AlgHom.toRingHom
      (MvPolynomial.aeval fun (x : σ) ↦
        (algebraMap P.Ring S : (a : P.Ring) → S)
          ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring) (MvPolynomial.X x) : P.Ring)))
    (comp (algebraMap P.Ring S) e.toRingEquiv.toRingHom)
P' : Algebra.PreSubmersivePresentation.{0, 0, u, v} (MvPolynomial (Fin n) R) S σ σ :=
  let __Generators : Algebra.Generators.{0, u, v} (MvPolynomial (Fin n) R) S σ :=
    Algebra.Generators.ofSurjective
      (fun (x : σ) ↦
        (algebraMap P.Ring S : (a : P.Ring) → S)
          ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring) (MvPolynomial.X x) : P.Ring))
      ⋯;
  { toGenerators := __Generators,
    relation := (⇑e.symm : (a : P.Ring) → MvPolynomial σ (MvPolynomial (Fin n) R)) ∘ P.relation,
    span_range_relation_eq_ker := ⋯, map := _root_.id, map_inj := ⋯ }
i j : σ
⊢ Eq (α := P.Ring)
    ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring)
        ((MvPolynomial.pderiv i :
            (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → MvPolynomial σ (MvPolynomial (Fin n) R))
          ((e.symm : (a : P.Ring) → MvPolynomial σ (MvPolynomial (Fin n) R)) (P.relation j))) :
      P.Ring)
    ((MvPolynomial.pderiv (P.map i) : (a : MvPolynomial ι R) → MvPolynomial ι R) (P.relation j) : MvPolynomial ι R)

Tactic:
simp [e, MvPolynomial.pderiv_sumToIter, ← MvPolynomial.pderiv_rename e₀.injective,
        show e₀ (Sum.inl i) = P.map i from rfl]

Premises used: MvPolynomial.pderiv_rename, MvPolynomial.pderiv_sumToIter, Equiv.injective, rfl
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsStandardSmoothOfRelativeDimension n R S
this_1 : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w : _root_.Finite σ
w_1 : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e_1 : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι :=
  Equiv.trans ((Equiv.ofInjective P.map ⋯).sumCongr (Equiv.symm (Finite.equivFinOfCardEq ⋯)))
    (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  AlgEquiv.trans (AlgEquiv.symm (MvPolynomial.sumAlgEquiv R σ (Fin n))) (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e : MvPolynomial σ (MvPolynomial (Fin n) R) →ₐ[R] P.Ring).comp
    (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
algInst : Algebra (MvPolynomial (Fin n) R) P.Ring := φ.toAlgebra
algInst_1 : Algebra.{u, v} (MvPolynomial (Fin n) R) S := toAlgebra (comp (algebraMap P.Ring S) φ.toRingHom)
scalarTowerInst : IsScalarTower.{u, u, v} (MvPolynomial (Fin n) R) P.Ring S := ⋯
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
H :
  Eq (α := RingHom.{u, v} (MvPolynomial σ (MvPolynomial (Fin n) R)) S)
    (AlgHom.toRingHom
      (MvPolynomial.aeval fun (x : σ) ↦
        (algebraMap P.Ring S : (a : P.Ring) → S)
          ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring) (MvPolynomial.X x) : P.Ring)))
    (comp (algebraMap P.Ring S) e.toRingEquiv.toRingHom)
P'_1 : Algebra.PreSubmersivePresentation.{0, 0, u, v} (MvPolynomial (Fin n) R) S σ σ :=
  let __Generators : Algebra.Generators.{0, u, v} (MvPolynomial (Fin n) R) S σ :=
    Algebra.Generators.ofSurjective
      (fun (x : σ) ↦
        (algebraMap P.Ring S : (a : P.Ring) → S)
          ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring) (MvPolynomial.X x) : P.Ring))
      ⋯;
  { toGenerators := __Generators,
    relation := (⇑e.symm : (a : P.Ring) → MvPolynomial σ (MvPolynomial (Fin n) R)) ∘ P.relation,
    span_range_relation_eq_ker := ⋯, map := _root_.id, map_inj := ⋯ }
P' : Algebra.SubmersivePresentation.{0, 0, u, v} (MvPolynomial (Fin n) R) S σ σ :=
  let __spread.0 := P'_1;
  { toPreSubmersivePresentation := __spread.0, jacobian_isUnit := ⋯ }
⊢ P'.dimension = 0

Tactic:
simp [Algebra.Presentation.dimension]

Premises used: Algebra.Presentation.dimension
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.IsStandardSmoothOfRelativeDimension n R S
this_1 : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w : _root_.Finite σ
w_1 : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e_1 : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι :=
  Equiv.trans ((Equiv.ofInjective P.map ⋯).sumCongr (Equiv.symm (Finite.equivFinOfCardEq ⋯)))
    (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  AlgEquiv.trans (AlgEquiv.symm (MvPolynomial.sumAlgEquiv R σ (Fin n))) (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e : MvPolynomial σ (MvPolynomial (Fin n) R) →ₐ[R] P.Ring).comp
    (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
algInst : Algebra (MvPolynomial (Fin n) R) P.Ring := φ.toAlgebra
algInst_1 : Algebra.{u, v} (MvPolynomial (Fin n) R) S := toAlgebra (comp (algebraMap P.Ring S) φ.toRingHom)
scalarTowerInst : IsScalarTower.{u, u, v} (MvPolynomial (Fin n) R) P.Ring S := ⋯
this_2 : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
H :
  Eq (α := RingHom.{u, v} (MvPolynomial σ (MvPolynomial (Fin n) R)) S)
    (AlgHom.toRingHom
      (MvPolynomial.aeval fun (x : σ) ↦
        (algebraMap P.Ring S : (a : P.Ring) → S)
          ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring) (MvPolynomial.X x) : P.Ring)))
    (comp (algebraMap P.Ring S) e.toRingEquiv.toRingHom)
P'_1 : Algebra.PreSubmersivePresentation.{0, 0, u, v} (MvPolynomial (Fin n) R) S σ σ :=
  let __Generators : Algebra.Generators.{0, u, v} (MvPolynomial (Fin n) R) S σ :=
    Algebra.Generators.ofSurjective
      (fun (x : σ) ↦
        (algebraMap P.Ring S : (a : P.Ring) → S)
          ((e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring) (MvPolynomial.X x) : P.Ring))
      ⋯;
  { toGenerators := __Generators,
    relation := (⇑e.symm : (a : P.Ring) → MvPolynomial σ (MvPolynomial (Fin n) R)) ∘ P.relation,
    span_range_relation_eq_ker := ⋯, map := _root_.id, map_inj := ⋯ }
P' : Algebra.SubmersivePresentation.{0, 0, u, v} (MvPolynomial (Fin n) R) S σ σ :=
  let __spread.0 := P'_1;
  { toPreSubmersivePresentation := __spread.0, jacobian_isUnit := ⋯ }
⊢ Etale (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) S))

Tactic:
exact etale_algebraMap.mpr (Algebra.Etale.iff_isStandardSmoothOfRelativeDimension_zero.mpr
    ⟨_, _, _, inferInstance, P', by simp [Algebra.Presentation.dimension]⟩)

Premises used: Iff.mpr, inferInstance, Algebra.Etale.iff_isStandardSmoothOfRelativeDimension_zero, RingHom.etale_algebraMap, Exists.intro, Algebra.IsStandardSmoothOfRelativeDimension.mk
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
n : ℕ
hf : IsStandardSmoothOfRelativeDimension n f
⊢ Algebra.IsStandardSmoothOfRelativeDimension n R S

Tactic:
algebraize [f]
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
n : ℕ
hf : IsStandardSmoothOfRelativeDimension n f
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.IsStandardSmoothOfRelativeDimension n R S
obtain :
  ∀ (g : MvPolynomial (Fin n) R →ₐ[R] S) (hg : g.Etale),
    ∃ (g : RingHom.{u, v} (MvPolynomial (Fin n) R) S), g.comp MvPolynomial.C = f ∧ g.Etale
⊢ ∃ (g : RingHom.{u, v} (MvPolynomial (Fin n) R) S), g.comp MvPolynomial.C = f ∧ g.Etale

Tactic:
obtain ⟨g, hg⟩ := Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial n R S

Premises used: Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
n : ℕ
hf : IsStandardSmoothOfRelativeDimension n f
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.IsStandardSmoothOfRelativeDimension n R S
g : MvPolynomial (Fin n) R →ₐ[R] S
hg : g.Etale
⊢ ∃ (g : RingHom.{u, v} (MvPolynomial (Fin n) R) S), g.comp MvPolynomial.C = f ∧ g.Etale

Tactic:
⟨_, g.comp_algebraMap, hg⟩

Premises used: AlgHom.comp_algebraMap, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
n : ℕ
hf : IsStandardSmoothOfRelativeDimension n f
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.IsStandardSmoothOfRelativeDimension n R S
g : MvPolynomial (Fin n) R →ₐ[R] S
hg : g.Etale
⊢ ∃ (g : RingHom.{u, v} (MvPolynomial (Fin n) R) S), g.comp MvPolynomial.C = f ∧ g.Etale

Tactic:
exact ⟨_, g.comp_algebraMap, hg⟩