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
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ (Q' : Ideal S), Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q'
ht :
  Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
    (Ideal.ResidueField
        (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
    ⊤
p : Ideal R := Ideal.under R Q
this_2 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this : Algebra (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
h :
  Eq (α := Q.ResidueField)
    ((algebraMap (↥R[t]) Q.ResidueField : (a : ↥R[t]) → Q.ResidueField)
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[t] x) t ⋯) :
      Q.ResidueField)
    ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)
⊢ Eq (α := Q.ResidueField)
    ((AlgHom.toRingHom.{u_1, u_3, u_3} (R := p.ResidueField)
            (IsScalarTower.toAlgHom p.ResidueField (Ideal.ResidueField (R := ↥R[t]) (Ideal.under (↥R[t]) Q))
              Q.ResidueField) :
          (a : (Ideal.under (↥R[t]) Q).ResidueField) → Q.ResidueField)
        ((algebraMap (↥R[t]) (Ideal.ResidueField (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) :
            (a : ↥R[t]) → (Ideal.under (↥R[t]) Q).ResidueField)
          (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[t] x) t ⋯)) :
      Q.ResidueField)
    ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)

Tactic:
rw [AlgHom.toRingHom_eq_coe, IsScalarTower.coe_toAlgHom, ← IsScalarTower.algebraMap_apply]

Premises used: IsScalarTower.coe_toAlgHom, AlgHom.toRingHom_eq_coe, IsScalarTower.algebraMap_apply
-- 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
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ (Q' : Ideal S), Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q'
ht :
  Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
    (Ideal.ResidueField
        (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
    ⊤
p : Ideal R := Ideal.under R Q
this_2 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this : Algebra (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
⊢ Eq (α := Q.ResidueField)
    ((algebraMap (↥R[t]) Q.ResidueField : (a : ↥R[t]) → Q.ResidueField)
        (Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Subalgebra R S) R[t] x) t ⋯) :
      Q.ResidueField)
    ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)

Tactic:
rfl
-- 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
this_1 : Algebra.{u_1, u_3} (Localization.AtPrime (Ideal.under R Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under R Q) Q
t : S
htQ : t ∉ Q
htQ' : ∀ (Q' : Ideal S), Membership.mem (γ := Set (Ideal S)) (Ideal.primesOver (Ideal.under R Q) S) Q' → Q' ≠ Q → t ∈ Q'
ht :
  Eq (α := Subalgebra.{u_1, u_3} (Ideal.ResidueField (Ideal.under R Q)) Q.ResidueField)
    (Ideal.ResidueField
        (Ideal.under R Q))[((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) t : Q.ResidueField)]
    ⊤
p : Ideal R := Ideal.under R Q
this_2 : Algebra.{u_1, u_3} (Localization.AtPrime p) (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) :=
  Localization.AtPrime.algebraOfLiesOver p (Ideal.under (↥R[t]) Q)
this : Algebra (Localization.AtPrime (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↥R[t]) Q) Q
refine_1 : Eq (α := Set (Ideal S)) (Ideal.primesOver (A := ↥R[t]) (Ideal.under (↥R[t]) Q) S) {Q}
refine_2 refine_2₁ :
  Function.Surjective.{u_3 + 1, u_3 + 1} (α := Ideal.ResidueField (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) (β :=
    Q.ResidueField)
    (⇑(algebraMap (Ideal.ResidueField (R := ↥R[t]) (Ideal.under (↥R[t]) Q)) Q.ResidueField) :
      (a : (Ideal.under (↥R[t]) Q).ResidueField) → Q.ResidueField)
⊢ ∃ (x : S),
    Eq (α := Set (Ideal S)) (Ideal.primesOver (A := ↥R[x]) (Ideal.under (↥R[x]) Q) S) {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)

Tactic:
classical
  refine ⟨t, ?_, RingHom.injective _, ?_⟩
  · refine Set.ext fun Q' ↦ ⟨fun ⟨_, _⟩ ↦ ?_, fun e ↦ by exact ⟨e ▸ inferInstance, ⟨e ▸ rfl⟩⟩⟩
    by_contra! H
    have : Q'.LiesOver p := .trans _ (Q.under (R[t])) _
    exact htQ (SetLike.le_def.mp (Q'.over_def (Q.under (R[t]))).ge
      (x := ⟨t, self_mem_adjoin_singleton _ _⟩) (htQ' Q' ⟨‹_›, ‹_›⟩ H))
  · change Function.Surjective (IsScalarTower.toAlgHom p.ResidueField _ _)
    rw [← AlgHom.range_eq_top, ← top_le_iff, ← ht]
    refine adjoin_singleton_le ?_
    use algebraMap (R[t]) _ ⟨t, self_mem_adjoin_singleton _ _⟩
    rw [AlgHom.toRingHom_eq_coe, IsScalarTower.coe_toAlgHom, ← IsScalarTower.algebraMap_apply]
    rfl

Premises used: Algebra.algebraMap, IsScalarTower.toAlgHom, Algebra.adjoin, Membership.mem, Ideal.ResidueField, Algebra.adjoin_singleton_le, Subtype, IsScalarTower.coe_toAlgHom, AlgHom.range_eq_top, Subtype.mk, AlgHom.toRingHom_eq_coe, top_le_iff, Singleton.singleton, DFunLike.coe, IsScalarTower.algebraMap_apply, Function.Surjective, Algebra.self_mem_adjoin_singleton
-- 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
obtain :
  ∀ (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)),
    ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
obtain ⟨x, hQ', hQ'Q⟩ :=
    exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective (R := R) Q

Premises used: Algebra.IsUnramifiedAt.exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective
-- 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 : Algebra (Localization.AtPrime Q') (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver Q' Q
⊢ Module.Finite (↥S') S

Tactic:
have : Module.Finite S' S := .of_restrictScalars_finite R _ _
-- 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 : Module.Finite (↥S') S
⊢ IsUnramifiedAt (↥S') Q

Tactic:
have : IsUnramifiedAt S' Q := .of_restrictScalars R _
-- 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 : IsUnramifiedAt (↥S') Q
⊢ Function.Bijective (α := Localization.AtPrime Q') (β := Localization.AtPrime Q)
    (⇑(Localization.localRingHom Q' Q (↑S'.val : ↥S' →+* S) ⋯) : (a : Localization.AtPrime Q') → Localization.AtPrime Q)

Tactic:
have hφ : Function.Bijective (Localization.localRingHom Q' Q S'.val rfl) :=
    ⟨Localization.localRingHom_injective_of_primesOver_eq_singleton hQ',
      Localization.localRingHom_surjective_of_primesOver_eq_singleton hQ' hQ'Q.2⟩
-- 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 : 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)
obtain :
  ∀ (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'))),
    ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
obtain ⟨r, hrQ', H⟩ := Localization.exists_awayMap_bijective_of_residueField_surjective hQ' hQ'Q.2

Premises used: Localization.exists_awayMap_bijective_of_residueField_surjective, And.right
-- 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 : 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'))
⊢ Module.Finite.{u_1, u_3} R ↥S'

Tactic:
have : Module.Finite R S' := finite_adjoin_simple_of_isIntegral (IsIntegral.isIntegral _)
-- 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 : Module.Finite.{u_1, u_3} R ↥S'
⊢ IsUnramifiedAt R Q'

Tactic:
have : IsUnramifiedAt R Q' := .of_equiv <| .symm <| .ofBijective (IsScalarTower.toAlgHom _ _ _) 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 : 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'
⊢ Subalgebra.map S'.val R[Subtype.mk (p := fun (x : S) ↦ x ∈ S') x ⋯] = Subalgebra.map S'.val ⊤

Tactic:
simp [Subalgebra.range_val, S']

Premises used: Subalgebra.range_val
-- 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'
obtain : ∀ (f : ↥S') (hfQ' : f ∉ Q') (hf : HasStandardEtaleSurjectionOn R f), ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
obtain ⟨f, hfQ', hf⟩ :=
    IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn_of_exists_adjoin_singleton_eq_top
    (R := R) (S := S') ⟨⟨x, self_mem_adjoin_singleton _ _⟩, Subalgebra.map_injective
      (f := S'.val) Subtype.val_injective (by simp [Subalgebra.range_val, S'])⟩ Q'

Premises used: _private.0.Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn_of_exists_adjoin_singleton_eq_top, Subtype.val_injective, Subtype.mk, Subalgebra.map_injective, Exists.intro, Algebra.self_mem_adjoin_singleton
-- 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
⊢ f ∣ 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
obtain :
  ∀ (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
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

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

Premises used: HasStandardEtaleSurjectionOn.of_dvd