Module: Mathlib.RingTheory.Unramified.LocalStructure

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt R Q
h✝ : Nontrivial S
this✝ : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra (Localization.AtPrime P) (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : R[x] = ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
hx' : Function.Surjective ⇑(aeval x)
p : R[X]
hpI : p ∈ I
m : P.ResidueField[X] := minpoly P.ResidueField ((algebraMap S Q.ResidueField) x)
q : R[X] := minpoly R x ^ (p.natDegree + 2) + p
w : P.ResidueField[X]
hp : Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = RingHom.ker ↑(aeval (1 ⊗ₜ[R] x))
hI' : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = RingHom.ker ↑(aeval (1 ⊗ₜ[R] x))
hm : Prime m
hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
hmp₂ : ¬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:
#adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
      (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
      goal. It is not yet clear whether this is due to defeq abuse in Mathlib or a problem in
      the new canonicalizer; a minimization would help. The original proof was:
      `simp_all [q]; grind` -/

Goal state after:
case refine_1
R : Type u_1
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : Module.Finite R S
Q : Ideal S
inst✝¹ : Q.IsPrime
inst✝ : IsUnramifiedAt R Q
h✝ : Nontrivial S
this✝ : Nontrivial R
P : Ideal R := Ideal.under R Q
this : Algebra (Localization.AtPrime P) (Localization.AtPrime Q) := Localization.AtPrime.algebraOfLiesOver P Q
x : S
hx : R[x] = ⊤
hRx : IsIntegral R x
I : Ideal R[X] := RingHom.ker (aeval x).toRingHom
hx' : Function.Surjective ⇑(aeval x)
p : R[X]
hpI : p ∈ I
m : P.ResidueField[X] := minpoly P.ResidueField ((algebraMap S Q.ResidueField) x)
q : R[X] := minpoly R x ^ (p.natDegree + 2) + p
w : P.ResidueField[X]
hp : Ideal.span {Polynomial.map (algebraMap R P.ResidueField) p} = RingHom.ker ↑(aeval (1 ⊗ₜ[R] x))
hI' : Ideal.map (mapRingHom (algebraMap R P.ResidueField)) I = RingHom.ker ↑(aeval (1 ⊗ₜ[R] x))
hm : Prime m
hmp₁ : m ∣ Polynomial.map (algebraMap R P.ResidueField) p
hmp₂ : ¬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))