-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma traceForm_dualSubmodule_adjoin
    {x : L} (hx : Algebra.adjoin K {x} = ⊤) (hAx : IsIntegral A x) :
    (traceForm K L).dualSubmodule (Subalgebra.toSubmodule (Algebra.adjoin A {x})) =
      (aeval x (derivative <| minpoly K x) : L)⁻¹ •
        (Subalgebra.toSubmodule (Algebra.adjoin A {x}))

Proof state:
A : Type u_1
K : Type u_2
L : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsIntegrallyClosed A
x : L
hx : adjoin K {x} = ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L
pbgen : pb.gen = x
hpb :
  ⇑((traceForm K L).dualBasis ⋯ pb.basis) = fun x =>
    (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))
this : Subalgebra.toSubmodule (adjoin A {x}) = span A (Set.range ⇑pb.basis)
⊢ span A (Set.range fun x => (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))) =
    span A ((fun x_1 => ((aeval x) (derivative (minpoly K x)))⁻¹ • x_1) '' Set.range (minpolyDiv A x).coeff)

Tactic:
simp only [← Set.range_comp, smul_eq_mul, div_eq_inv_mul, pbgen,
  minpolyDiv_eq_of_isIntegrallyClosed K hAx]

Result:
A : Type u_1
K : Type u_2
L : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsIntegrallyClosed A
x : L
hx : adjoin K {x} = ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L
pbgen : pb.gen = x
hpb :
  ⇑((traceForm K L).dualBasis ⋯ pb.basis) = fun x =>
    (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))
this : Subalgebra.toSubmodule (adjoin A {x}) = span A (Set.range ⇑pb.basis)
⊢ span A (Set.range fun x_1 => ((aeval x) (derivative (minpoly K x)))⁻¹ * (minpolyDiv K x).coeff ↑x_1) =
    span A (Set.range ((fun a => ((aeval x) (derivative (minpoly K x)))⁻¹ * a) ∘ (minpolyDiv K x).coeff))

Proof state:
case e_s.h
A : Type u_1
K : Type u_2
L : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsIntegrallyClosed A
x : L
hx : adjoin K {x} = ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map (((adjoin K {x}).equivOfEq ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hpb :
  ⇑((traceForm K L).dualBasis ⋯ pb.basis) = fun x =>
    (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))
y : L
⊢ y ∈ ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range (minpoly A x).natDegree)) ↔ y ∈ Set.range ⇑pb.basis

Tactic:
have : natDegree (minpoly A x) = natDegree (minpoly K x) := by
  rw [minpoly.isIntegrallyClosed_eq_field_fractions' K hAx, (minpoly.monic hAx).natDegree_map]

Result:
case e_s.h
A : Type u_1
K : Type u_2
L : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsIntegrallyClosed A
x : L
hx : adjoin K {x} = ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L := (adjoin.powerBasis' hKx).map (((adjoin K {x}).equivOfEq ⊤ hx).trans Subalgebra.topEquiv)
pbgen : pb.gen = x
hpb :
  ⇑((traceForm K L).dualBasis ⋯ pb.basis) = fun x =>
    (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))
y : L
this : (minpoly A x).natDegree = (minpoly K x).natDegree
⊢ y ∈ ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range (minpoly A x).natDegree)) ↔ y ∈ Set.range ⇑pb.basis

Proof state:
A : Type u_1
K : Type u_2
L : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsIntegrallyClosed A
x : L
hx : adjoin K {x} = ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L
pbgen : pb.gen = x
hpb :
  ⇑((traceForm K L).dualBasis ⋯ pb.basis) = fun x =>
    (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))
this : Subalgebra.toSubmodule (adjoin A {x}) = span A (Set.range ⇑pb.basis)
⊢ (traceForm K L).dualSubmodule (Subalgebra.toSubmodule (adjoin A {x})) =
    ((aeval x) (derivative (minpoly K x)))⁻¹ • Subalgebra.toSubmodule (adjoin A {x})

Tactic:
conv_lhs => rw [this]

Result:
A : Type u_1
K : Type u_2
L : Type u
inst✝¹¹ : CommRing A
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra A L
inst✝⁵ : IsScalarTower A K L
inst✝⁴ : IsDomain A
inst✝³ : IsFractionRing A K
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsIntegrallyClosed A
x : L
hx : adjoin K {x} = ⊤
hAx : IsIntegral A x
hKx : IsIntegral K x
pb : PowerBasis K L
pbgen : pb.gen = x
hpb :
  ⇑((traceForm K L).dualBasis ⋯ pb.basis) = fun x =>
    (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))
this : Subalgebra.toSubmodule (adjoin A {x}) = span A (Set.range ⇑pb.basis)
⊢ (traceForm K L).dualSubmodule (span A (Set.range ⇑pb.basis)) =
    ((aeval x) (derivative (minpoly K x)))⁻¹ • Subalgebra.toSubmodule (adjoin A {x})