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
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))

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
-- 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
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

Tactic:
⟨_, hq'x, .mk ((Localization.awayMapₐ f _).comp P.equivAwayAdjoinRoot.toAlgHom) ?_⟩

Premises used: AlgEquiv.toAlgHom, StandardEtalePair.equivAwayAdjoinRoot, And.intro, Exists.intro, HasStandardEtaleSurjectionOn.mk, AlgHom.comp, Localization.awayMapₐ
-- 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
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))
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)))
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

Tactic:
refine ⟨_, hq'x, .mk ((Localization.awayMapₐ f _).comp P.equivAwayAdjoinRoot.toAlgHom) ?_⟩
-- 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
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))
⊢ 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:
simpa using IsLocalization.Away.mapₐ_surjective_of_surjective _
      (Ideal.Quotient.lift_surjective_of_surjective _ _ hx')

Premises used: IsLocalization.Away.mapₐ_surjective_of_surjective
-- 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
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)
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
⊢ ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f

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')
-- 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
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)
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
⊢ ∃ (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

Premises used: Ideal.exists_mem_span_singleton_map_residueField_eq
-- 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
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)
⊢ 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
-- 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
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)
⊢ Prime m

Tactic:
have hm : Prime m := minpoly.prime (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
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
⊢ m ∣ Polynomial.map (algebraMap R P.ResidueField) p

Tactic:
have hmp₁ : m ∣ p.map (algebraMap _ _) := by simp_all [m, I, minpoly.dvd_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
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
⊢ ¬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
-- 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
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
⊢ Eq.{u_3 + 1} (α := S) ((aeval x : (a : R[X]) → S) q : S) (0 : S)

Tactic:
simpa [q]
-- 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
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
inr : q.Monic
inr₁ : ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
⊢ ∃ (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:
refine ⟨q, ?_, by simpa [q], ?_⟩
-- 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
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.Monic

Tactic:
((minpoly.monic hRx).pow _).add_of_left (degree_lt_degree ?_)

Premises used: Polynomial.Monic.add_of_left, minpoly.monic, Polynomial.degree_lt_degree, Polynomial.Monic.pow