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 : 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}
⊢ ∃ (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)
have 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)
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
-- 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 : Module.Finite R S
inst_5 : IsUnramifiedAt R Q
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have 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
Tactic: obtain ⟨x, hQ', hQ'Q⟩ :=
    exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective (R := R) Q
-- 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 : 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
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have this₁ : Module.Finite (↥S') S
Tactic: have : Module.Finite S' S := .of_restrictScalars_finite R _ _
-- 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 : 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
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have this₁ : IsUnramifiedAt (↥S') Q
Tactic: have : IsUnramifiedAt S' Q := .of_restrictScalars R _
-- 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 : 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
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have hφ : Function.Bijective (α := Localization.AtPrime Q') (β := Localization.AtPrime Q)
  (⇑(Localization.localRingHom Q' Q (↑S'.val : ↥S' →+* S) sorry) : (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⟩
-- 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 : 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)
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have 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
Tactic: obtain ⟨r, hrQ', H⟩ := Localization.exists_awayMap_bijective_of_residueField_surjective hQ' hQ'Q.2
-- 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 : 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'))
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have this₁ : Module.Finite.{u_1, u_3} R ↥S'
Tactic: have : Module.Finite R S' := finite_adjoin_simple_of_isIntegral (IsIntegral.isIntegral _)
-- 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 : 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'
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have this₁ : IsUnramifiedAt R Q'
Tactic: have : IsUnramifiedAt R Q' := .of_equiv <| .symm <| .ofBijective (IsScalarTower.toAlgHom _ _ _) 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
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 ∉ Q, HasStandardEtaleSurjectionOn R f
have obtain : ∀ (f : ↥S') (hfQ' : f ∉ Q') (hf : 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'
-- 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 : 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 ∉ Q, HasStandardEtaleSurjectionOn R f
have 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
Tactic: obtain ⟨P, φ, hP⟩ := hf.of_dvd (g := f * r) (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 : FiniteType R S
inst_5 : IsUnramifiedAt R Q
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have 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
Tactic: wlog H : Unramified R S
-- 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 : 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
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have 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
Tactic: wlog H : Unramified R S
Cleared hypotheses: Q, inst_3, inst_4, inst_5
-- 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 : 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
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have inr : ∀ (s : S) (hsQ : s ∉ Q) (hs : FormallyUnramified.{u_3, u_1} R (Localization.Away s)),
  ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
Tactic: obtain ⟨s, hsQ, hs⟩ := exists_formallyUnramified_of_isUnramifiedAt (R := R) Q
-- 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 : 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)
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have hQ : 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])
-- 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 : 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)
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have inst : Unramified.{u_1, u_3} R (Localization.Away s)
Tactic: have inst : Unramified R (Localization.Away s) := {}
-- 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 : ¬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 ∉ Q, HasStandardEtaleSurjectionOn R f
have 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
Tactic: obtain ⟨f, hf, H⟩ := this (R := R)
      (Q.map (algebraMap _ (Localization.Away s))) inferInstance
-- 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 : 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
have 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
Tactic: obtain ⟨f, t, rfl⟩ := IsLocalization.exists_mk'_eq (.powers s) f
Cleared hypotheses: f, hf, H
-- 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)
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have inr : s * f ∉ Q
Tactic: refine ⟨s * f, ?_, ?_⟩