-- 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
obtain :
  ∀ (f : S) (hfp : f ∉ p) (H : IsStandardSmooth.{u_1, u_3} 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)
obtain₁ :
  ∀ (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),
    ∃ 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)
obtain₂ :
  ∀ (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),
    Etale.{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)
obtain₃ :
  ∀ (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),
    let algInst := φ.toAlgebra;
    Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) →
      ∀ (this : IsScalarTower.{u_1, u_1, u_3} R (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)
obtain₄ :
  ∀ (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),
    let algInst := φ.toAlgebra;
    Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) →
      ∀ (this : 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)),
        ∃ 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)
obtain₅ :
  ∀ (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),
    let algInst := φ.toAlgebra;
    Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) →
      ∀ (this : 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₀)),
        ∃ 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)
obtain₆ :
  ∀ (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),
    let algInst := φ.toAlgebra;
    Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) →
      ∀ (this : 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₀),
        ∃ 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)
obtain₇ :
  ∀ (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),
    let algInst := φ.toAlgebra;
    Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) →
      ∀ (this : 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),
        ∃ 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)
obtain₈ obtain₉ obtain₁₀ :
  ∀ (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),
    let algInst := φ.toAlgebra;
    Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) →
      ∀ (this : 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) (this : IsLocalization.Away (f * g) (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)
obtain₁₁ obtain₁₂ :
  ∀ (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),
    let algInst := φ.toAlgebra;
    Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f) →
      ∀ (this : 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) (this : IsLocalization.Away (f * g) (Localization.Away g₀)),
        let e : Localization.Away g₀ ≃ₐ[S] Localization.Away (f * g) :=
          IsLocalization.algEquiv (Submonoid.powers (f * g)) (Localization.Away g₀) (Localization.Away (f * g));
        let 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₀)));
        ∀ (this : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away (f * 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:
classical
  obtain ⟨f, hfp, H⟩ := IsSmoothAt.exists_notMem_isStandardSmooth R p
  obtain ⟨n, φ, hgC, hg⟩ := RingHom.IsStandardSmooth.exists_etale_mvPolynomial
    (f := algebraMap R (Localization.Away f)) (by simpa [RingHom.isStandardSmooth_algebraMap])
  algebraize [φ]
  have := IsScalarTower.of_algebraMap_eq' hgC.symm
  have : (Ideal.map (algebraMap S (Localization.Away f)) p).IsPrime :=
    IsLocalization.isPrime_of_isPrime_disjoint (.powers f) _ _ ‹_›
      ((Ideal.disjoint_powers_iff_notMem_of_isPrime _).mpr hfp)
  obtain ⟨g₀, hg, H⟩ := IsEtaleAt.exists_isStandardEtale (R := (MvPolynomial (Fin n) R))
    (S := (Localization.Away f)) (p.map (algebraMap _ _))
  obtain ⟨g, ⟨_, m, rfl⟩, hg₀⟩ := IsLocalization.exists_mk'_eq (.powers f) g₀
  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
  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]
  let e : Localization.Away g₀ ≃ₐ[S] Localization.Away (f * g) :=
    IsLocalization.algEquiv (.powers (f * g)) _ _
  let : Algebra (MvPolynomial (Fin n) R) (Localization.Away (f * g)) :=
    (e.toRingHom.comp (algebraMap (MvPolynomial (Fin n) R) _)).toAlgebra
  have : IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away (f * g)) := by
    refine .of_algebraMap_eq' ?_
    simp only [RingHom.algebraMap_toAlgebra, RingHom.comp_assoc, ← IsScalarTower.algebraMap_eq]
    exact (e.toAlgHom.comp_algebraMap_of_tower (R := R)).symm
  let e' : Localization.Away g₀ ≃ₐ[MvPolynomial (Fin n) R] Localization.Away (f * g) :=
    { __ := e, commutes' r := rfl }
  exact ⟨f * g, ‹p.IsPrime›.mul_notMem ‹_› ‹_›, n, ‹_›, ‹_›, .of_equiv e'⟩

Premises used: Algebra.IsSmoothAt.exists_notMem_isStandardSmooth, rfl