Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : FinitePresentation R S
inst✝ : IsSmoothAt R p
f : S
hfp : f ∉ p
H✝ : IsStandardSmooth R (Localization.Away f)
n : ℕ
φ : MvPolynomial (Fin n) R →+* Localization.Away f
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg✝ : φ.Etale
algInst✝ : Algebra (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst✝ : Etale (MvPolynomial (Fin n) R) (Localization.Away f)
this✝² : IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f)
this✝¹ : (Ideal.map (algebraMap S (Localization.Away f)) p).IsPrime
g₀ : Localization.Away f
H : IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ : IsLocalization.mk' (Localization.Away f) g ⟨(fun x ↦ f ^ x) m, ⋯⟩ = g₀
hg : g ∉ p
this✝ : 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 (MvPolynomial (Fin n) R) (Localization.Away (f * g)) :=
  (e.toRingEquiv.toRingHom.comp (algebraMap (MvPolynomial (Fin n) R) (Localization.Away g₀))).toAlgebra
⊢ ∃ f ∉ p,
    ∃ n x,
      IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
        IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away f)

Tactic:
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

Goal state after:
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal S
inst✝² : p.IsPrime
inst✝¹ : FinitePresentation R S
inst✝ : IsSmoothAt R p
f : S
hfp : f ∉ p
H✝ : IsStandardSmooth R (Localization.Away f)
n : ℕ
φ : MvPolynomial (Fin n) R →+* Localization.Away f
hgC : φ.comp MvPolynomial.C = algebraMap R (Localization.Away f)
hg✝ : φ.Etale
algInst✝ : Algebra (MvPolynomial (Fin n) R) (Localization.Away f) := φ.toAlgebra
algebraizeInst✝ : Etale (MvPolynomial (Fin n) R) (Localization.Away f)
this✝³ : IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f)
this✝² : (Ideal.map (algebraMap S (Localization.Away f)) p).IsPrime
g₀ : Localization.Away f
H : IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away g₀)
g : S
m : ℕ
hg₀ : IsLocalization.mk' (Localization.Away f) g ⟨(fun x ↦ f ^ x) m, ⋯⟩ = g₀
hg : g ∉ p
this✝¹ : 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 (MvPolynomial (Fin n) R) (Localization.Away (f * g)) :=
  (e.toRingEquiv.toRingHom.comp (algebraMap (MvPolynomial (Fin n) R) (Localization.Away g₀))).toAlgebra
this : IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away (f * g))
⊢ ∃ f ∉ p,
    ∃ n x,
      IsScalarTower R (MvPolynomial (Fin n) R) (Localization.Away f) ∧
        IsStandardEtale (MvPolynomial (Fin n) R) (Localization.Away f)