awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
⊢ Algebra.IsStandardSmoothOfRelativeDimension n R T

Tactic:
h
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
h₁ : inst_4 = toAlgebra (algebraMap R T)
⊢ Algebra.IsStandardSmoothOfRelativeDimension n R T

Tactic:
convert! h
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
h₁ :
  ∀ (r : R) (x : T),
    (have I := inst_4;
      r • x) =
      r • x
⊢ inst_4 = toAlgebra (algebraMap R T)

Tactic:
ext
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
r : R
x : T
h₁ : HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) r : T) x = r • x
⊢ (have I := inst_4;
    r • x) =
    r • x

Tactic:
simp_rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
r : R
x : T
⊢ HMul.hMul (α := T) ((algebraMap R T : (a : R) → T) r : T) x = r • x

Tactic:
rfl
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : IsStandardSmoothOfRelativeDimension n (algebraMap R T)
⊢ Algebra.IsStandardSmoothOfRelativeDimension n R T

Tactic:
replace h : Algebra.IsStandardSmoothOfRelativeDimension n R T := by
      rw [RingHom.IsStandardSmoothOfRelativeDimension] at h
      convert! h; ext; simp_rw [Algebra.smul_def]; rfl
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
⊢ Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)

Tactic:
this
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
h₁ : Eq (α := Algebra S (S ⊗[R] T)) (toAlgebra (algebraMap S (S ⊗[R] T))) Algebra.TensorProduct.leftAlgebra
⊢ Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)

Tactic:
convert! this
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
h₁ :
  ∀ (r : S) (x : S ⊗[R] T),
    (have I : Algebra S (S ⊗[R] T) := toAlgebra (algebraMap S (S ⊗[R] T));
      r • x) =
      r • x
⊢ Eq (α := Algebra S (S ⊗[R] T)) (toAlgebra (algebraMap S (S ⊗[R] T))) Algebra.TensorProduct.leftAlgebra

Tactic:
ext
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
r : S
x : S ⊗[R] T
h₁ : r • x = HMul.hMul (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) r : S ⊗[R] T) x
⊢ (have I : Algebra S (S ⊗[R] T) := toAlgebra (algebraMap S (S ⊗[R] T));
    r • x) =
    r • x

Tactic:
simp_rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
r : S
x : S ⊗[R] T
⊢ r • x = HMul.hMul (α := S ⊗[R] T) ((algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) r : S ⊗[R] T) x

Tactic:
rfl
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
h₂ : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
⊢ IsStandardSmoothOfRelativeDimension n (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))

Tactic:
suffices Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T) by
      rw [RingHom.IsStandardSmoothOfRelativeDimension]
      convert! this; ext; simp_rw [Algebra.smul_def]; rfl
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
R S T : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
⊢ Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
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ᵣ
h :
  ∀ (r : R) (x : Rᵣ),
    (have I : Algebra R Rᵣ := RingHom.toAlgebra (algebraMap R Rᵣ);
      r • x) =
      r • x
⊢ RingHom.toAlgebra (algebraMap R Rᵣ) = inst_2

Tactic:
ext
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
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ᵣ
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
⊢ (have I : Algebra R Rᵣ := RingHom.toAlgebra (algebraMap R Rᵣ);
    r_1 • x) =
    r_1 • x

Tactic:
rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
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) =
    HMul.hMul (α := Rᵣ) ((algebraMap R Rᵣ : (a : R) → Rᵣ) r_1 : Rᵣ) x

Tactic:
rfl
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
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ᵣ
⊢ RingHom.toAlgebra (algebraMap R Rᵣ) = inst_2

Tactic:
have : (algebraMap R Rᵣ).toAlgebra = ‹Algebra R Rᵣ› := by
    ext
    rw [Algebra.smul_def]
    rfl
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
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
rw : Algebra.IsStandardSmoothOfRelativeDimension 0 R Rᵣ
⊢ IsStandardSmoothOfRelativeDimension 0 (algebraMap R Rᵣ)

Tactic:
rw [IsStandardSmoothOfRelativeDimension, this]

Premises used: RingHom.IsStandardSmoothOfRelativeDimension
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
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
⊢ Algebra.IsStandardSmoothOfRelativeDimension 0 R Rᵣ

Tactic:
Algebra.IsStandardSmoothOfRelativeDimension.localization_away r

Premises used: Algebra.IsStandardSmoothOfRelativeDimension.localization_away
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
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
⊢ Algebra.IsStandardSmoothOfRelativeDimension 0 R Rᵣ

Tactic:
exact Algebra.IsStandardSmoothOfRelativeDimension.localization_away r

Premises used: Algebra.IsStandardSmoothOfRelativeDimension.localization_away
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
⊢ LocalizationPreserves.{u_2} fun {R S : Type u_2} [CommRing R] [CommRing S] ↦ IsStandardSmooth

Tactic:
isStandardSmooth_isStableUnderBaseChange.localizationPreserves

Premises used: RingHom.IsStableUnderBaseChange.localizationPreserves, RingHom.isStandardSmooth_isStableUnderBaseChange
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
n : ℕ
⊢ LocalizationPreserves.{u_2} fun {R S : Type u_2} [CommRing R] [CommRing S] ↦ IsStandardSmoothOfRelativeDimension n

Tactic:
(isStandardSmoothOfRelativeDimension_isStableUnderBaseChange n).localizationPreserves

Premises used: RingHom.IsStableUnderBaseChange.localizationPreserves, RingHom.isStandardSmoothOfRelativeDimension_isStableUnderBaseChange
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ IsStandardSmooth (algebraMap R S)

Tactic:
(IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway r).isStandardSmooth

Premises used: RingHom.IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway, RingHom.IsStandardSmoothOfRelativeDimension.isStandardSmooth
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ IsStandardSmooth (algebraMap R S)

Tactic:
exact (IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway r).isStandardSmooth

Premises used: RingHom.IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway, RingHom.IsStandardSmoothOfRelativeDimension.isStandardSmooth
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ IsStandardSmoothOfRelativeDimension 0 (algebraMap R S)

Tactic:
IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway r

Premises used: RingHom.IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
R S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ IsStandardSmoothOfRelativeDimension 0 (algebraMap R S)

Tactic:
exact IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway r

Premises used: RingHom.IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway
-- Module: Mathlib.RingTheory.RingHom.StandardSmooth
Goal:
⊢ StableUnderCompositionWithLocalizationAway.{u_2} fun {R S : Type u_2} [CommRing R] [CommRing S] ↦ IsStandardSmooth

Tactic:
isStandardSmooth_stableUnderComposition.stableUnderCompositionWithLocalizationAway
    isStandardSmooth_holdsForLocalizationAway

Premises used: RingHom.isStandardSmooth_stableUnderComposition, RingHom.isStandardSmooth_holdsForLocalizationAway, RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAway
-- 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 : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
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
⊢ ∃ (g : MvPolynomial (Fin n) R →ₐ[R] S), g.Etale

Tactic:
obtain ⟨ι, σ, _, _, P, e⟩ :=
    Algebra.IsStandardSmoothOfRelativeDimension.out (R := R) (S := S) (n := n)

Premises used: Algebra.IsStandardSmoothOfRelativeDimension.out
-- 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 : (α : 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
rw₄ rw₅ : Nat.card ι - Nat.card σ = Nat.card ι - Nat.card σ
⊢ Nat.card (↑(Set.range P.map)ᶜ : Type) = n

Tactic:
rw [Nat.card_coe_set_eq, Set.ncard_compl,
        Set.ncard_range_of_injective P.map_inj, ← e, Algebra.Presentation.dimension]

Premises used: Algebra.SubmersivePresentation.toPreSubmersivePresentation, Set.ncard_compl, Algebra.PreSubmersivePresentation.map_inj, Nat.card_coe_set_eq, Algebra.Presentation.dimension, Set.ncard_range_of_injective
-- 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 : (α : 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 := ⋯
⊢ IsScalarTower R (MvPolynomial (Fin n) R) P.Ring

Tactic:
have := IsScalarTower.of_algebraMap_eq' φ.comp_algebraMap.symm
-- 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 : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
⊢ IsScalarTower R (MvPolynomial (Fin n) R) S

Tactic:
have : IsScalarTower R (MvPolynomial (Fin n) R) S := .to₁₂₄ _ _ P.Ring _
-- 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
⊢ ∃ (g : MvPolynomial (Fin n) R →ₐ[R] S), g.Etale

Tactic:
⟨IsScalarTower.toAlgHom _ _ _, ?_⟩

Premises used: IsScalarTower.toAlgHom, Exists.intro
-- 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
refine : Etale (R := MvPolynomial (Fin n) R) (AlgHom.toRingHom (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) S))
⊢ ∃ (g : MvPolynomial (Fin n) R →ₐ[R] S), g.Etale

Tactic:
refine ⟨IsScalarTower.toAlgHom _ _ _, ?_⟩
-- 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
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:
simp [e, IsScalarTower.algebraMap_eq R (MvPolynomial (Fin n) R) S]

Premises used: IsScalarTower.algebraMap_eq, MvPolynomial, Fin
-- 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 : 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:
simp [e, @RingHom.algebraMap_toAlgebra (MvPolynomial (Fin n) R) S, φ]

Premises used: RingHom.algebraMap_toAlgebra