awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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))
⊢ Module.Finite.{u_1, u_3} R ↥S'

Tactic:
have : Module.Finite R S' := ⟨(Submodule.fg_top _).mpr hS'⟩
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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'
⊢ 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
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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)
⊢ (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum ↥S')) ⊆ unramifiedLocus R ↥S'

Tactic:
rw [← basicOpen_subset_unramifiedLocus_iff] at this

Premises used: Algebra.basicOpen_subset_unramifiedLocus_iff
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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 : (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum ↥S')) ⊆ unramifiedLocus R ↥S'
⊢ IsUnramifiedAt R (A := ↥S') (Ideal.under (↥S') Q)

Tactic:
@this ⟨Q.under S', inferInstance⟩ hrQ

Premises used: Set.Mem, setOf, Algebra.unramifiedLocus, Ideal.comap
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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 : (↑(PrimeSpectrum.basicOpen r) : Set (PrimeSpectrum ↥S')) ⊆ unramifiedLocus R ↥S'
⊢ IsUnramifiedAt R (A := ↥S') (Ideal.under (↥S') Q)

Tactic:
exact @this ⟨Q.under S', inferInstance⟩ hrQ
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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)

Tactic:
have : IsUnramifiedAt R (Ideal.under (↥S') Q) := by
    rw [← basicOpen_subset_unramifiedLocus_iff] at this
    exact @this ⟨Q.under S', inferInstance⟩ hrQ
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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)
obtain :
  ∀ (f : ↥S') (hfQ : f ∉ Ideal.under (↥S') Q) (hf : HasStandardEtaleSurjectionOn R f),
    ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
obtain ⟨f, hfQ, hf⟩ :=
    IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn_of_finite (R := R) (Q.under S')

Premises used: _private.0.Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn_of_finite, Membership.mem, Subtype, Ideal.under
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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 ∣ r * f

Tactic:
simp
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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)) ⋯
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
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
obtain ⟨P, φ, hφ⟩ := hf.of_dvd (g := r * f) (by simp)

Premises used: HasStandardEtaleSurjectionOn.of_dvd
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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)) ⋯
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:
⟨_, ‹Q.IsPrime›.mul_notMem hrQ hfQ,
    .mk (f := r.1 * f.1) (e.toAlgHom.comp φ) (e.surjective.comp hφ)⟩

Premises used: AlgEquiv.toAlgHom, Ideal.IsPrime.mul_notMem, And.intro, Exists.intro, Function.Surjective.comp, HasStandardEtaleSurjectionOn.mk, AlgHom.comp, AlgEquiv.surjective
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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)) ⋯
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:
refine ⟨_, ‹Q.IsPrime›.mul_notMem hrQ hfQ,
    .mk (f := r.1 * f.1) (e.toAlgHom.comp φ) (e.surjective.comp hφ)⟩
-- 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
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsEtaleAt R Q
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)
⊢ ∃ f ∉ Q, IsStandardEtale.{u_1, u_3} R (Localization.Away f)

Tactic:
obtain ⟨f, hfQ, h⟩ := exists_etale_of_isEtaleAt (R := R) Q

Premises used: Algebra.exists_etale_of_isEtaleAt
-- 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
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)
obtain :
  ∀ (g : S) (hgQ : g ∉ Q) (hg : HasStandardEtaleSurjectionOn R g),
    ∃ f ∉ Q, IsStandardEtale.{u_1, u_3} R (Localization.Away f)
⊢ ∃ f ∉ Q, IsStandardEtale.{u_1, u_3} R (Localization.Away f)

Tactic:
obtain ⟨g, hgQ, hg⟩ := IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn (R := R) Q

Premises used: Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn
-- 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
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
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
⊢ Etale.{u_1, u_3} R (Localization.Away (f * g))

Tactic:
rw [← basicOpen_subset_etaleLocus_iff_etale] at h ⊢

Premises used: Algebra.basicOpen_subset_etaleLocus_iff_etale
-- 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
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsEtaleAt R Q
f : S
hfQ : f ∉ Q
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:
.trans (PrimeSpectrum.basicOpen_mul_le_left _ _) h

Premises used: HasSubset.Subset.trans, PrimeSpectrum.basicOpen_mul_le_left
-- 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
Q : Ideal S
inst_3 : Q.IsPrime
inst_4 : FinitePresentation R S
inst_5 : IsEtaleAt R Q
f : S
hfQ : f ∉ Q
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:
exact .trans (PrimeSpectrum.basicOpen_mul_le_left _ _) h
-- 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
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))

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
-- 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
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
this : Etale.{u_1, u_3} R (Localization.Away (f * g))
⊢ g ∣ f * g

Tactic:
simp
-- 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
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
this : Etale.{u_1, u_3} R (Localization.Away (f * g))
⊢ ∃ f ∉ Q, IsStandardEtale.{u_1, u_3} R (Localization.Away f)

Tactic:
exact ⟨f * g, ‹Q.IsPrime›.mul_notMem hfQ hgQ, (hg.of_dvd (by simp)).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
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)
⊢ ∃ 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

Premises used: Algebra.IsSmoothAt.exists_notMem_isStandardSmooth
-- 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)
⊢ RingHom.IsStandardSmooth.{u_1, u_3} (S := Localization.Away f) (algebraMap R (Localization.Away f))

Tactic:
simpa [RingHom.isStandardSmooth_algebraMap]

Premises used: RingHom.isStandardSmooth_algebraMap
-- 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)
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)
⊢ ∃ 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])

Premises used: RingHom.IsStandardSmooth.exists_etale_mvPolynomial
-- 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
⊢ Etale.{u_1, u_3} (MvPolynomial (Fin n) R) (Localization.Away f)

Tactic:
algebraize [φ]
-- 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)
⊢ IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f)

Tactic:
have := IsScalarTower.of_algebraMap_eq' hgC.symm
-- 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 : IsScalarTower.{u_1, u_1, u_3} R (MvPolynomial (Fin n) R) (Localization.Away f)
⊢ 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)