-- 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_1 : 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)
this_2 :
  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)
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)
this : IsIntegral.{u_1, u} A (A := L) ((algebraMap B L : (a : B) → L) x : L)
a :
  (∀ (z : B) (y_1 : L),
      Membership.mem (γ := Subalgebra A L) A[((algebraMap B L : (a : B) → L) x : L)] y_1 →
        Membership.mem.{u_2, u_2} (α := K) (γ := Submodule A K) 1
          ((Algebra.trace K L : (a : L) → K)
              (HMul.hMul (α := 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)
                (y * HMul.hMul (α := L) ((algebraMap B L : (a : B) → L) z : L) y_1)) :
            K)) ↔
    ∀ (a : B),
      Membership.mem.{u_2, u_2} (α := K) (γ := Subring K) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A K))
        ((Algebra.trace K L : (a : L) → K)
            (HMul.hMul (α := 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)
              (HMul.hMul (β := L) y ((algebraMap B L : (a : B) → L) a : L))) :
          K)
⊢ (∀ (z : B),
      Membership.mem (γ := Submodule A L)
        (LinearMap.BilinForm.dualSubmodule.{u_1, u_2, u} (R := A) (S := K) (M := L) (traceForm K L)
            ((Subalgebra.toSubmodule : (a : Subalgebra A L) → Submodule A L)
              A[((algebraMap B L : (a : B) → L) x : L)]) :
          Submodule A L)
        (HMul.hMul (α := 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)
          (HMul.hMul (β := L) y ((algebraMap B L : (a : B) → L) z : L)))) ↔
    ∀ (a : L),
      Membership.mem (γ := FractionalIdeal.{u_3, u} (R := B) B⁰ L) 1 a →
        Membership.mem.{u_2, u_2} (α := K) (γ := Subring K) (RingHom.range.{u_1, u_2} (R := A) (algebraMap A K))
          ((((traceForm K L : (a : L) → L →ₗ[K] K)
                    (HMul.hMul (α := 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)
                      y) :
                  L →ₗ[K] K) :
                (a : L) → K)
              a :
            K)

Tactic:
simp only [LinearMap.BilinForm.mem_dualSubmodule, traceForm_apply, Subalgebra.mem_toSubmodule,
    minpoly.isIntegrallyClosed_eq_field_fractions K L hAx,
    derivative_map, aeval_map_algebraMap, aeval_algebraMap_apply, mul_assoc,
    FractionalIdeal.mem_one_iff, forall_exists_index, forall_apply_eq_imp_iff]

Premises used: Polynomial.aeval_map_algebraMap, Algebra.traceForm_apply, Subalgebra.mem_toSubmodule, mul_assoc, FractionalIdeal.mem_one_iff, forall_exists_index, minpoly.isIntegrallyClosed_eq_field_fractions, LinearMap.BilinForm.mem_dualSubmodule, Polynomial.derivative_map, forall_apply_eq_imp_iff, Polynomial.aeval_algebraMap_apply