-- 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:
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
⊢ (∃ x_1 < (minpoly A x).natDegree, x ^ x_1 = y) ↔ ∃ y_1, x ^ ↑y_1 = y

Tactic:
simp only [PowerBasis.map_dim, adjoin.powerBasis'_dim, this]

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
⊢ (∃ x_1 < (minpoly K x).natDegree, x ^ x_1 = y) ↔ ∃ y_1, x ^ ↑y_1 = y

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 (span A (Set.range ⇑pb.basis)) =
    ((aeval x) (derivative (minpoly K x)))⁻¹ • Subalgebra.toSubmodule (adjoin A {x})

Tactic:
rw [← span_coeff_minpolyDiv hAx, LinearMap.BilinForm.dualSubmodule_span_of_basis,
  Submodule.smul_span, hpb]

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 => (minpolyDiv K pb.gen).coeff ↑x / (aeval pb.gen) (derivative (minpoly K pb.gen))) =
    span A (((aeval x) (derivative (minpoly K x)))⁻¹ • Set.range (minpolyDiv A x).coeff)

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 := (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))
⊢ (traceForm K L).dualSubmodule (Subalgebra.toSubmodule (adjoin A {x})) =
    ((aeval x) (derivative (minpoly K x)))⁻¹ • Subalgebra.toSubmodule (adjoin A {x})

Tactic:
have : (Subalgebra.toSubmodule (Algebra.adjoin A {x})) =
    Submodule.span A (Set.range pb.basis) := by
  rw [← span_range_natDegree_eq_adjoin (minpoly.monic hAx) (minpoly.aeval _ _)]
  congr; ext y
  have : natDegree (minpoly A x) = natDegree (minpoly K x) := by
    rw [minpoly.isIntegrallyClosed_eq_field_fractions' K hAx, (minpoly.monic hAx).natDegree_map]
  simp only [Finset.coe_image, Finset.coe_range, Set.mem_image, Set.mem_Iio, Set.mem_range,
    pb.basis_eq_pow, pbgen]
  simp only [PowerBasis.map_dim, adjoin.powerBasis'_dim, this]
  exact ⟨fun ⟨a, b, c⟩ ↦ ⟨⟨a, b⟩, c⟩, fun ⟨⟨a, b⟩, c⟩ ↦ ⟨a, b, c⟩⟩

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 := (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))
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})

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 := (adjoin.powerBasis' hKx).map (((adjoin K {x}).equivOfEq ⊤ hx).trans Subalgebra.topEquiv)
⊢ pb.gen = x

Tactic:
simp [pb]

Result:
no goals

Proof state:
case pos
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)
i : ℕ
hi : i < pb.dim
⊢ ((fun a => ((aeval x) (derivative (minpoly K x)))⁻¹ * a) ∘ (minpolyDiv K x).coeff) i ∈
    ↑(span A (Set.range fun x_1 => ((aeval x) (derivative (minpoly K x)))⁻¹ * (minpolyDiv K x).coeff ↑x_1))

Tactic:
exact Submodule.subset_span ⟨⟨i, hi⟩, rfl⟩

Result:
no goals