-- Module: Mathlib.RingTheory.DedekindDomain.Different
Goal:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst : CommRing A
inst_1 : Field K
inst_2 : CommRing B
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : Algebra A B
inst_7 : Algebra K L
inst_8 : Algebra A L
inst_9 : IsScalarTower A K L
inst_10 : IsScalarTower A B L
inst_11 : IsDomain A
inst_12 : IsFractionRing A K
inst_13 : FiniteDimensional K L
inst_14 : Algebra.IsSeparable K L
inst_15 : IsIntegralClosure B A L
inst_16 : IsIntegrallyClosed A
inst_17 : IsDedekindDomain B
inst_18 : IsTorsionFree A B
x : B
hx : Eq (α := Subalgebra K L) K[((algebraMap B L : (a : B) → L) x : L)] ⊤
hAx : IsIntegral A x
this : IsFractionRing B L
y : L
hne₁ :
  Ne.{u + 1} (α := L)
    (((aeval ((algebraMap B L : (a : B) → L) x) : K[X] →ₐ[K] L) : (a : K[X]) → L)
        ((derivative : (a : K[X]) → K[X]) (minpoly.{u_2, u} K (B := L) ((algebraMap B L : (a : B) → L) x : L)) : K[X]) :
      L)
    (0 : L)
rwa :
  ∀
    (hne₁ :
      Ne.{u + 1} (α := L)
        (((aeval ((algebraMap B L : (a : B) → L) x) : K[X] →ₐ[K] L) : (a : K[X]) → L)
            ((derivative : (a : K[X]) → K[X]) (Polynomial.map (algebraMap A K) (minpoly A x)) : K[X]) :
          L)
        (0 : L)),
    Ne.{u + 1} (α := L)
      ((algebraMap B L : (a : B) → L)
          ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B) :
        L)
      (0 : L)
rwa₁ :
  ∀
    (hne₁ :
      Ne.{u + 1} (α := L)
        (((aeval ((algebraMap B L : (a : B) → L) x) : K[X] →ₐ[K] L) : (a : K[X]) → L)
            (Polynomial.map (algebraMap A K) ((derivative : (a : A[X]) → A[X]) (minpoly A x))) :
          L)
        (0 : L)),
    Ne.{u + 1} (α := L)
      ((algebraMap B L : (a : B) → L)
          ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B) :
        L)
      (0 : L)
rwa₂ :
  ∀
    (hne₁ :
      Ne.{u + 1} (α := L)
        (((aeval ((algebraMap B L : (a : B) → L) x) : A[X] →ₐ[A] L) : (a : A[X]) → L)
            ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) :
          L)
        (0 : L)),
    Ne.{u + 1} (α := L)
      ((algebraMap B L : (a : B) → L)
          ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B) :
        L)
      (0 : L)
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀
    (hne₁ :
      Ne.{u + 1} (α := L)
        ((algebraMap B L : (a : B) → L)
            ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B) :
          L)
        (0 : L)),
    Ne.{u + 1} (α := L)
      ((algebraMap B L : (a : B) → L)
          ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B) :
        L)
      (0 : L)
⊢ Ne.{u + 1} (α := L)
    ((algebraMap B L : (a : B) → L)
        ((aeval x : (a : A[X]) → B) ((derivative : (a : A[X]) → A[X]) (minpoly A x) : A[X]) : B) :
      L)
    (0 : L)

Tactic:
rwa [minpoly.isIntegrallyClosed_eq_field_fractions K L hAx, derivative_map,
      aeval_map_algebraMap, aeval_algebraMap_apply] at hne₁

Premises used: Polynomial.aeval_map_algebraMap, minpoly.isIntegrallyClosed_eq_field_fractions, Polynomial.derivative_map, Polynomial.aeval_algebraMap_apply