-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
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)
⊢ ∃ 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)
have 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)
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'⟩