awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsSmoothAt R p
f : S
hfp : f ∉ p
H : IsStandardSmooth.{u_1, u_3} R (Localization.Away f)
n : ℕ
φ : RingHom.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg : φ.Etale
algInst : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst : Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
this_1 : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f)
this :
  Ideal.IsPrime (α := Localization.Away f)
    (Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p)
obtain :
  ∀ (g₀ : Localization.Away f)
    (hg : g₀ ∉ Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p)
    (H : IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away g₀)),
    ∃ f ∉ p,
      ∃ (n : ℕ) (x : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)),
        IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
          IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
⊢ ∃ f ∉ p,
    ∃ (n : ℕ) (x : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)),
      IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
        IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)

Tactic:
obtain ⟨g₀, hg, H⟩ := IsEtaleAt.exists_isStandardEtale (R := (MvPolynomial (Fin n) R))
    (S := (Localization.Away f)) (p.map (algebraMap _ _))

Premises used: Algebra.algebraMap, Ideal.map, Algebra.IsEtaleAt.exists_isStandardEtale
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsSmoothAt R p
f : S
hfp : f ∉ p
H_1 : IsStandardSmooth.{u_1, u_3} R (Localization.Away f)
n : ℕ
φ : RingHom.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg_1 : φ.Etale
algInst : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst : Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
this_1 : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f)
this :
  Ideal.IsPrime (α := Localization.Away f)
    (Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p)
g₀ : Localization.Away f
hg : g₀ ∉ Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p
H : IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away g₀)
obtain :
  ∀ (g : S) (m : ℕ)
    (hg₀ :
      IsLocalization.mk' (Localization.Away f) g
          (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers f) x)
            ((fun (x : ℕ) ↦ f ^ x) m) ⋯) =
        g₀),
    ∃ f ∉ p,
      ∃ (n : ℕ) (x : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)),
        IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
          IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
⊢ ∃ f ∉ p,
    ∃ (n : ℕ) (x : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)),
      IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
        IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)

Tactic:
obtain ⟨g, ⟨_, m, rfl⟩, hg₀⟩ := IsLocalization.exists_mk'_eq (.powers f) g₀

Premises used: Submonoid.powers, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsSmoothAt R p
f : S
hfp : f ∉ p
H_1 : IsStandardSmooth.{u_1, u_3} R (Localization.Away f)
n : ℕ
φ : RingHom.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg_1 : φ.Etale
algInst : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst : Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
this_1 : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f)
this :
  Ideal.IsPrime (α := Localization.Away f)
    (Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p)
g₀ : Localization.Away f
hg : g₀ ∉ Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p
H : IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ :
  IsLocalization.mk' (Localization.Away f) g
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers f) x)
        ((fun (x : ℕ) ↦ f ^ x) m) ⋯) =
    g₀
⊢ g ∉ p

Tactic:
simpa [Submonoid.mem_powers_iff, Ideal.IsPrime.mul_mem_iff_mem_or_mem,
    IsLocalization.mk'_mem_map_algebraMap_iff, mt (‹p.IsPrime›.mem_of_pow_mem _) hfp,
    ← hg₀] using hg

Premises used: Ideal.IsPrime.mem_of_pow_mem, mt, IsLocalization.mk'_mem_map_algebraMap_iff, Submonoid.mem_powers_iff, Ideal.IsPrime.mul_mem_iff_mem_or_mem
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsSmoothAt R p
f : S
hfp : f ∉ p
H_1 : IsStandardSmooth.{u_1, u_3} R (Localization.Away f)
n : ℕ
φ : RingHom.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg_1 : φ.Etale
algInst : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst : Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
this_1 : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f)
this :
  Ideal.IsPrime (α := Localization.Away f)
    (Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p)
g₀ : Localization.Away f
hg : g₀ ∉ Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p
H : IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ :
  IsLocalization.mk' (Localization.Away f) g
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers f) x)
        ((fun (x : ℕ) ↦ f ^ x) m) ⋯) =
    g₀
⊢ g ∉ p

Tactic:
replace hg : g ∉ p := by simpa [Submonoid.mem_powers_iff, Ideal.IsPrime.mul_mem_iff_mem_or_mem,
    IsLocalization.mk'_mem_map_algebraMap_iff, mt (‹p.IsPrime›.mem_of_pow_mem _) hfp,
    ← hg₀] using hg
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsSmoothAt R p
f : S
hfp : f ∉ p
H_1 : IsStandardSmooth.{u_1, u_3} R (Localization.Away f)
n : ℕ
φ : RingHom.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg_1 : φ.Etale
algInst : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst : Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
this_1 : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f)
this :
  Ideal.IsPrime (α := Localization.Away f)
    (Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p)
g₀ : Localization.Away f
H : IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ :
  IsLocalization.mk' (Localization.Away f) g
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers f) x)
        ((fun (x : ℕ) ↦ f ^ x) m) ⋯) =
    g₀
hg : g ∉ p
suffices :
  IsLocalization.Away (R := Localization.Away f)
    ((algebraMap S (Localization.Away f) : (a : S) → Localization.Away f) g : Localization.Away f)
    (Localization.Away g₀)
⊢ IsLocalization.Away (f * g) (Localization.Away g₀)

Tactic:
suffices IsLocalization.Away (algebraMap _ (Localization.Away f) g) (Localization.Away g₀) from
      .mul' (Localization.Away f) _ _ _
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsSmoothAt R p
f : S
hfp : f ∉ p
H_1 : IsStandardSmooth.{u_1, u_3} R (Localization.Away f)
n : ℕ
φ : RingHom.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg_1 : φ.Etale
algInst : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst : Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
this_1 : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f)
this :
  Ideal.IsPrime (α := Localization.Away f)
    (Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p)
g₀ : Localization.Away f
H : IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ :
  IsLocalization.mk' (Localization.Away f) g
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers f) x)
        ((fun (x : ℕ) ↦ f ^ x) m) ⋯) =
    g₀
hg : g ∉ p
⊢ IsLocalization.Away (R := Localization.Away f)
    ((algebraMap S (Localization.Away f) : (a : S) → Localization.Away f) g : Localization.Away f)
    (Localization.Away g₀)

Tactic:
IsLocalization.Away.of_associated (r := g₀)
      ⟨(IsLocalization.Away.algebraMap_pow_isUnit f m).unit, ?_⟩

Premises used: IsLocalization.Away.algebraMap_pow_isUnit, Exists.intro, IsUnit.unit, IsLocalization.Away.of_associated
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsSmoothAt R p
f : S
hfp : f ∉ p
H_1 : IsStandardSmooth.{u_1, u_3} R (Localization.Away f)
n : ℕ
φ : RingHom.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg_1 : φ.Etale
algInst : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst : Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
this_1 : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f)
this :
  Ideal.IsPrime (α := Localization.Away f)
    (Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p)
g₀ : Localization.Away f
H : IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ :
  IsLocalization.mk' (Localization.Away f) g
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers f) x)
        ((fun (x : ℕ) ↦ f ^ x) m) ⋯) =
    g₀
hg : g ∉ p
refine :
  g₀ *
      (↑(IsUnit.unit (a :=
            HPow.hPow (α := Localization.Away f)
              ((algebraMap S (Localization.Away f) : (a : S) → Localization.Away f) f) m)
            ⋯) :
        Localization.Away f) =
    (algebraMap S (Localization.Away f) : (a : S) → Localization.Away f) g
⊢ IsLocalization.Away (R := Localization.Away f)
    ((algebraMap S (Localization.Away f) : (a : S) → Localization.Away f) g : Localization.Away f)
    (Localization.Away g₀)

Tactic:
refine IsLocalization.Away.of_associated (r := g₀)
      ⟨(IsLocalization.Away.algebraMap_pow_isUnit f m).unit, ?_⟩

Premises used: IsLocalization.Away.algebraMap_pow_isUnit, Exists.intro, IsUnit.unit, IsLocalization.Away.of_associated
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsSmoothAt R p
f : S
hfp : f ∉ p
H_1 : IsStandardSmooth.{u_1, u_3} R (Localization.Away f)
n : ℕ
φ : RingHom.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg_1 : φ.Etale
algInst : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst : Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
this_1 : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f)
this :
  Ideal.IsPrime (α := Localization.Away f)
    (Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p)
g₀ : Localization.Away f
H : IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ :
  IsLocalization.mk' (Localization.Away f) g
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers f) x)
        ((fun (x : ℕ) ↦ f ^ x) m) ⋯) =
    g₀
hg : g ∉ p
⊢ g₀ *
      (↑(IsUnit.unit (a :=
            HPow.hPow (α := Localization.Away f)
              ((algebraMap S (Localization.Away f) : (a : S) → Localization.Away f) f) m)
            ⋯) :
        Localization.Away f) =
    (algebraMap S (Localization.Away f) : (a : S) → Localization.Away f) g

Tactic:
simp only [← hg₀, IsUnit.unit_spec, ← map_pow, mul_comm, IsLocalization.mk'_spec'_mk]

Premises used: map_pow, mul_comm, IsLocalization.mk'_spec'_mk, IsUnit.unit_spec
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsSmoothAt R p
f : S
hfp : f ∉ p
H_1 : IsStandardSmooth.{u_1, u_3} R (Localization.Away f)
n : ℕ
φ : RingHom.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg_1 : φ.Etale
algInst : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst : Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
this_1 : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f)
this :
  Ideal.IsPrime (α := Localization.Away f)
    (Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p)
g₀ : Localization.Away f
H : IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ :
  IsLocalization.mk' (Localization.Away f) g
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers f) x)
        ((fun (x : ℕ) ↦ f ^ x) m) ⋯) =
    g₀
hg : g ∉ p
⊢ IsLocalization.Away (f * g) (Localization.Away g₀)

Tactic:
have : IsLocalization.Away (f * g) (Localization.Away g₀) := by
    suffices IsLocalization.Away (algebraMap _ (Localization.Away f) g) (Localization.Away g₀) from
      .mul' (Localization.Away f) _ _ _
    refine IsLocalization.Away.of_associated (r := g₀)
      ⟨(IsLocalization.Away.algebraMap_pow_isUnit f m).unit, ?_⟩
    simp only [← hg₀, IsUnit.unit_spec, ← map_pow, mul_comm, IsLocalization.mk'_spec'_mk]
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsSmoothAt R p
f : S
hfp : f ∉ p
H_1 : IsStandardSmooth.{u_1, u_3} R (Localization.Away f)
n : ℕ
φ : RingHom.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg_1 : φ.Etale
algInst : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst : Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
this_1 : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f)
this_2 :
  Ideal.IsPrime (α := Localization.Away f)
    (Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p)
g₀ : Localization.Away f
H : IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ :
  IsLocalization.mk' (Localization.Away f) g
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers f) x)
        ((fun (x : ℕ) ↦ f ^ x) m) ⋯) =
    g₀
hg : g ∉ p
this_3 : IsLocalization.Away (f * g) (Localization.Away g₀)
e : Localization.Away g₀ ≃ₐ[S] Localization.Away (f * g) :=
  IsLocalization.algEquiv (Submonoid.powers (f * g)) (Localization.Away g₀) (Localization.Away (f * g))
this : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away (f * g)) :=
  RingHom.toAlgebra (e.toRingEquiv.toRingHom.comp (algebraMap (MvPolynomial (Fin n) R) (Localization.Away g₀)))
⊢ IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away (f * g))

Tactic:
.of_algebraMap_eq' ?_

Premises used: IsScalarTower.of_algebraMap_eq'
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsSmoothAt R p
f : S
hfp : f ∉ p
H_1 : IsStandardSmooth.{u_1, u_3} R (Localization.Away f)
n : ℕ
φ : RingHom.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg_1 : φ.Etale
algInst : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst : Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
this_1 : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f)
this_2 :
  Ideal.IsPrime (α := Localization.Away f)
    (Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p)
g₀ : Localization.Away f
H : IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ :
  IsLocalization.mk' (Localization.Away f) g
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers f) x)
        ((fun (x : ℕ) ↦ f ^ x) m) ⋯) =
    g₀
hg : g ∉ p
this_3 : IsLocalization.Away (f * g) (Localization.Away g₀)
e : Localization.Away g₀ ≃ₐ[S] Localization.Away (f * g) :=
  IsLocalization.algEquiv (Submonoid.powers (f * g)) (Localization.Away g₀) (Localization.Away (f * g))
this : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away (f * g)) :=
  RingHom.toAlgebra (e.toRingEquiv.toRingHom.comp (algebraMap (MvPolynomial (Fin n) R) (Localization.Away g₀)))
refine :
  Eq (α := RingHom.{u_1, u_3} R (Localization.Away (f * g))) (algebraMap R (Localization.Away (f * g)))
    (@RingHom.comp _ (MvPolynomial (Fin n) R) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (MvPolynomial (Fin n) R) (Localization.Away (f * g))) (algebraMap R (MvPolynomial (Fin n) R)))
⊢ IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away (f * g))

Tactic:
refine .of_algebraMap_eq' ?_
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsSmoothAt R p
f : S
hfp : f ∉ p
H_1 : IsStandardSmooth.{u_1, u_3} R (Localization.Away f)
n : ℕ
φ : RingHom.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg_1 : φ.Etale
algInst : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst : Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
this_1 : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f)
this_2 :
  Ideal.IsPrime (α := Localization.Away f)
    (Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p)
g₀ : Localization.Away f
H : IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ :
  IsLocalization.mk' (Localization.Away f) g
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers f) x)
        ((fun (x : ℕ) ↦ f ^ x) m) ⋯) =
    g₀
hg : g ∉ p
this_3 : IsLocalization.Away (f * g) (Localization.Away g₀)
e : Localization.Away g₀ ≃ₐ[S] Localization.Away (f * g) :=
  IsLocalization.algEquiv (Submonoid.powers (f * g)) (Localization.Away g₀) (Localization.Away (f * g))
this : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away (f * g)) :=
  RingHom.toAlgebra (e.toRingEquiv.toRingHom.comp (algebraMap (MvPolynomial (Fin n) R) (Localization.Away g₀)))
simp :
  Eq (α := RingHom.{u_1, u_3} R (Localization.Away (f * g))) (algebraMap R (Localization.Away (f * g)))
    (e.toRingEquiv.toRingHom.comp (algebraMap R (Localization.Away g₀)))
⊢ Eq (α := RingHom.{u_1, u_3} R (Localization.Away (f * g))) (algebraMap R (Localization.Away (f * g)))
    (@RingHom.comp _ (MvPolynomial (Fin n) R) _ _ Semiring.toNonAssocSemiring _
      (algebraMap (MvPolynomial (Fin n) R) (Localization.Away (f * g))) (algebraMap R (MvPolynomial (Fin n) R)))

Tactic:
simp only [RingHom.algebraMap_toAlgebra, RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq]

Premises used: RingHom.comp_assoc, IsScalarTower.algebraMap_eq, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal S
inst_3 : p.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsSmoothAt R p
f : S
hfp : f ∉ p
H_1 : IsStandardSmooth.{u_1, u_3} R (Localization.Away f)
n : ℕ
φ : RingHom.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg_1 : φ.Etale
algInst : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst : Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
this_1 : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f)
this_2 :
  Ideal.IsPrime (α := Localization.Away f)
    (Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p)
g₀ : Localization.Away f
H : IsStandardEtale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ :
  IsLocalization.mk' (Localization.Away f) g
      (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (Submonoid.powers f) x)
        ((fun (x : ℕ) ↦ f ^ x) m) ⋯) =
    g₀
hg : g ∉ p
this_3 : IsLocalization.Away (f * g) (Localization.Away g₀)
e : Localization.Away g₀ ≃ₐ[S] Localization.Away (f * g) :=
  IsLocalization.algEquiv (Submonoid.powers (f * g)) (Localization.Away g₀) (Localization.Away (f * g))
this : Algebra.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away (f * g)) :=
  RingHom.toAlgebra (e.toRingEquiv.toRingHom.comp (algebraMap (MvPolynomial (Fin n) R) (Localization.Away g₀)))
⊢ Eq (α := RingHom.{u_1, u_3} R (Localization.Away (f * g))) (algebraMap R (Localization.Away (f * g)))
    (e.toRingEquiv.toRingHom.comp (algebraMap R (Localization.Away g₀)))

Tactic:
(e.toAlgHom.comp_algebraMap_of_tower (R := R)).symm

Premises used: AlgEquiv.toAlgHom, AlgHom.comp_algebraMap_of_tower, MonoidHomClass.toMonoidHom, MulEquiv.toMonoidHom, RingHomClass.toRingHom, RingEquiv.toRingHom, Eq.symm