awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
x : S
hQ' : Eq (α := Set (Ideal S)) (Ideal.primesOver (A := ↥R[x]) (Ideal.under (↥R[x]) Q) S) {Q}
hQ'Q :
  Function.Bijective.{u_3 + 1, u_3 + 1} (α := Ideal.ResidueField (R := ↥R[x]) (Ideal.under (↥R[x]) Q)) (β :=
    Q.ResidueField)
    (⇑(algebraMap (Ideal.ResidueField (R := ↥R[x]) (Ideal.under (↥R[x]) Q)) Q.ResidueField) :
      (a : (Ideal.under (↥R[x]) Q).ResidueField) → Q.ResidueField)
S' : Subalgebra R S := R[x]
Q' : Ideal ↥S' := Ideal.under (↥S') Q
this_1 : Algebra (Localization.AtPrime Q') (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver Q' Q
this_2 : Module.Finite (↥S') S
this_3 : IsUnramifiedAt (↥S') Q
hφ :
  Function.Bijective (α := Localization.AtPrime Q') (β := Localization.AtPrime Q)
    (⇑(Localization.localRingHom Q' Q (↑S'.val : ↥S' →+* S) ⋯) : (a : Localization.AtPrime Q') → Localization.AtPrime Q)
r : ↥R[x]
hrQ' : r ∉ Ideal.under (↥R[x]) Q
H :
  ∀ (r' : ↥R[x]),
    r ∣ r' →
      Function.Bijective (α := Localization.Away r') (β :=
        Localization.Away (M := S) ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) r' : S))
        (⇑(Localization.awayMap (algebraMap (↥R[x]) S) r') :
          (a : Localization.Away r') → Localization.Away ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) r'))
this_4 : Module.Finite.{u_1, u_3} R ↥S'
this : IsUnramifiedAt R Q'
f : ↥S'
hfQ' : f ∉ Q'
hf : HasStandardEtaleSurjectionOn R f
P : StandardEtalePair R
φ : AlgHom.{u_1, u_1, u_3} R P.Ring (Localization.Away (f * r))
hP :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := P.Ring) (β := Localization.Away (f * r))
    (⇑φ : (a : P.Ring) → Localization.Away (f * r))
⊢ r ∣ f * r

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 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
x : S
hQ' : Eq (α := Set (Ideal S)) (Ideal.primesOver (A := ↥R[x]) (Ideal.under (↥R[x]) Q) S) {Q}
hQ'Q :
  Function.Bijective.{u_3 + 1, u_3 + 1} (α := Ideal.ResidueField (R := ↥R[x]) (Ideal.under (↥R[x]) Q)) (β :=
    Q.ResidueField)
    (⇑(algebraMap (Ideal.ResidueField (R := ↥R[x]) (Ideal.under (↥R[x]) Q)) Q.ResidueField) :
      (a : (Ideal.under (↥R[x]) Q).ResidueField) → Q.ResidueField)
S' : Subalgebra R S := R[x]
Q' : Ideal ↥S' := Ideal.under (↥S') Q
this_1 : Algebra (Localization.AtPrime Q') (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver Q' Q
this_2 : Module.Finite (↥S') S
this_3 : IsUnramifiedAt (↥S') Q
hφ :
  Function.Bijective (α := Localization.AtPrime Q') (β := Localization.AtPrime Q)
    (⇑(Localization.localRingHom Q' Q (↑S'.val : ↥S' →+* S) ⋯) : (a : Localization.AtPrime Q') → Localization.AtPrime Q)
r : ↥R[x]
hrQ' : r ∉ Ideal.under (↥R[x]) Q
H :
  ∀ (r' : ↥R[x]),
    r ∣ r' →
      Function.Bijective (α := Localization.Away r') (β :=
        Localization.Away (M := S) ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) r' : S))
        (⇑(Localization.awayMap (algebraMap (↥R[x]) S) r') :
          (a : Localization.Away r') → Localization.Away ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) r'))
this_4 : Module.Finite.{u_1, u_3} R ↥S'
this : IsUnramifiedAt R Q'
f : ↥S'
hfQ' : f ∉ Q'
hf : HasStandardEtaleSurjectionOn R f
P : StandardEtalePair R
φ : AlgHom.{u_1, u_1, u_3} R P.Ring (Localization.Away (f * r))
hP :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := P.Ring) (β := Localization.Away (f * r))
    (⇑φ : (a : P.Ring) → Localization.Away (f * r))
⊢ Function.Surjective.{u_1 + 1, u_3 + 1} (α := P.Ring) (β :=
    Localization.Away (M := S) ((IsScalarTower.toAlgHom R (↥S') S : (a : ↥S') → S) (f * r) : S))
    (⇑(AlgHom.comp (Localization.awayMapₐ (IsScalarTower.toAlgHom R (↥S') S) (f * r)) φ) :
      (a : P.Ring) → Localization.Away ((IsScalarTower.toAlgHom R (↥S') S : (a : ↥S') → S) (f * r)))

Tactic:
exact (H _ (by simp)).surjective.comp hP

Premises used: Function.Bijective.surjective, Function.Surjective.comp
-- 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 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
x : S
hQ' : Eq (α := Set (Ideal S)) (Ideal.primesOver (A := ↥R[x]) (Ideal.under (↥R[x]) Q) S) {Q}
hQ'Q :
  Function.Bijective.{u_3 + 1, u_3 + 1} (α := Ideal.ResidueField (R := ↥R[x]) (Ideal.under (↥R[x]) Q)) (β :=
    Q.ResidueField)
    (⇑(algebraMap (Ideal.ResidueField (R := ↥R[x]) (Ideal.under (↥R[x]) Q)) Q.ResidueField) :
      (a : (Ideal.under (↥R[x]) Q).ResidueField) → Q.ResidueField)
S' : Subalgebra R S := R[x]
Q' : Ideal ↥S' := Ideal.under (↥S') Q
this_1 : Algebra (Localization.AtPrime Q') (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver Q' Q
this_2 : Module.Finite (↥S') S
this_3 : IsUnramifiedAt (↥S') Q
hφ :
  Function.Bijective (α := Localization.AtPrime Q') (β := Localization.AtPrime Q)
    (⇑(Localization.localRingHom Q' Q (↑S'.val : ↥S' →+* S) ⋯) : (a : Localization.AtPrime Q') → Localization.AtPrime Q)
r : ↥R[x]
hrQ' : r ∉ Ideal.under (↥R[x]) Q
H :
  ∀ (r' : ↥R[x]),
    r ∣ r' →
      Function.Bijective (α := Localization.Away r') (β :=
        Localization.Away (M := S) ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) r' : S))
        (⇑(Localization.awayMap (algebraMap (↥R[x]) S) r') :
          (a : Localization.Away r') → Localization.Away ((algebraMap (↥R[x]) S : (a : ↥R[x]) → S) r'))
this_4 : Module.Finite.{u_1, u_3} R ↥S'
this : IsUnramifiedAt R Q'
f : ↥S'
hfQ' : f ∉ Q'
hf : HasStandardEtaleSurjectionOn R f
P : StandardEtalePair R
φ : AlgHom.{u_1, u_1, u_3} R P.Ring (Localization.Away (f * r))
hP :
  Function.Surjective.{u_1 + 1, u_3 + 1} (α := P.Ring) (β := Localization.Away (f * r))
    (⇑φ : (a : P.Ring) → Localization.Away (f * r))
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
exact ⟨_, (inferInstance : Q'.IsPrime).mul_notMem hfQ' hrQ', .mk
    (f := IsScalarTower.toAlgHom R S' S (f * r))
    ((Localization.awayMapₐ (IsScalarTower.toAlgHom _ _ S) (f * r)).comp φ)
    (by exact (H _ (by simp)).surjective.comp hP)⟩
-- 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 : FiniteType R S
inst_5 : IsUnramifiedAt R Q
inr :
  ∀
    (this :
      ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_6 : CommRing S] [inst_7 : Algebra R S] (Q : Ideal S)
        [inst_8 : Q.IsPrime] [FiniteType R S] [IsUnramifiedAt R Q] (H : Unramified R S),
        ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f)
    (H : ¬Unramified R S), ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
wlog :
  ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_6 : CommRing S] [inst_7 : Algebra R S] (Q : Ideal S)
    [inst_8 : Q.IsPrime] [FiniteType R S] [IsUnramifiedAt R Q] (H : Unramified R S),
    ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
wlog H : Unramified R S

Premises used: Algebra.Unramified
-- 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 : FiniteType R S
inst_5 : IsUnramifiedAt R Q
this :
  ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_6 : CommRing S] [inst_7 : Algebra R S] (Q : Ideal S)
    [inst_8 : Q.IsPrime] [FiniteType R S] [IsUnramifiedAt R Q] (H : Unramified R S),
    ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
H : ¬Unramified R S
inr :
  ∀ (s : S) (hsQ : s ∉ Q) (hs : FormallyUnramified.{u_3, u_1} R (Localization.Away s)),
    ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
obtain ⟨s, hsQ, hs⟩ := exists_formallyUnramified_of_isUnramifiedAt (R := R) Q

Premises used: Algebra.exists_formallyUnramified_of_isUnramifiedAt
-- 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 : FiniteType R S
inst_5 : IsUnramifiedAt R Q
this :
  ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_6 : CommRing S] [inst_7 : Algebra R S] (Q : Ideal S)
    [inst_8 : Q.IsPrime] [FiniteType R S] [IsUnramifiedAt R Q] (H : Unramified R S),
    ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
H : ¬Unramified R S
s : S
hsQ : s ∉ Q
hs : FormallyUnramified.{u_3, u_1} R (Localization.Away s)
⊢ Disjoint (↑(Submonoid.powers s) : Set S) (↑Q : Set S)

Tactic:
simp [Set.disjoint_iff,
        Set.ext_iff, Submonoid.mem_powers_iff, mt (‹Q.IsPrime›.mem_of_pow_mem _) hsQ]

Premises used: Ideal.IsPrime.mem_of_pow_mem, mt, Submonoid.mem_powers_iff, Set.ext_iff, Set.disjoint_iff
-- 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 : FiniteType R S
inst_5 : IsUnramifiedAt R Q
this :
  ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_6 : CommRing S] [inst_7 : Algebra R S] (Q : Ideal S)
    [inst_8 : Q.IsPrime] [FiniteType R S] [IsUnramifiedAt R Q] (H : Unramified R S),
    ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
H : ¬Unramified R S
s : S
hsQ : s ∉ Q
hs : FormallyUnramified.{u_3, u_1} R (Localization.Away s)
⊢ Ideal.IsPrime (α := Localization.Away s)
    (Ideal.map (F := S →+* Localization.Away s) (algebraMap S (Localization.Away s)) Q)

Tactic:
have hQ : (Ideal.map (algebraMap S (Localization.Away s)) Q).IsPrime :=
      IsLocalization.isPrime_of_isPrime_disjoint (.powers s) _ _ ‹_› (by simp [Set.disjoint_iff,
        Set.ext_iff, Submonoid.mem_powers_iff, mt (‹Q.IsPrime›.mem_of_pow_mem _) hsQ])
-- 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 : FiniteType R S
inst_5 : IsUnramifiedAt R Q
this :
  ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_6 : CommRing S] [inst_7 : Algebra R S] (Q : Ideal S)
    [inst_8 : Q.IsPrime] [FiniteType R S] [IsUnramifiedAt R Q] (H : Unramified R S),
    ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
H : ¬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)
⊢ Unramified.{u_1, u_3} R (Localization.Away s)

Tactic:
have inst : Unramified R (Localization.Away s) := {}
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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 : ¬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)
inr :
  ∀ (f : Localization.Away s)
    (hf : f ∉ Ideal.map (F := S →+* Localization.Away s) (algebraMap S (Localization.Away s)) Q)
    (H : HasStandardEtaleSurjectionOn R f), ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
obtain ⟨f, hf, H⟩ := this (R := R)
      (Q.map (algebraMap _ (Localization.Away s))) inferInstance

Premises used: Algebra.algebraMap, Localization.Away, inferInstance, Ideal.map
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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 : Localization.Away s
hf : f ∉ Ideal.map (F := S →+* Localization.Away s) (algebraMap S (Localization.Away s)) Q
H : HasStandardEtaleSurjectionOn R f
inr :
  ∀ (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)),
    ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
obtain ⟨f, t, rfl⟩ := IsLocalization.exists_mk'_eq (.powers s) f

Premises used: Submonoid.powers, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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)
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
⟨s * f, ?_, ?_⟩

Premises used: HMul.hMul, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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
inr₁ : HasStandardEtaleSurjectionOn R (s * f)
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
refine ⟨s * f, ?_, ?_⟩
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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)
⊢ s * f ∉ Q

Tactic:
simpa [IsLocalization.mk'_mem_map_algebraMap_iff, Submonoid.mem_powers_iff,
        Ideal.IsPrime.mul_mem_left_iff, hsQ, (mt (‹Q.IsPrime›.mem_of_pow_mem _) hsQ)] using hf

Premises used: Ideal.IsPrime.mem_of_pow_mem, mt, IsLocalization.mk'_mem_map_algebraMap_iff, Submonoid.mem_powers_iff, Ideal.IsPrime.mul_mem_left_iff
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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)
⊢ (algebraMap S (Localization.Away s) : (a : S) → Localization.Away s) f =
    HMul.hMul (α := Localization.Away s) (β := Localization.Away s)
      (IsLocalization.mk' (Localization.Away s) f t : Localization.Away s)
      ((algebraMap S (Localization.Away s) : (a : S) → Localization.Away s) (↑t : S) : Localization.Away s)

Tactic:
simp
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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 :
  ∀ (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)
⊢ HasStandardEtaleSurjectionOn R (s * f)

Tactic:
obtain ⟨P, φ, hφ⟩ : HasStandardEtaleSurjectionOn R (algebraMap S (Localization.Away s) f) :=
      H.of_dvd ⟨algebraMap _ _ t.1, by simp⟩

Premises used: HasStandardEtaleSurjectionOn.of_dvd, Algebra.algebraMap, Localization.Away, HasStandardEtaleSurjectionOn, Exists.intro, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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)
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:
.mk _ hφ

Premises used: HasStandardEtaleSurjectionOn.mk
-- Module: Mathlib.RingTheory.Unramified.LocalStructure
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)
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:
exact .mk _ hφ