-- 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
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))
⊢ ↑(Finset.image (fun x_1 => x ^ x_1) (Finset.range (minpoly A x).natDegree)) = Set.range ⇑pb.basis

Tactic:
ext y

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

Tactic:
let pb := (Algebra.adjoin.powerBasis' hKx).map
  ((Subalgebra.equivOfEq _ _ hx).trans (Subalgebra.topEquiv))

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

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

Tactic:
rintro _ ⟨i, rfl⟩

Result:
case a.intro
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 : ℕ
⊢ ((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))

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))
y : L
⊢ (minpoly A x).natDegree = (minpoly K x).natDegree

Tactic:
rw [minpoly.isIntegrallyClosed_eq_field_fractions' K hAx, (minpoly.monic hAx).natDegree_map]

Result:
no goals

Proof state:
case neg
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
⊢ 0 ∈ ↑(span A (Set.range fun x_1 => ((aeval x) (derivative (minpoly K x)))⁻¹ * (minpolyDiv K x).coeff ↑x_1))

Tactic:
exact zero_mem _

Result:
no goals