awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_3 : Module.Finite R S
H : ∃ (x : S), Eq (α := Subalgebra R S) R[x] ⊤
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have this : Nontrivial R
Tactic: have := (algebraMap R S).domain_nontrivial
-- 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
inst_3 : Module.Finite R S
H : ∃ (x : S), Eq (α := Subalgebra R S) R[x] ⊤
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P Q
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have inr : ∀ (x : S) (hx : Eq (α := Subalgebra R S) R[x] ⊤), ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
Tactic: obtain ⟨x, hx⟩ := H
Cleared hypotheses: H
-- 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
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have hRx : IsIntegral R x
Tactic: have hRx : IsIntegral R x := 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
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
Tactic: have hx' : Function.Surjective (aeval (R := R) x) :=
    (AlgHom.range_eq_top _).mp ((adjoin_singleton_eq_range_aeval R x).symm.trans hx)
-- 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
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P : Ideal R := Ideal.under R Q
this_2 : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
this :
  ∃ (q : R[X]),
    q.Monic ∧
      Eq.{u_3 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S) ∧
        ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have obtain : ∀ (q : R[X]) (hq : q.Monic) (hqx : Eq.{u_3 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S))
  (hq'x : ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q),
  ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
Tactic: obtain ⟨q, hq, hqx, hq'x⟩ := this
Cleared hypotheses: this
-- 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
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P_1 : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P_1) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P_1 Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
q : R[X]
hq : q.Monic
hqx : Eq.{u_3 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S)
hq'x : ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
P : StandardEtalePair R := { f := q, monic_f := hq, g := (derivative : (a : R[X]) → R[X]) q, cond := ⋯ }
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have hP : P.HasMap (S := Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))
  ((algebraMap S
          (Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S)) :
        (a : S) → Localization.Away ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q)))
      x :
    Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))
Tactic: have hP : P.HasMap (algebraMap _ (Localization.Away (aeval x q.derivative)) x) :=
      ⟨by simp_all [P], by simpa using IsLocalization.Away.algebraMap_isUnit _⟩
-- 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
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P_1 : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P_1) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P_1 Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
q : R[X]
hq : q.Monic
hqx : Eq.{u_3 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S)
hq'x : ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
P : StandardEtalePair R := { f := q, monic_f := hq, g := (derivative : (a : R[X]) → R[X]) q, cond := ⋯ }
hP :
  P.HasMap (S :=
    Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))
    ((algebraMap S
            (Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S)) :
          (a : S) → Localization.Away ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q)))
        x :
      Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))
f : AdjoinRoot P.f →ₐ[R] S := AdjoinRoot.liftAlgHom P.f (ofId R S) x hqx
⊢ IsLocalization.Away.{u_3, u_3} (R := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S)
    (Localization.Away (M := S)
      ((f : (a : AdjoinRoot P.f) → S) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f) : S))
have simp : IsLocalization.Away.{u_3, u_3} (R := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S)
  (Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))
Tactic: simp only [AdjoinRoot.liftAlgHom_mk, toRingHom_ofId, f, ← aeval_def, P]
-- 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
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P_1 : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P_1) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P_1 Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
q : R[X]
hq : q.Monic
hqx : Eq.{u_3 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S)
hq'x : ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
P : StandardEtalePair R := { f := q, monic_f := hq, g := (derivative : (a : R[X]) → R[X]) q, cond := ⋯ }
hP :
  P.HasMap (S :=
    Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))
    ((algebraMap S
            (Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S)) :
          (a : S) → Localization.Away ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q)))
        x :
      Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))
f : AdjoinRoot P.f →ₐ[R] S := AdjoinRoot.liftAlgHom P.f (ofId R S) x hqx
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have this₁ : IsLocalization.Away.{u_3, u_3} (R := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S)
  (Localization.Away (M := S)
    ((f : (a : AdjoinRoot P.f) → S) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f) : S))
Tactic: have : IsLocalization.Away (aeval x (derivative q)) (Localization.Away (f (.mk P.f P.g))) := by
      simp only [AdjoinRoot.liftAlgHom_mk, toRingHom_ofId, f, ← aeval_def, P]; infer_instance
-- 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
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P_1 : Ideal R := Ideal.under R Q
this_2 : Algebra.{u_1, u_3} (Localization.AtPrime P_1) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P_1 Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
q : R[X]
hq : q.Monic
hqx : Eq.{u_3 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S)
hq'x : ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
P : StandardEtalePair R := { f := q, monic_f := hq, g := (derivative : (a : R[X]) → R[X]) q, cond := ⋯ }
hP :
  P.HasMap (S :=
    Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))
    ((algebraMap S
            (Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S)) :
          (a : S) → Localization.Away ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q)))
        x :
      Localization.Away (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S))
f : AdjoinRoot P.f →ₐ[R] S := AdjoinRoot.liftAlgHom P.f (ofId R S) x hqx
this :
  IsLocalization.Away.{u_3, u_3} (R := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S)
    (Localization.Away (M := S)
      ((f : (a : AdjoinRoot P.f) → S) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f) : S))
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have refine : Function.Surjective.{u_1 + 1, u_3 + 1} (α := P.Ring) (β :=
  Localization.Away (M := S)
    ((f : (a : AdjoinRoot P.f) → S) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g : AdjoinRoot P.f) : S))
  (⇑(AlgHom.comp (Localization.awayMapₐ f ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g))
        (↑P.equivAwayAdjoinRoot :
          P.Ring →ₐ[R] Localization.Away ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g))) :
    (a : P.Ring) →
      Localization.Away ((f : (a : AdjoinRoot P.f) → S) ((AdjoinRoot.mk P.f : (a : R[X]) → AdjoinRoot P.f) P.g)))
Tactic: refine ⟨_, hq'x, .mk ((Localization.awayMapₐ f _).comp P.equivAwayAdjoinRoot.toAlgHom) ?_⟩
-- 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
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
have inr : ∃ (q : R[X]),
  q.Monic ∧
    Eq.{u_3 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S) ∧
      ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
Tactic: suffices ∃ q : R[X], q.Monic ∧ aeval x q = 0 ∧ aeval x q.derivative ∉ Q by
    -- Since if we have such a `q`, then `(R[X]/q)[1/q'] → S[1/q'(x)]` is the desired surjection.
    obtain ⟨q, hq, hqx, hq'x⟩ := this
    let P : StandardEtalePair R := ⟨q, hq, q.derivative, 1, 0, 1, by simp⟩
    have hP : P.HasMap (algebraMap _ (Localization.Away (aeval x q.derivative)) x) :=
      ⟨by simp_all [P], by simpa using IsLocalization.Away.algebraMap_isUnit _⟩
    let f : AdjoinRoot P.f →ₐ[R] S := AdjoinRoot.liftAlgHom _ (Algebra.ofId _ _) x hqx
    have : IsLocalization.Away (aeval x (derivative q)) (Localization.Away (f (.mk P.f P.g))) := by
      simp only [AdjoinRoot.liftAlgHom_mk, toRingHom_ofId, f, ← aeval_def, P]; infer_instance
    refine ⟨_, hq'x, .mk ((Localization.awayMapₐ f _).comp P.equivAwayAdjoinRoot.toAlgHom) ?_⟩
    simpa using IsLocalization.Away.mapₐ_surjective_of_surjective _
      (Ideal.Quotient.lift_surjective_of_surjective _ _ hx')
-- 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
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
⊢ ∃ (q : R[X]),
    q.Monic ∧
      Eq.{u_3 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S) ∧
        ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
have inr : ∀ (p : R[X]) (hpI : p ∈ I)
  (hp :
    Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
      (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)),
  ∃ (q : R[X]),
    q.Monic ∧
      Eq.{u_3 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S) ∧
        ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
Tactic: obtain ⟨p, hpI, hp⟩ := Ideal.exists_mem_span_singleton_map_residueField_eq P I
-- 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
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
p : R[X]
hpI : p ∈ I
hp :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
⊢ ∃ (q : R[X]),
    q.Monic ∧
      Eq.{u_3 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S) ∧
        ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
have hI' : Eq (α := Ideal P.ResidueField[X])
  (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
  (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
Tactic: have hI' : I.map (mapRingHom (algebraMap R P.ResidueField)) =
      RingHom.ker (aeval (1 ⊗ₜ x : P.Fiber S)).toRingHom :=
    exists_hasStandardEtaleSurjectionOn_of_exists_adjoin_singleton_eq_top_aux₁ P x hx
-- 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
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
p : R[X]
hpI : p ∈ I
hp :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
hI' :
  Eq (α := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
m : P.ResidueField[X] :=
  minpoly P.ResidueField (B := Q.ResidueField)
    ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x : Q.ResidueField)
⊢ ∃ (q : R[X]),
    q.Monic ∧
      Eq.{u_3 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S) ∧
        ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
have hm : Prime m
Tactic: have hm : Prime m := minpoly.prime (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
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
p : R[X]
hpI : p ∈ I
hp :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
hI' :
  Eq (α := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
m : P.ResidueField[X] :=
  minpoly P.ResidueField (B := Q.ResidueField)
    ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x : Q.ResidueField)
hm : Prime m
⊢ ∃ (q : R[X]),
    q.Monic ∧
      Eq.{u_3 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S) ∧
        ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
have hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
Tactic: have hmp₁ : m ∣ p.map (algebraMap _ _) := by simp_all [m, I, minpoly.dvd_iff]
-- 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
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
p : R[X]
hpI : p ∈ I
hp :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
hI' :
  Eq (α := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
m : P.ResidueField[X] :=
  minpoly P.ResidueField (B := Q.ResidueField)
    ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x : Q.ResidueField)
hm : Prime m
hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
⊢ ∃ (q : R[X]),
    q.Monic ∧
      Eq.{u_3 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S) ∧
        ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
have hmp₂ : ¬HPow.hPow (β := ℕ) m 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p
Tactic: have hmp₂ : ¬ m ^ 2 ∣ p.map (algebraMap _ _) :=
    exists_hasStandardEtaleSurjectionOn_of_exists_adjoin_singleton_eq_top_aux₂ x p (hp.trans hI') hx
-- 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
inst_3 : Module.Finite R S
Q : Ideal S
inst_4 : Q.IsPrime
inst_5 : IsUnramifiedAt R Q
h : Nontrivial S
this_1 : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra.{u_1, u_3} (Localization.AtPrime P) (Localization.AtPrime Q) :=
  Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : Eq (α := Subalgebra R S) R[x] ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (F := RingHom.{u_1, u_3} R[X] S) (AlgHom.toRingHom (aeval x))
hx' : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R[X]) (β := S) (⇑(aeval x) : (a : R[X]) → S)
p : R[X]
hpI : p ∈ I
hp :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
hI' :
  Eq (α := Ideal P.ResidueField[X])
    (Ideal.map (F := R[X] →+* P.ResidueField[X]) (mapRingHom (algebraMap R P.ResidueField)) I)
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S) (AlgHom.toRingHom (aeval (1 ⊗ₜ[R] x))))
m : P.ResidueField[X] :=
  minpoly P.ResidueField (B := Q.ResidueField)
    ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x : Q.ResidueField)
hm : Prime m
hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
hmp₂ : ¬HPow.hPow (β := ℕ) m 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p
q : R[X] := HPow.hPow (α := R[X]) (minpoly R x) (p.natDegree + 2) + p
⊢ ∃ (q : R[X]),
    q.Monic ∧
      Eq.{u_3 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S) ∧
        ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
have inr : q.Monic
Tactic: refine ⟨q, ?_, by simpa [q], ?_⟩