-- Mathlib/RingTheory/Trace/Basic.lean
/--
The dual basis of a powerbasis `{1, x, x²...}` under the trace form is `aᵢ / f'(x)`,
with `f` being the minimal polynomial of `x` and `f / (X - x) = ∑ aᵢxⁱ`.
-/
lemma traceForm_dualBasis_powerBasis_eq [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (pb : PowerBasis K L) (i) :
    (Algebra.traceForm K L).dualBasis (traceForm_nondegenerate K L) pb.basis i =
      (minpolyDiv K pb.gen).coeff i / aeval pb.gen (derivative <| minpoly K pb.gen)

Proof state:
case a
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
⊢ (if j = i then 1 else 0) =
    ((traceForm K L) ((minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen)))) (pb.basis j)

Tactic:
apply (algebraMap K (AlgebraicClosure K)).injective

Result:
case a.a
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
⊢ (algebraMap K (AlgebraicClosure K)) (if j = i then 1 else 0) =
    (algebraMap K (AlgebraicClosure K))
      (((traceForm K L) ((minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen)))) (pb.basis j))

Proof state:
case a.a
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
this :
  ∑ x : L →ₐ[K] AlgebraicClosure K,
      x pb.gen ^ ↑j / x ((aeval pb.gen) (derivative (minpoly K pb.gen))) * x ((minpolyDiv K pb.gen).coeff ↑i) =
    if j = i then 1 else 0
σ : L →ₐ[K] AlgebraicClosure K
a✝ : σ ∈ Finset.univ
⊢ σ pb.gen ^ ↑j / σ ((aeval pb.gen) (derivative (minpoly K pb.gen))) * σ ((minpolyDiv K pb.gen).coeff ↑i) =
    σ ((minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen)) * pb.gen ^ ↑j)

Tactic:
simp only [_root_.map_mul, map_div₀, map_pow]

Result:
case a.a
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
this :
  ∑ x : L →ₐ[K] AlgebraicClosure K,
      x pb.gen ^ ↑j / x ((aeval pb.gen) (derivative (minpoly K pb.gen))) * x ((minpolyDiv K pb.gen).coeff ↑i) =
    if j = i then 1 else 0
σ : L →ₐ[K] AlgebraicClosure K
a✝ : σ ∈ Finset.univ
⊢ σ pb.gen ^ ↑j / σ ((aeval pb.gen) (derivative (minpoly K pb.gen))) * σ ((minpolyDiv K pb.gen).coeff ↑i) =
    σ ((minpolyDiv K pb.gen).coeff ↑i) / σ ((aeval pb.gen) (derivative (minpoly K pb.gen))) * σ pb.gen ^ ↑j

Proof state:
case a.a
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
this :
  ∑ x : L →ₐ[K] AlgebraicClosure K,
      x pb.gen ^ ↑j / x ((aeval pb.gen) (derivative (minpoly K pb.gen))) * x ((minpolyDiv K pb.gen).coeff ↑i) =
    if j = i then 1 else 0
⊢ (algebraMap K (AlgebraicClosure K)) (if j = i then 1 else 0) =
    (algebraMap K (AlgebraicClosure K))
      (((traceForm K L) ((minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen)))) (pb.basis j))

Tactic:
rw [PowerBasis.coe_basis]

Result:
case a.a
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
this :
  ∑ x : L →ₐ[K] AlgebraicClosure K,
      x pb.gen ^ ↑j / x ((aeval pb.gen) (derivative (minpoly K pb.gen))) * x ((minpolyDiv K pb.gen).coeff ↑i) =
    if j = i then 1 else 0
⊢ (algebraMap K (AlgebraicClosure K)) (if j = i then 1 else 0) =
    (algebraMap K (AlgebraicClosure K))
      (((traceForm K L) ((minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen))))
        ((fun i => pb.gen ^ ↑i) j))

Proof state:
case a
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
pb : PowerBasis K L
i : Fin pb.dim
⊢ ∀ (i_1 : Fin pb.dim),
    (((traceForm K L).toDual ⋯) (((traceForm K L).dualBasis ⋯ pb.basis) i)) (pb.basis i_1) =
      (((traceForm K L).toDual ⋯) ((minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen))))
        (pb.basis i_1)

Tactic:
intro j

Result:
case a
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
⊢ (((traceForm K L).toDual ⋯) (((traceForm K L).dualBasis ⋯ pb.basis) i)) (pb.basis j) =
    (((traceForm K L).toDual ⋯) ((minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen))))
      (pb.basis j)

Proof state:
case a
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
pb : PowerBasis K L
i : Fin pb.dim
⊢ ((traceForm K L).toDual ⋯) (((traceForm K L).dualBasis ⋯ pb.basis) i) =
    ((traceForm K L).toDual ⋯) ((minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen)))

Tactic:
apply pb.basis.ext

Result:
case a
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
pb : PowerBasis K L
i : Fin pb.dim
⊢ ∀ (i_1 : Fin pb.dim),
    (((traceForm K L).toDual ⋯) (((traceForm K L).dualBasis ⋯ pb.basis) i)) (pb.basis i_1) =
      (((traceForm K L).toDual ⋯) ((minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen))))
        (pb.basis i_1)

Proof state:
case a.a
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
this :
  ∑ x : L →ₐ[K] AlgebraicClosure K,
      x pb.gen ^ ↑j / x ((aeval pb.gen) (derivative (minpoly K pb.gen))) * x ((minpolyDiv K pb.gen).coeff ↑i) =
    if j = i then 1 else 0
⊢ (if j = i then 1 else 0) =
    (algebraMap K (AlgebraicClosure K))
      ((Algebra.trace K L)
        ((minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen)) * pb.gen ^ ↑j))

Tactic:
rw [← this, trace_eq_sum_embeddings (E := AlgebraicClosure K)]

Result:
case a.a
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
this :
  ∑ x : L →ₐ[K] AlgebraicClosure K,
      x pb.gen ^ ↑j / x ((aeval pb.gen) (derivative (minpoly K pb.gen))) * x ((minpolyDiv K pb.gen).coeff ↑i) =
    if j = i then 1 else 0
⊢ ∑ x : L →ₐ[K] AlgebraicClosure K,
      x pb.gen ^ ↑j / x ((aeval pb.gen) (derivative (minpoly K pb.gen))) * x ((minpolyDiv K pb.gen).coeff ↑i) =
    ∑ σ : L →ₐ[K] AlgebraicClosure K,
      σ ((minpolyDiv K pb.gen).coeff ↑i / (aeval pb.gen) (derivative (minpoly K pb.gen)) * pb.gen ^ ↑j)