awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
Goal:
R : Type u
inst : CommRing R
Rᵣ : Type u_2
inst_1 : CommRing Rᵣ
inst_2 : Algebra R Rᵣ
r : R
inst_3 : IsLocalization.Away r Rᵣ
r_1 : R
x : Rᵣ
⊢ (have I : Algebra R Rᵣ := RingHom.toAlgebra (algebraMap R Rᵣ);
    r_1 • x) =
    r_1 • x
have h : (have I : Algebra R Rᵣ := RingHom.toAlgebra (algebraMap R Rᵣ);
  r_1 • x) =
  HMul.hMul (α := Rᵣ) ((algebraMap R Rᵣ : (a : R) → Rᵣ) r_1 : Rᵣ) x
Tactic: rw [Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (hypothesis)
Goal:
R : Type u
inst : CommRing R
Rᵣ : Type u_2
inst_1 : CommRing Rᵣ
inst_2 : Algebra R Rᵣ
r : R
inst_3 : IsLocalization.Away r Rᵣ
⊢ IsStandardSmoothOfRelativeDimension 0 (algebraMap R Rᵣ)
have this : RingHom.toAlgebra (algebraMap R Rᵣ) = inst_2
Tactic: have : (algebraMap R Rᵣ).toAlgebra = ‹Algebra R Rᵣ› := by
    ext
    rw [Algebra.smul_def]
    rfl
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (goal)
Goal:
R : Type u
inst : CommRing R
Rᵣ : Type u_2
inst_1 : CommRing Rᵣ
inst_2 : Algebra R Rᵣ
r : R
inst_3 : IsLocalization.Away r Rᵣ
this : RingHom.toAlgebra (algebraMap R Rᵣ) = inst_2
⊢ IsStandardSmoothOfRelativeDimension 0 (algebraMap R Rᵣ)
have rw : Algebra.IsStandardSmoothOfRelativeDimension 0 R Rᵣ
Tactic: rw [IsStandardSmoothOfRelativeDimension, this]
-- 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 : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
⊢ ∃ (g : MvPolynomial (Fin n) R →ₐ[R] S), g.Etale
have obtain : ∀ (ι σ : Type) (w : _root_.Finite σ),
  _root_.Finite ι →
    ∀ (P : Algebra.SubmersivePresentation R S ι σ) (e : P.dimension = n),
      ∃ (g : MvPolynomial (Fin n) R →ₐ[R] S), g.Etale
Tactic: obtain ⟨ι, σ, _, _, P, e⟩ :=
    Algebra.IsStandardSmoothOfRelativeDimension.out (R := R) (S := S) (n := n)
-- 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 : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w : _root_.Finite σ
w_1 : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e : P.dimension = n
⊢ Nat.card (↑(Set.range P.map)ᶜ : Type) = n
have rw : (Set.range P.map)ᶜ.ncard = n
Tactic: rw [Nat.card_coe_set_eq, Set.ncard_compl,
        Set.ncard_range_of_injective P.map_inj, ← e, Algebra.Presentation.dimension]
-- 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 : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w : _root_.Finite σ
w_1 : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e : P.dimension = n
rw : (Set.range P.map)ᶜ.ncard = n
⊢ Nat.card (↑(Set.range P.map)ᶜ : Type) = n
have rw₁ : Nat.card ι - (Set.range P.map).ncard = n
Tactic: rw [Nat.card_coe_set_eq, Set.ncard_compl,
        Set.ncard_range_of_injective P.map_inj, ← e, Algebra.Presentation.dimension]
-- 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 : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w : _root_.Finite σ
w_1 : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e : P.dimension = n
rw : (Set.range P.map)ᶜ.ncard = n
rw₁ : Nat.card ι - (Set.range P.map).ncard = n
⊢ Nat.card (↑(Set.range P.map)ᶜ : Type) = n
have rw₂ : Nat.card ι - Nat.card σ = n
Tactic: rw [Nat.card_coe_set_eq, Set.ncard_compl,
        Set.ncard_range_of_injective P.map_inj, ← e, Algebra.Presentation.dimension]
-- 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 : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w : _root_.Finite σ
w_1 : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e : P.dimension = n
rw : (Set.range P.map)ᶜ.ncard = n
rw₁ : Nat.card ι - (Set.range P.map).ncard = n
rw₂ : Nat.card ι - Nat.card σ = n
⊢ Nat.card (↑(Set.range P.map)ᶜ : Type) = n
have rw₃ : Nat.card ι - Nat.card σ = P.dimension
Tactic: rw [Nat.card_coe_set_eq, Set.ncard_compl,
        Set.ncard_range_of_injective P.map_inj, ← e, Algebra.Presentation.dimension]
-- 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 : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w : _root_.Finite σ
w_1 : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e : P.dimension = n
rw : (Set.range P.map)ᶜ.ncard = n
rw₁ : Nat.card ι - (Set.range P.map).ncard = n
rw₂ : Nat.card ι - Nat.card σ = n
rw₃ : Nat.card ι - Nat.card σ = P.dimension
⊢ Nat.card (↑(Set.range P.map)ᶜ : Type) = n
have rw₄ : Nat.card ι - Nat.card σ = Nat.card ι - Nat.card σ
Tactic: rw [Nat.card_coe_set_eq, Set.ncard_compl,
        Set.ncard_range_of_injective P.map_inj, ← e, Algebra.Presentation.dimension]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (hypothesis)
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 : (α : 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 := ⋯
⊢ ∃ (g : MvPolynomial (Fin n) R →ₐ[R] S), g.Etale
have this₁ : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
Tactic: have := IsScalarTower.of_algebraMap_eq' φ.comp_algebraMap.symm
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (hypothesis)
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 : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
⊢ ∃ (g : MvPolynomial (Fin n) R →ₐ[R] S), g.Etale
have this₁ : IsScalarTower R (MvPolynomial (Fin n) R) S
Tactic: have : IsScalarTower R (MvPolynomial (Fin n) R) S := .to₁₂₄ _ _ P.Ring _
-- 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
⊢ ∃ (g : MvPolynomial (Fin n) R →ₐ[R] S), g.Etale
have refine : Etale (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) S))
Tactic: refine ⟨IsScalarTower.toAlgHom _ _ _, ?_⟩
-- 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
⊢ 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)
have hC : ∀ (x : R),
  Eq.{v + 1} (α := S)
    ((comp (β := MvPolynomial (Fin n) R)
            (comp (β := MvPolynomial σ (MvPolynomial (Fin n) R))
              (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)))
              MvPolynomial.C)
            MvPolynomial.C :
          (a : R) → S)
        x :
      S)
    ((comp (comp (comp (algebraMap P.Ring S) e.toRingEquiv.toRingHom) MvPolynomial.C) MvPolynomial.C : (a : R) → S) x :
      S)
Tactic: ext
-- 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
hC :
  ∀ (x : R),
    Eq.{v + 1} (α := S)
      ((comp (β := MvPolynomial (Fin n) R)
              (comp (β := MvPolynomial σ (MvPolynomial (Fin n) R))
                (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)))
                MvPolynomial.C)
              MvPolynomial.C :
            (a : R) → S)
          x :
        S)
      ((comp (comp (comp (algebraMap P.Ring S) e.toRingEquiv.toRingHom) MvPolynomial.C) MvPolynomial.C : (a : R) → S)
          x :
        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)
have hC₁ : ∀ (i : Fin n),
  Eq.{v + 1} (α := S)
    ((comp (β := MvPolynomial σ (MvPolynomial (Fin n) R))
            (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)))
            MvPolynomial.C :
          (a : MvPolynomial (Fin n) R) → S)
        (MvPolynomial.X i) :
      S)
    ((comp (comp (algebraMap P.Ring S) e.toRingEquiv.toRingHom) MvPolynomial.C : (a : MvPolynomial (Fin n) R) → S)
        (MvPolynomial.X i) :
      S)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.StandardSmooth (hypothesis)
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
⊢ Etale (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) S))
have 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)
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]
-- 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)
⊢ 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)
have 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))
Tactic: convert! P.algebraMap_surjective.comp e.surjective
-- 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)
⊢ 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))
        ⋯))
have 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))
      sorry)
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]