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 : 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 : p.natDegree < (HPow.hPow (α := R[X]) (minpoly R x) (p.natDegree + 2)).natDegree
⊢ q.Monic

Tactic:
refine ((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
-- 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
⊢ leadingCoeff (minpoly R x) ^ (p.natDegree + 2) ≠ 0

Tactic:
simp [minpoly.monic hRx]

Premises used: minpoly.monic
-- 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 : p.natDegree < p.natDegree + 2
⊢ p.natDegree < (HPow.hPow (α := R[X]) (minpoly R x) (p.natDegree + 2)).natDegree

Tactic:
grw [natDegree_pow' (by simp [minpoly.monic hRx]),
      ← Nat.le_mul_of_pos_right _ (minpoly.natDegree_pos hRx)]

Premises used: Nat.le_mul_of_pos_right, minpoly.natDegree_pos, Polynomial.natDegree_pow'
-- 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
⊢ p.natDegree < p.natDegree + 2

Tactic:
lia
-- 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
⊢ minpoly R x ∈ I

Tactic:
simp [I]
-- 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
obtain :
  ∀ (w : P.ResidueField[X])
    (hw :
      (mapRingHom (algebraMap R P.ResidueField) : (a : R[X]) → P.ResidueField[X]) (minpoly R x) =
        Polynomial.map (algebraMap R P.ResidueField) p * w),
    ∃ (w : P.ResidueField[X]),
      Polynomial.map (algebraMap R P.ResidueField) q = Polynomial.map (algebraMap R P.ResidueField) p * w ∧ ¬m ∣ w
⊢ ∃ (w : P.ResidueField[X]),
    Polynomial.map (algebraMap R P.ResidueField) q = Polynomial.map (algebraMap R P.ResidueField) p * w ∧ ¬m ∣ w

Tactic:
obtain ⟨w, hw⟩ := Ideal.mem_span_singleton.mp
      (hp.ge (Ideal.mem_map_of_mem _ (x := minpoly R x) (by simp [I])))

Premises used: Eq.ge, Ideal.mem_map_of_mem, Iff.mp, Ideal.mem_span_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
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
w : P.ResidueField[X]
hw :
  (mapRingHom (algebraMap R P.ResidueField) : (a : R[X]) → P.ResidueField[X]) (minpoly R x) =
    Polynomial.map (algebraMap R P.ResidueField) p * w
⊢ ∃ (w : P.ResidueField[X]),
    Polynomial.map (algebraMap R P.ResidueField) q = Polynomial.map (algebraMap R P.ResidueField) p * w ∧ ¬m ∣ w

Tactic:
⟨1 + w * (minpoly R x).map (algebraMap R P.ResidueField) ^ (p.natDegree + 1), ?_, ?_⟩

Premises used: HMul.hMul, Algebra.algebraMap, Ideal.ResidueField, minpoly, HPow.hPow, HAdd.hAdd, And.intro, Exists.intro, Polynomial.map, Polynomial.natDegree, OfNat.ofNat
-- 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
w : P.ResidueField[X]
hw :
  (mapRingHom (algebraMap R P.ResidueField) : (a : R[X]) → P.ResidueField[X]) (minpoly R x) =
    Polynomial.map (algebraMap R P.ResidueField) p * w
refine_1 :
  Polynomial.map (algebraMap R P.ResidueField) q =
    Polynomial.map (algebraMap R P.ResidueField) p *
      (1 +
        w *
          HPow.hPow (α := P.ResidueField[X]) (Polynomial.map (algebraMap R P.ResidueField) (minpoly R x))
            (p.natDegree + 1))
refine_2 :
  ¬m ∣
      1 +
        w *
          HPow.hPow (α := P.ResidueField[X]) (Polynomial.map (algebraMap R P.ResidueField) (minpoly R x))
            (p.natDegree + 1)
⊢ ∃ (w : P.ResidueField[X]),
    Polynomial.map (algebraMap R P.ResidueField) q = Polynomial.map (algebraMap R P.ResidueField) p * w ∧ ¬m ∣ w

Tactic:
refine ⟨1 + w * (minpoly R x).map (algebraMap R P.ResidueField) ^ (p.natDegree + 1), ?_, ?_⟩
-- 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
w : P.ResidueField[X]
hw :
  (mapRingHom (algebraMap R P.ResidueField) : (a : R[X]) → P.ResidueField[X]) (minpoly R x) =
    Polynomial.map (algebraMap R P.ResidueField) p * w
refine_1 :
  ∀
    (hp :
      Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
        (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S)
          (↑(aeval (1 ⊗ₜ[R] x)) : P.ResidueField[X] →+* P.ResidueField ⊗[R] S)))
    (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)
          (↑(aeval (1 ⊗ₜ[R] x)) : P.ResidueField[X] →+* P.ResidueField ⊗[R] S)))
    (hm : Prime m) (hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p)
    (hmp₂ : ¬HPow.hPow (β := ℕ) m 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p)
    (hw :
      Polynomial.map (algebraMap R P.ResidueField) (minpoly R x) = Polynomial.map (algebraMap R P.ResidueField) p * w),
    (Polynomial.map (algebraMap R P.ResidueField) p * w) ^ (p.natDegree + 2) +
        Polynomial.map (algebraMap R P.ResidueField) p =
      Polynomial.map (algebraMap R P.ResidueField) p *
        (1 + w * (Polynomial.map (algebraMap R P.ResidueField) p * w) ^ (p.natDegree + 1))
⊢ Polynomial.map (algebraMap R P.ResidueField) q =
    Polynomial.map (algebraMap R P.ResidueField) p *
      (1 +
        w *
          HPow.hPow (α := P.ResidueField[X]) (Polynomial.map (algebraMap R P.ResidueField) (minpoly R x))
            (p.natDegree + 1))

Tactic:
simp_all [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
m : P.ResidueField[X] :=
  minpoly P.ResidueField (B := Q.ResidueField)
    ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x : Q.ResidueField)
q : R[X] := HPow.hPow (α := R[X]) (minpoly R x) (p.natDegree + 2) + p
w : P.ResidueField[X]
hp :
  Eq (α := Ideal P.ResidueField[X]) (Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p})
    (RingHom.ker (F := P.ResidueField[X] →+* P.ResidueField ⊗[R] S)
      (↑(aeval (1 ⊗ₜ[R] x)) : P.ResidueField[X] →+* P.ResidueField ⊗[R] S))
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)
      (↑(aeval (1 ⊗ₜ[R] x)) : P.ResidueField[X] →+* P.ResidueField ⊗[R] S))
hm : Prime m
hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
hmp₂ : ¬HPow.hPow (β := ℕ) m 2 ∣ Polynomial.map (algebraMap R P.ResidueField) p
hw : Polynomial.map (algebraMap R P.ResidueField) (minpoly R x) = Polynomial.map (algebraMap R P.ResidueField) p * w
⊢ (Polynomial.map (algebraMap R P.ResidueField) p * w) ^ (p.natDegree + 2) +
      Polynomial.map (algebraMap R P.ResidueField) p =
    Polynomial.map (algebraMap R P.ResidueField) p *
      (1 + w * (Polynomial.map (algebraMap R P.ResidueField) p * w) ^ (p.natDegree + 1))

Tactic:
ring
-- 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
w : P.ResidueField[X]
hw :
  (mapRingHom (algebraMap R P.ResidueField) : (a : R[X]) → P.ResidueField[X]) (minpoly R x) =
    Polynomial.map (algebraMap R P.ResidueField) p * w
⊢ m ∣ Polynomial.map (algebraMap R P.ResidueField) (minpoly R x)

Tactic:
simp [m, minpoly.dvd_iff]

Premises used: 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
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
w : P.ResidueField[X]
hw :
  (mapRingHom (algebraMap R P.ResidueField) : (a : R[X]) → P.ResidueField[X]) (minpoly R x) =
    Polynomial.map (algebraMap R P.ResidueField) p * w
⊢ p.natDegree + 1 ≠ 0

Tactic:
simp