-- 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)
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]
h₁ : Polynomial.map (algebraMap R P.ResidueField) q = Polynomial.map (algebraMap R P.ResidueField) p * w
h₂ : ¬m ∣ w
hm' :
  Ne (α := P.ResidueField[X]) ((derivative : (a : P.ResidueField[X]) → P.ResidueField[X]) m : P.ResidueField[X])
    (0 : P.ResidueField[X])
this : ¬m ∣ (derivative : (a : P.ResidueField[X]) → P.ResidueField[X]) (Polynomial.map (algebraMap R P.ResidueField) q)
rwa :
  ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉
    RingHom.ker (F := S →+* Q.ResidueField) (algebraMap S Q.ResidueField)
rwa₁ :
  ¬Eq (α := Q.ResidueField)
      ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField)
          ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X])) :
        Q.ResidueField)
      (0 : Q.ResidueField)
rwa₂ :
  ¬Eq.{u_3 + 1} (α := Q.ResidueField)
      (((aeval ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x) :
              AlgHom.{u_1, u_1, u_3} R R[X] Q.ResidueField) :
            (a : R[X]) → Q.ResidueField)
          ((derivative : (a : R[X]) → R[X]) q) :
        Q.ResidueField)
      (0 : Q.ResidueField)
rwa₃ :
  ¬Eq.{u_3 + 1} (α := Q.ResidueField)
      (((aeval ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x) :
              AlgHom.{u_1, u_1, u_3} P.ResidueField P.ResidueField[X] Q.ResidueField) :
            (a : P.ResidueField[X]) → Q.ResidueField)
          (Polynomial.map (algebraMap R P.ResidueField) ((derivative : (a : R[X]) → R[X]) q)) :
        Q.ResidueField)
      (0 : Q.ResidueField)
⊢ ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) q : R[X]) : S) ∉ Q
have rwa₄ : ¬Eq.{u_3 + 1} (α := Q.ResidueField)
    (((aeval ((algebraMap S Q.ResidueField : (a : S) → Q.ResidueField) x) :
            AlgHom.{u_1, u_1, u_3} P.ResidueField P.ResidueField[X] Q.ResidueField) :
          (a : P.ResidueField[X]) → Q.ResidueField)
        ((derivative : (a : P.ResidueField[X]) → P.ResidueField[X]) (Polynomial.map (algebraMap R P.ResidueField) q)) :
      Q.ResidueField)
    (0 : Q.ResidueField)
Tactic: rwa [← Ideal.ker_algebraMap_residueField Q, RingHom.mem_ker, ← aeval_algebraMap_apply,
      ← aeval_map_algebraMap P.ResidueField, ← derivative_map, ← minpoly.dvd_iff]