awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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
have h : P'.jacobian = P.jacobian
Tactic: convert! P.jacobian_isUnit using 1
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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 := ⋯ }
⊢ P'.jacobian = P.jacobian
have 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))
Tactic: simp_rw [Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det, map_det]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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 := ⋯ }
⊢ 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))
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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 := ⋯ }
⊢ 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)
have 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)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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)
    ((mapMatrix (algebraMap P.Ring S) : (a : Matrix σ σ P.Ring) → Matrix σ σ S) P.jacobiMatrix i j : S)
have trans : 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: trans algebraMap P.Ring S (e ((e.symm (P.relation j)).pderiv i))
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (hypothesis)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
n : ℕ
hf : IsStandardSmoothOfRelativeDimension n f
⊢ ∃ (g : RingHom.{u, v} (MvPolynomial (Fin n) R) S), g.comp MvPolynomial.C = f ∧ g.Etale
have algebraizeInst : Algebra.IsStandardSmoothOfRelativeDimension n R S
Tactic: algebraize [f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
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 : RingHom.{u, v} (MvPolynomial (Fin n) R) S), g.comp MvPolynomial.C = f ∧ g.Etale
have 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
Tactic: obtain ⟨g, hg⟩ := Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial n R S
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
n : ℕ
hf : IsStandardSmoothOfRelativeDimension n f
⊢ ∃ (g : RingHom.{u, v} (MvPolynomial (Fin n) R) S), g.comp MvPolynomial.C = f ∧ g.Etale
have algebraize : Algebra.IsStandardSmoothOfRelativeDimension n R S →
  ∃ (g : RingHom.{u, v} (MvPolynomial (Fin n) R) S), g.comp MvPolynomial.C = f ∧ g.Etale
Tactic: classical
  algebraize [f]
  obtain ⟨g, hg⟩ := Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial n R S
  exact ⟨_, g.comp_algebraMap, hg⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
n : ℕ
hf : IsStandardSmoothOfRelativeDimension n f
algebraize :
  Algebra.IsStandardSmoothOfRelativeDimension n R S →
    ∃ (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
have algebraize₁ : let algInst := f.toAlgebra;
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: classical
  algebraize [f]
  obtain ⟨g, hg⟩ := Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial n R S
  exact ⟨_, g.comp_algebraMap, hg⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
Goal:
R : Type u
S : Type v
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.IsStandardSmooth
⊢ ∃ (n : ℕ) (g : RingHom.{u, v} (MvPolynomial (Fin n) R) S), g.comp MvPolynomial.C = f ∧ g.Etale
have obtain : ∀ (w w_1 : Type) (w_2 : _root_.Finite w_1),
  _root_.Finite w →
    ∀ (P : Algebra.SubmersivePresentation R S w w_1),
      ∃ (n : ℕ) (g : RingHom.{u, v} (MvPolynomial (Fin n) R) S), g.comp MvPolynomial.C = f ∧ g.Etale
Tactic: obtain ⟨_, _, _, _, ⟨P⟩⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Surjective (goal)
Goal:
⊢ RespectsIso.{u_1} fun {X Y : Type u_1} [CommRing X] [CommRing Y] (f : X →+* Y) ↦
    Function.Surjective (α := X) (β := Y) (⇑f : (a : X) → Y)
have apply : ∀ {R S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S),
  Function.Surjective (α := R) (β := S) (⇑e.toRingHom : (a : R) → S)
Tactic: apply surjective_stableUnderComposition.respectsIso
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Surjective (goal)
Goal:
⊢ IsStableUnderBaseChange.{u_1} fun {X Y : Type u_1} [CommRing X] [CommRing Y] (f : X →+* Y) ↦
    Function.Surjective (α := X) (β := Y) (⇑f : (a : X) → Y)
have refine : ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T],
  Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T) →
    Function.Surjective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
Tactic: refine IsStableUnderBaseChange.mk surjective_respectsIso ?_
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Surjective (goal)
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
x : S
y : T
⊢ ∃ (a : S), Eq (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a : S ⊗[R] T) (x ⊗ₜ[R] y : S ⊗[R] T)
have tmul : ∀ (y : R),
  ∃ (a : S),
    Eq (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a : S ⊗[R] T)
      (x ⊗ₜ[R] (algebraMap R T : (a : R) → T) y : S ⊗[R] T)
Tactic: obtain ⟨y, rfl⟩ := h y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Surjective (goal)
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
x : S
y : R
⊢ ∃ (a : S),
    Eq (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a : S ⊗[R] T)
      (x ⊗ₜ[R] (algebraMap R T : (a : R) → T) y : S ⊗[R] T)
have h₁ : Eq (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) (y • x) : S ⊗[R] T)
  (x ⊗ₜ[R] (algebraMap R T : (a : R) → T) y : S ⊗[R] T)
Tactic: use y • x
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Surjective (goal)
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
x : S
y : R
⊢ Eq (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) (y • x) : S ⊗[R] T)
    (x ⊗ₜ[R] (algebraMap R T : (a : R) → T) y : S ⊗[R] T)
have h₁ : Eq (α := S ⊗[R] T) ((y • x) ⊗ₜ[R] 1 : S ⊗[R] T) (x ⊗ₜ[R] (algebraMap R T : (a : R) → T) y : S ⊗[R] T)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Surjective (goal)
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
x : S
y : R
⊢ Eq (α := S ⊗[R] T) ((y • x) ⊗ₜ[R] 1 : S ⊗[R] T) (x ⊗ₜ[R] (algebraMap R T : (a : R) → T) y : S ⊗[R] T)
have h₁ : Eq (α := S ⊗[R] T) (x ⊗ₜ[R] HSMul.hSMul (β := T) y 1) (x ⊗ₜ[R] (algebraMap R T : (a : R) → T) y)
Tactic: rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Surjective (goal)
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
x : S
y : R
h₁ : Eq (α := S ⊗[R] T) (x ⊗ₜ[R] HSMul.hSMul (β := T) y 1) (x ⊗ₜ[R] (algebraMap R T : (a : R) → T) y)
⊢ Eq (α := S ⊗[R] T) ((y • x) ⊗ₜ[R] 1 : S ⊗[R] T) (x ⊗ₜ[R] (algebraMap R T : (a : R) → T) y : S ⊗[R] T)
have h₂ : Eq (α := S ⊗[R] T) (x ⊗ₜ[R] HSMul.hSMul (β := T) y 1) (x ⊗ₜ[R] HSMul.hSMul (β := T) y 1)
Tactic: rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Surjective (goal)
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
x y : S ⊗[R] T
ex : ∃ (a : S), (algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a = x
ey : ∃ (a : S), (algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a = y
⊢ ∃ (a : S), (algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a = x + y
have add : ∀ (x y : S),
  ∃ (a : S),
    (algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a =
      HAdd.hAdd (α := S ⊗[R] T) (β := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) x : S ⊗[R] T)
        ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) y : S ⊗[R] T)
Tactic: obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey
Cleared hypotheses: x, y, ex, ey
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Surjective (goal)
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
x : S ⊗[R] T
⊢ ∃ (a : S), (algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a = x
have zero : ∃ (a : S), Eq (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a : S ⊗[R] T) (0 : S ⊗[R] T)
Tactic: induction x with
  | zero => exact ⟨0, map_zero _⟩
  | tmul x y =>
    obtain ⟨y, rfl⟩ := h y; use y • x; dsimp
    rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]
  | add x y ex ey => obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey; exact ⟨x + y, map_add _ x y⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Surjective (goal)
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
x : S ⊗[R] T
zero : ∃ (a : S), Eq (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a : S ⊗[R] T) (0 : S ⊗[R] T)
⊢ ∃ (a : S), (algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a = x
have tmul : ∀ (x : S) (y : T),
  ∃ (a : S), Eq (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a : S ⊗[R] T) (x ⊗ₜ[R] y : S ⊗[R] T)
Tactic: induction x with
  | zero => exact ⟨0, map_zero _⟩
  | tmul x y =>
    obtain ⟨y, rfl⟩ := h y; use y • x; dsimp
    rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]
  | add x y ex ey => obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey; exact ⟨x + y, map_add _ x y⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Surjective (goal)
Goal:
R S T : Type u_1
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
x : S ⊗[R] T
zero : ∃ (a : S), Eq (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a : S ⊗[R] T) (0 : S ⊗[R] T)
tmul :
  ∀ (x : S) (y : T),
    ∃ (a : S), Eq (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a : S ⊗[R] T) (x ⊗ₜ[R] y : S ⊗[R] T)
⊢ ∃ (a : S), (algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a = x
have add : ∀ (x y : S ⊗[R] T) (ex : ∃ (a : S), (algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a = x)
  (ey : ∃ (a : S), (algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a = y),
  ∃ (a : S), (algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a = x + y
Tactic: induction x with
  | zero => exact ⟨0, map_zero _⟩
  | tmul x y =>
    obtain ⟨y, rfl⟩ := h y; use y • x; dsimp
    rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]
  | add x y ex ey => obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey; exact ⟨x + y, map_add _ x y⟩
Cleared hypotheses: x