awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
Goal:
R : Type u_1
S : Type u_3
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : FiniteType R S
inst_6 : IsUnramifiedAt R Q
this :
  ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_7 : CommRing S] [inst_8 : Algebra R S] (Q : Ideal S)
    [inst_9 : Q.IsPrime] [FiniteType R S] [IsUnramifiedAt R Q] (H : Unramified R S),
    ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
H_1 : ¬Unramified R S
s : S
hsQ : s ∉ Q
hs : FormallyUnramified.{u_3, u_1} R (Localization.Away s)
hQ :
  Ideal.IsPrime (α := Localization.Away s)
    (Ideal.map (F := S →+* Localization.Away s) (algebraMap S (Localization.Away s)) Q)
inst : Unramified.{u_1, u_3} R (Localization.Away s)
f : S
t : ↥(Submonoid.powers s)
hf :
  IsLocalization.mk' (Localization.Away s) f t ∉
    Ideal.map (F := S →+* Localization.Away s) (algebraMap S (Localization.Away s)) Q
H : HasStandardEtaleSurjectionOn R (S := Localization.Away s) (IsLocalization.mk' (Localization.Away s) f t)
inr : s * f ∉ Q
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have inr₁ : HasStandardEtaleSurjectionOn R (s * f)
Tactic: refine ⟨s * f, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
Goal:
R : Type u_1
S : Type u_3
inst_1 : CommRing R
inst_2 : CommRing S
inst_3 : Algebra R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : FiniteType R S
inst_6 : IsUnramifiedAt R Q
this :
  ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_7 : CommRing S] [inst_8 : Algebra R S] (Q : Ideal S)
    [inst_9 : Q.IsPrime] [FiniteType R S] [IsUnramifiedAt R Q] (H : Unramified R S),
    ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
H_1 : ¬Unramified R S
s : S
hsQ : s ∉ Q
hs : FormallyUnramified.{u_3, u_1} R (Localization.Away s)
hQ :
  Ideal.IsPrime (α := Localization.Away s)
    (Ideal.map (F := S →+* Localization.Away s) (algebraMap S (Localization.Away s)) Q)
inst : Unramified.{u_1, u_3} R (Localization.Away s)
f : S
t : ↥(Submonoid.powers s)
hf :
  IsLocalization.mk' (Localization.Away s) f t ∉
    Ideal.map (F := S →+* Localization.Away s) (algebraMap S (Localization.Away s)) Q
H : HasStandardEtaleSurjectionOn R (S := Localization.Away s) (IsLocalization.mk' (Localization.Away s) f t)
⊢ HasStandardEtaleSurjectionOn R (s * f)
have inr : ∀ (P : StandardEtalePair R)
  (φ :
    AlgHom.{u_1, u_1, u_3} R P.Ring
      (Localization.Away (M := Localization.Away s)
        ((algebraMap S (Localization.Away s) : (a : S) → Localization.Away s) f : Localization.Away s)))
  (hφ :
    Function.Surjective.{u_1 + 1, u_3 + 1} (α := P.Ring) (β :=
      Localization.Away (M := Localization.Away s)
        ((algebraMap S (Localization.Away s) : (a : S) → Localization.Away s) f : Localization.Away s))
      (⇑φ : (a : P.Ring) → Localization.Away ((algebraMap S (Localization.Away s) : (a : S) → Localization.Away s) f))),
  HasStandardEtaleSurjectionOn R (s * f)
Tactic: obtain ⟨P, φ, hφ⟩ : HasStandardEtaleSurjectionOn R (algebraMap S (Localization.Away s) f) :=
      H.of_dvd ⟨algebraMap _ _ t.1, by simp⟩
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (hypothesis)
Goal:
R_1 : Type u_1
S_1 : Type u_3
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_1
S : Type u_3
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : FiniteType R S
inst_8 : IsUnramifiedAt R Q
H : Unramified R S
S' : Subalgebra R S
hS' : Submodule.FG.{u_1, u_3} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S')
r : ↥S'
hrQ : (↑r : S) ∉ Q
hr :
  Function.Bijective (α := Localization.Away r) (β :=
    Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
    (⇑(Localization.awayMap S'.val.toRingHom r) :
      (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have this : Module.Finite.{u_1, u_3} R ↥S'
Tactic: have : Module.Finite R S' := ⟨(Submodule.fg_top _).mpr hS'⟩
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (hypothesis)
Goal:
R_1 : Type u_1
S_1 : Type u_3
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_1
S : Type u_3
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : FiniteType R S
inst_8 : IsUnramifiedAt R Q
H : Unramified R S
S' : Subalgebra R S
hS' : Submodule.FG.{u_1, u_3} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S')
r : ↥S'
hrQ : (↑r : S) ∉ Q
hr :
  Function.Bijective (α := Localization.Away r) (β :=
    Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
    (⇑(Localization.awayMap S'.val.toRingHom r) :
      (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
this : Module.Finite.{u_1, u_3} R ↥S'
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have this₁ : FormallyUnramified.{u_3, u_1} R (Localization.Away r)
Tactic: have : FormallyUnramified R (Localization.Away r) :=
    .of_equiv (AlgEquiv.ofBijective (Localization.awayMapₐ S'.val r) hr :).symm
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (hypothesis)
Goal:
R_1 : Type u_1
S_1 : Type u_3
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_1
S : Type u_3
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : FiniteType R S
inst_8 : IsUnramifiedAt R Q
H : Unramified R S
S' : Subalgebra R S
hS' : Submodule.FG.{u_1, u_3} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S')
r : ↥S'
hrQ : (↑r : S) ∉ Q
hr :
  Function.Bijective (α := Localization.Away r) (β :=
    Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
    (⇑(Localization.awayMap S'.val.toRingHom r) :
      (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
this_1 : Module.Finite.{u_1, u_3} R ↥S'
this : FormallyUnramified.{u_3, u_1} R (Localization.Away r)
⊢ IsUnramifiedAt R (A := ↥S') (Ideal.under (↥S') Q)
have this₁ : (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum ↥S')) ⊆ unramifiedLocus R ↥S'
Tactic: rw [← basicOpen_subset_unramifiedLocus_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (hypothesis)
Goal:
R_1 : Type u_1
S_1 : Type u_3
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_1
S : Type u_3
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : FiniteType R S
inst_8 : IsUnramifiedAt R Q
H : Unramified R S
S' : Subalgebra R S
hS' : Submodule.FG.{u_1, u_3} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S')
r : ↥S'
hrQ : (↑r : S) ∉ Q
hr :
  Function.Bijective (α := Localization.Away r) (β :=
    Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
    (⇑(Localization.awayMap S'.val.toRingHom r) :
      (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
this_1 : Module.Finite.{u_1, u_3} R ↥S'
this : FormallyUnramified.{u_3, u_1} R (Localization.Away r)
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have this₁ : IsUnramifiedAt R (A := ↥S') (Ideal.under (↥S') Q)
Tactic: have : IsUnramifiedAt R (Ideal.under (↥S') Q) := by
    rw [← basicOpen_subset_unramifiedLocus_iff] at this
    exact @this ⟨Q.under S', inferInstance⟩ hrQ
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_3
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_1
S : Type u_3
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : FiniteType R S
inst_8 : IsUnramifiedAt R Q
H : Unramified R S
S' : Subalgebra R S
hS' : Submodule.FG.{u_1, u_3} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S')
r : ↥S'
hrQ : (↑r : S) ∉ Q
hr :
  Function.Bijective (α := Localization.Away r) (β :=
    Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
    (⇑(Localization.awayMap S'.val.toRingHom r) :
      (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
this_1 : Module.Finite.{u_1, u_3} R ↥S'
this_2 : FormallyUnramified.{u_3, u_1} R (Localization.Away r)
this : IsUnramifiedAt R (A := ↥S') (Ideal.under (↥S') Q)
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have obtain : ∀ (f : ↥S') (hfQ : f ∉ Ideal.under (↥S') Q) (hf : HasStandardEtaleSurjectionOn R f),
  ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
Tactic: obtain ⟨f, hfQ, hf⟩ :=
    IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn_of_finite (R := R) (Q.under S')
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (goal)
Goal:
R_1 : Type u_1
S_1 : Type u_3
inst : CommRing R_1
inst_1 : CommRing S_1
inst_2 : Algebra R_1 S_1
R : Type u_1
S : Type u_3
inst_3 : CommRing R
inst_4 : CommRing S
inst_5 : Algebra R S
Q : Ideal S
inst_6 : Q.IsPrime
inst_7 : FiniteType R S
inst_8 : IsUnramifiedAt R Q
H : Unramified R S
S' : Subalgebra R S
hS' : Submodule.FG.{u_1, u_3} (R := R) (M := S) ((Subalgebra.toSubmodule : (a : Subalgebra R S) → Submodule R S) S')
r : ↥S'
hrQ : (↑r : S) ∉ Q
hr :
  Function.Bijective (α := Localization.Away r) (β :=
    Localization.Away (M := S) ((S'.val.toRingHom : (a : ↥S') → S) r : S))
    (⇑(Localization.awayMap S'.val.toRingHom r) :
      (a : Localization.Away r) → Localization.Away ((S'.val.toRingHom : (a : ↥S') → S) r))
this_1 : Module.Finite.{u_1, u_3} R ↥S'
this_2 : FormallyUnramified.{u_3, u_1} R (Localization.Away r)
this : IsUnramifiedAt R (A := ↥S') (Ideal.under (↥S') Q)
f : ↥S'
hfQ : f ∉ Ideal.under (↥S') Q
hf : HasStandardEtaleSurjectionOn R f
e : Localization.Away (r * f) ≃ₐ[R] Localization.Away ((↑r : S) * (↑f : S)) :=
  AlgEquiv.ofBijective (Localization.awayMapₐ S'.val (r * f)) ⋯
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have obtain : ∀ (P : StandardEtalePair R) (φ : AlgHom.{u_1, u_1, u_3} R P.Ring (Localization.Away (r * f)))
  (hφ :
    Function.Surjective.{u_1 + 1, u_3 + 1} (α := P.Ring) (β := Localization.Away (r * f))
      (⇑φ : (a : P.Ring) → Localization.Away (r * f))),
  ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
Tactic: obtain ⟨P, φ, hφ⟩ := hf.of_dvd (g := r * f) (by simp)
-- 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
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsEtaleAt R Q
⊢ ∃ f ∉ Q, IsStandardEtale.{u_1, u_3} R (Localization.Away f)
have obtain : ∀ (f : S) (hfQ : f ∉ Q) (h : Etale.{u_1, u_3} R (Localization.Away f)),
  ∃ f ∉ Q, IsStandardEtale.{u_1, u_3} R (Localization.Away f)
Tactic: obtain ⟨f, hfQ, h⟩ := exists_etale_of_isEtaleAt (R := R) Q
-- 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
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsEtaleAt R Q
f : S
hfQ : f ∉ Q
h : Etale.{u_1, u_3} R (Localization.Away f)
⊢ ∃ f ∉ Q, IsStandardEtale.{u_1, u_3} R (Localization.Away f)
have obtain : ∀ (g : S) (hgQ : g ∉ Q) (hg : HasStandardEtaleSurjectionOn R g),
  ∃ f ∉ Q, IsStandardEtale.{u_1, u_3} R (Localization.Away f)
Tactic: obtain ⟨g, hgQ, hg⟩ := IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn (R := R) Q
-- 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
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsEtaleAt R Q
f : S
hfQ : f ∉ Q
h : Etale.{u_1, u_3} R (Localization.Away f)
g : S
hgQ : g ∉ Q
hg : HasStandardEtaleSurjectionOn R g
⊢ Etale.{u_1, u_3} R (Localization.Away (f * g))
have rw : ∀ (h : (↑(PrimeSpectrum.basicOpen f) : Set (PrimeSpectrum S)) ⊆ etaleLocus R S) (g : S) (hgQ : g ∉ Q)
  (hg : HasStandardEtaleSurjectionOn R g), (↑(PrimeSpectrum.basicOpen (f * g)) : Set (PrimeSpectrum S)) ⊆ etaleLocus R S
Tactic: rw [← basicOpen_subset_etaleLocus_iff_etale] at h ⊢
Cleared hypotheses: h, g, hgQ, hg
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (hypothesis)
Goal:
R : Type u_1
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsEtaleAt R Q
f : S
hfQ : f ∉ Q
h : Etale.{u_1, u_3} R (Localization.Away f)
g : S
hgQ : g ∉ Q
hg : HasStandardEtaleSurjectionOn R g
⊢ ∃ f ∉ Q, IsStandardEtale.{u_1, u_3} R (Localization.Away f)
have this : Etale.{u_1, u_3} R (Localization.Away (f * g))
Tactic: have : Etale R (Localization.Away (f * g)) := by
    rw [← basicOpen_subset_etaleLocus_iff_etale] at h ⊢
    exact .trans (PrimeSpectrum.basicOpen_mul_le_left _ _) h
-- 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
⊢ ∃ 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)),
  ∃ 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 ⟨f, hfp, H⟩ := IsSmoothAt.exists_notMem_isStandardSmooth R p
-- 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
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)
have obtain : ∀ (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)
Tactic: obtain ⟨n, φ, hgC, hg⟩ := RingHom.IsStandardSmooth.exists_etale_mvPolynomial
    (f := algebraMap R (Localization.Away f)) (by simpa [RingHom.isStandardSmooth_algebraMap])
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (hypothesis)
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
⊢ ∃ 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 algebraizeInst : Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)
Tactic: algebraize [φ]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (hypothesis)
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)
⊢ ∃ 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 this : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f)
Tactic: have := IsScalarTower.of_algebraMap_eq' hgC.symm
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (hypothesis)
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 : 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)
have this₁ : Ideal.IsPrime (α := Localization.Away f)
  (Ideal.map (F := S →+* Localization.Away f) (algebraMap S (Localization.Away f)) p)
Tactic: 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)
-- 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
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)
⊢ ∃ 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 : ∀ (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)
Tactic: obtain ⟨g₀, hg, H⟩ := IsEtaleAt.exists_isStandardEtale (R := (MvPolynomial (Fin n) R))
    (S := (Localization.Away f)) (p.map (algebraMap _ _))
-- 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
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₀)
⊢ ∃ 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 : ∀ (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) sorry) =
      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)
Tactic: obtain ⟨g, ⟨_, m, rfl⟩, hg₀⟩ := IsLocalization.exists_mk'_eq (.powers f) g₀
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.LocalStructure (hypothesis)
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₀
⊢ ∃ 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 hg₁ : 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
Cleared hypotheses: hg