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
i : σ
⊢ Eq.{v + 1} (α := 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)) :
          (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → S)
        (MvPolynomial.X i) :
      S)
    ((comp (algebraMap P.Ring S) e.toRingEquiv.toRingHom : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → S)
        (MvPolynomial.X i) :
      S)

Tactic:
simp [e]
-- 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
⊢ 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)

Tactic:
have H : (MvPolynomial.aeval fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))).toRingHom =
      (algebraMap P.Ring S).comp e.toRingHom := by
    ext
    · simp [e, IsScalarTower.algebraMap_eq R (MvPolynomial (Fin n) R) S]
    · simp [e, @RingHom.algebraMap_toAlgebra (MvPolynomial (Fin n) R) S, φ]
    · simp [e]
-- 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)
⊢ Function.Surjective.{u + 1, v + 1} (α := MvPolynomial σ (MvPolynomial (Fin n) R)) (β := S)
    (Function.comp (β := P.Ring) (⇑(algebraMap P.Ring S) : (a : P.Ring) → S)
      (⇑e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring))

Tactic:
P.algebraMap_surjective.comp e.surjective

Premises used: Algebra.Generators.algebraMap_surjective, Algebra.SubmersivePresentation.toPreSubmersivePresentation, Algebra.PreSubmersivePresentation.toPresentation, Function.Surjective.comp, AlgEquiv.surjective, Algebra.Presentation.toGenerators
-- 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)
h :
  Eq (α := MvPolynomial σ (MvPolynomial (Fin n) R) → S)
    (⇑(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)) :
      (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → S)
    (Function.comp (β := P.Ring) (⇑(algebraMap P.Ring S) : (a : P.Ring) → S)
      (⇑e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring))
⊢ Function.Surjective.{max (u + 1) 1, v + 1} (α := MvPolynomial σ (MvPolynomial (Fin n) R)) (β := S)
    (⇑(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)) :
      (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → S)

Tactic:
convert! P.algebraMap_surjective.comp e.surjective

Premises used: Algebra.Generators.algebraMap_surjective, Algebra.SubmersivePresentation.toPreSubmersivePresentation, Algebra.PreSubmersivePresentation.toPresentation, Function.Surjective.comp, AlgEquiv.surjective, Algebra.Presentation.toGenerators
-- 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)
⊢ Eq (α := MvPolynomial σ (MvPolynomial (Fin n) R) → S)
    (⇑(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)) :
      (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → S)
    (Function.comp (β := P.Ring) (⇑(algebraMap P.Ring S) : (a : P.Ring) → S)
      (⇑e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring))

Tactic:
congr($H)

Premises used: congrArg, id, DFunLike.coe
-- 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)
⊢ Eq (α := MvPolynomial σ (MvPolynomial (Fin n) R) → S)
    (⇑(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)) :
      (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → S)
    (Function.comp (β := P.Ring) (⇑(algebraMap P.Ring S) : (a : P.Ring) → S)
      (⇑e : (a : MvPolynomial σ (MvPolynomial (Fin n) R)) → P.Ring))

Tactic:
exact congr($H)
-- 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)
rw :
  Ideal.comap e.toRingEquiv P.ker =
    Algebra.Generators.ker
      (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))
        ⋯)
⊢ Eq (α :=
    Ideal
      (Algebra.Generators.Ring.{0, u, v} (R := MvPolynomial (Fin n) R) (S := 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))
          ⋯)))
    (Ideal.span (Set.range ((⇑e.symm : (a : P.Ring) → MvPolynomial σ (MvPolynomial (Fin n) R)) ∘ P.relation)))
    (Algebra.Generators.ker
      (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))
        ⋯))

Tactic:
rw [Set.range_comp, ← AlgEquiv.coe_ringEquiv e.symm, AlgEquiv.symm_toRingEquiv,
        ← Ideal.map_span, P.span_range_relation_eq_ker, Ideal.map_symm]

Premises used: Set.range_comp, AlgEquiv.symm, Algebra.SubmersivePresentation.toPreSubmersivePresentation, Ideal.map_span, Algebra.PreSubmersivePresentation.toPresentation, Algebra.Presentation.span_range_relation_eq_ker, AlgEquiv.coe_ringEquiv, Ideal.map_symm, AlgEquiv.symm_toRingEquiv
-- 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)
⊢ Ideal.comap e.toRingEquiv P.ker =
    Algebra.Generators.ker
      (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))
        ⋯)

Tactic:
congr(RingHom.ker $H).symm

Premises used: Multiset.sum, Multiset.foldr, congrArg, Set.Mem, setOf, Finsupp.sum, MvPolynomial.eval₂, id, Set.preimage, Set.singleton, Ideal.comap, AddMonoidAlgebra, Eq.symm, Finset.sum, RingHom.ker
-- 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)
⊢ Ideal.comap e.toRingEquiv P.ker =
    Algebra.Generators.ker
      (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))
        ⋯)

Tactic:
exact congr(RingHom.ker $H).symm

Premises used: congrArg, id, Eq.symm, RingHom.ker
-- 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 := ⋯ }
⊢ IsUnit P.jacobian

Tactic:
P.jacobian_isUnit

Premises used: Algebra.SubmersivePresentation.jacobian_isUnit