awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
tfae_1_to_3 : ∀ (a : Algebra.IsSeparable K L), BilinForm.Nondegenerate (traceForm K L)
⊢ Ne (α := L →ₗ[K] K) (Algebra.trace K L) 0

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
tfae_1_to_3 : ∀ (a : Algebra.IsSeparable K L), BilinForm.Nondegenerate (traceForm K L)
⊢ ∀ (a : BilinForm.Nondegenerate (traceForm K L)), Ne (α := L →ₗ[K] K) (Algebra.trace K L) 0

Tactic:
3 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
tfae_1_to_3 : ∀ (a : Algebra.IsSeparable K L), BilinForm.Nondegenerate (traceForm K L)
H₁ : BilinForm.Nondegenerate (traceForm K L)
H₂ : Eq (α := L →ₗ[K] K) (Algebra.trace K L) 0
H :
  ∀ (x y : L),
    Eq.{u_4 + 1} (α := K) ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
      ((((0 : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
⊢ Eq (α := BilinForm K L) (traceForm K L) 0

Tactic:
ext
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
tfae_1_to_3 : ∀ (a : Algebra.IsSeparable K L), BilinForm.Nondegenerate (traceForm K L)
H₁ : BilinForm.Nondegenerate (traceForm K L)
H₂ : Eq (α := L →ₗ[K] K) (Algebra.trace K L) 0
x y : L
⊢ Eq.{u_4 + 1} (α := K) ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)
    ((((0 : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) y : K)

Tactic:
simp [H₂]
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
tfae_1_to_3 : ∀ (a : Algebra.IsSeparable K L), BilinForm.Nondegenerate (traceForm K L)
⊢ ∀ (a : BilinForm.Nondegenerate (traceForm K L)), Ne (α := L →ₗ[K] K) (Algebra.trace K L) 0

Tactic:
tfae_have 3 → 2 := fun H₁ H₂ ↦ H₁.ne_zero (by ext; simp [H₂])
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
tfae_1_to_3 : ∀ (a : Algebra.IsSeparable K L), BilinForm.Nondegenerate (traceForm K L)
tfae_3_to_2 : ∀ (a : BilinForm.Nondegenerate (traceForm K L)), Ne (α := L →ₗ[K] K) (Algebra.trace K L) 0
⊢ Ne (α := L →ₗ[K] K) (Algebra.trace K L) 0

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
tfae_1_to_3 : ∀ (a : Algebra.IsSeparable K L), BilinForm.Nondegenerate (traceForm K L)
tfae_3_to_2 : ∀ (a : BilinForm.Nondegenerate (traceForm K L)), Ne (α := L →ₗ[K] K) (Algebra.trace K L) 0
⊢ Algebra.IsSeparable K L

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
tfae_1_to_3 : ∀ (a : Algebra.IsSeparable K L), BilinForm.Nondegenerate (traceForm K L)
tfae_3_to_2 : ∀ (a : BilinForm.Nondegenerate (traceForm K L)), Ne (α := L →ₗ[K] K) (Algebra.trace K L) 0
⊢ ∀ (a : Ne (α := L →ₗ[K] K) (Algebra.trace K L) 0), Algebra.IsSeparable K L

Tactic:
2 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
tfae_1_to_3 : ∀ (a : Algebra.IsSeparable K L), BilinForm.Nondegenerate (traceForm K L)
tfae_3_to_2 : ∀ (a : BilinForm.Nondegenerate (traceForm K L)), Ne (α := L →ₗ[K] K) (Algebra.trace K L) 0
⊢ ∀ (a : Ne (α := L →ₗ[K] K) (Algebra.trace K L) 0), Algebra.IsSeparable K L

Tactic:
tfae_have 2 → 1 := not_imp_comm.mp Algebra.trace_eq_zero_of_not_isSeparable

Premises used: not_imp_comm, Algebra.trace_eq_zero_of_not_isSeparable, Iff.mp
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
tfae_1_to_3 : ∀ (a : Algebra.IsSeparable K L), BilinForm.Nondegenerate (traceForm K L)
tfae_3_to_2 : ∀ (a : BilinForm.Nondegenerate (traceForm K L)), Ne (α := L →ₗ[K] K) (Algebra.trace K L) 0
tfae_2_to_1 : ∀ (a : Ne (α := L →ₗ[K] K) (Algebra.trace K L) 0), Algebra.IsSeparable K L
⊢ [Algebra.IsSeparable K L, Ne (α := L →ₗ[K] K) (Algebra.trace K L) 0, BilinForm.Nondegenerate (traceForm K L)].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
⊢ Ne (α := L →ₗ[K] K) (trace K L) 0

Tactic:
((traceForm_nondegenerate_tfae K L).out 0 1).mp ‹_›

Premises used: traceForm_nondegenerate_tfae, List.TFAE.out, Iff.mp, OfNat.ofNat
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
rw : Eq (α := Submodule K K) (range (trace K L)) ⊤
⊢ Function.Surjective.{u_5 + 1, u_4 + 1} (α := L) (β := K) (⇑(trace K L) : (a : L) → K)

Tactic:
rw [← LinearMap.range_eq_top]

Premises used: LinearMap.range_eq_top
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
apply : ¬Eq (α := Ideal K) (range (trace K L)) ⊥
⊢ Eq (α := Submodule K K) (range (trace K L)) ⊤

Tactic:
apply (IsSimpleOrder.eq_bot_or_eq_top (α := Ideal K) _).resolve_left

Premises used: Or.resolve_left, IsSimpleOrder.eq_bot_or_eq_top
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
rw : ¬Eq (α := L →ₗ[K] K) (trace K L) 0
⊢ ¬Eq (α := Ideal K) (range (trace K L)) ⊥

Tactic:
rw [LinearMap.range_eq_bot]

Premises used: LinearMap.range_eq_bot
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
⊢ ¬Eq (α := L →ₗ[K] K) (trace K L) 0

Tactic:
Algebra.trace_ne_zero K L

Premises used: Algebra.trace_ne_zero
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
⊢ ¬Eq (α := L →ₗ[K] K) (trace K L) 0

Tactic:
exact Algebra.trace_ne_zero K L

Premises used: Algebra.trace_ne_zero
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
R : Type u_7
S : Type u_8
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
x : S
hx : IsNilpotent x
⊢ IsNilpotent.{u_7} (R := R) ((trace R S : (a : S) → R) x : R)

Tactic:
LinearMap.isNilpotent_trace_of_isNilpotent (hx.map (lmul R S))

Premises used: Algebra.lmul, IsNilpotent.map, LinearMap.isNilpotent_trace_of_isNilpotent
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
ι : Type w
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
inst_5 : Finite ι
inst_6 : DecidableEq ι
b : Basis ι K L
⊢ b.traceDual = BilinForm.dualBasis.{u_5, u_4, w} (V := L) (K := K) (ι := ι) (traceForm K L) ⋯ b

Tactic:
rfl

Premises used: Module.Basis.traceDual, rfl
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
ι : Type w
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
inst_5 : Finite ι
inst_6 : DecidableEq ι
b : Basis ι K L
x : L
i : ι
⊢ Eq.{u_4 + 1} (α := K) ((((b.traceDual.repr : (a : L) → ι →₀ K) x : ι →₀ K) : (a : ι) → K) i : K)
    ((((traceForm K L : (a : L) → L →ₗ[K] K) x : L →ₗ[K] K) : (a : L) → K) ((b : (a : ι) → L) i : L) : K)

Tactic:
(traceForm K L).dualBasis_repr_apply _ b _ i

Premises used: LinearMap.BilinForm.dualBasis_repr_apply
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
ι : Type w
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
inst_5 : Finite ι
inst_6 : DecidableEq ι
b : Basis ι K L
i j : ι
⊢ Eq.{u_4 + 1} (α := K)
    ((Algebra.trace K L : (a : L) → K)
        (HMul.hMul (α := L) (β := L) ((b.traceDual : (a : ι) → L) i : L) ((b : (a : ι) → L) j : L)) :
      K)
    (if j = i then 1 else 0 : K)

Tactic:
(traceForm K L).apply_dualBasis_left _ _ i j

Premises used: LinearMap.BilinForm.apply_dualBasis_left
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
ι : Type w
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
inst_5 : Finite ι
inst_6 : DecidableEq ι
b : Basis ι K L
i j : ι
⊢ Eq.{u_4 + 1} (α := K)
    ((Algebra.trace K L : (a : L) → K)
        (HMul.hMul (α := L) (β := L) ((b : (a : ι) → L) i : L) ((b.traceDual : (a : ι) → L) j : L)) :
      K)
    (if i = j then 1 else 0 : K)

Tactic:
(traceForm K L).apply_dualBasis_right _ (traceForm_isSymm K) _ i j

Premises used: Algebra.traceForm_isSymm, LinearMap.BilinForm.apply_dualBasis_right
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
ι : Type w
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
inst_5 : Finite ι
inst_6 : DecidableEq ι
b : Basis ι K L
⊢ b.traceDual.traceDual = b

Tactic:
(traceForm K L).dualBasis_dualBasis _ (traceForm_isSymm K) _

Premises used: Algebra.traceForm_isSymm, LinearMap.BilinForm.dualBasis_dualBasis, Module.Basis.traceDual
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
ι : Type w
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
inst_5 : Finite ι
inst_6 : DecidableEq ι
⊢ Function.Involutive (α := Basis ι K L) traceDual

Tactic:
(traceForm K L).dualBasis_involutive _ (traceForm_isSymm K)

Premises used: Algebra.traceForm_isSymm, LinearMap.BilinForm.dualBasis_involutive, Module.Basis.traceDual
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
ι : Type w
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
inst_5 : Finite ι
inst_6 : DecidableEq ι
⊢ Function.Injective (α := Basis ι K L) traceDual

Tactic:
(traceForm K L).dualBasis_injective _ (traceForm_isSymm K)

Premises used: LinearMap.BilinForm.dualBasis_injective, Algebra.traceForm_isSymm, Module.Basis.traceDual
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
ι : Type w
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
inst_5 : Finite ι
inst_6 : DecidableEq ι
b b' : Basis ι K L
⊢ b.traceDual = b'.traceDual ↔ b = b'

Tactic:
(traceDual_injective K L).eq_iff

Premises used: Function.Injective.eq_iff, Module.Basis.traceDual_injective
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
ι : Type w
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
inst_5 : Finite ι
inst_6 : DecidableEq ι
b : Basis ι K L
v : ι → L
⊢ (⇑b.traceDual : (a : ι) → L) = v ↔
    ∀ (i j : ι),
      Eq.{u_4 + 1} (α := K)
        ((((traceForm K L : (a : L) → L →ₗ[K] K) (v i) : L →ₗ[K] K) : (a : L) → K) ((b : (a : ι) → L) j : L) : K)
        (if j = i then 1 else 0 : K)

Tactic:
(traceForm K L).dualBasis_eq_iff (traceForm_nondegenerate K L) b v

Premises used: LinearMap.BilinForm.dualBasis_eq_iff, traceForm_nondegenerate
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
pb : PowerBasis K L
i : Fin pb.dim
revert :
  ∀ (i : Fin pb.dim),
    (pb.basis.traceDual : (a : Fin pb.dim) → L) i =
      HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑i : ℕ))
        ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)
⊢ (pb.basis.traceDual : (a : Fin pb.dim) → L) i =
    HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑i : ℕ))
      ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)

Tactic:
revert i
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
pb : PowerBasis K L
rw :
  ∀ (i j : Fin pb.dim),
    Eq.{u_4 + 1} (α := K)
      ((((traceForm K L : (a : L) → L →ₗ[K] K)
                (HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑i : ℕ))
                  ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)) :
              L →ₗ[K] K) :
            (a : L) → K)
          ((pb.basis : (a : Fin pb.dim) → L) j : L) :
        K)
      (if j = i then 1 else 0 : K)
⊢ ∀ (i : Fin pb.dim),
    (pb.basis.traceDual : (a : Fin pb.dim) → L) i =
      HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑i : ℕ))
        ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)

Tactic:
rw [← funext_iff, Basis.traceDual_eq_iff]

Premises used: funext_iff, Module.Basis.traceDual_eq_iff
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
a :
  Eq (α := AlgebraicClosure K)
    (((algebraMap K (AlgebraicClosure K) : K →+* AlgebraicClosure K) : (a : K) → AlgebraicClosure K)
        ((((traceForm K L : (a : L) → L →ₗ[K] K)
                (HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑i : ℕ))
                  ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)) :
              L →ₗ[K] K) :
            (a : L) → K)
          ((pb.basis : (a : Fin pb.dim) → L) j : L)) :
      AlgebraicClosure K)
    (((algebraMap K (AlgebraicClosure K) : K →+* AlgebraicClosure K) : (a : K) → AlgebraicClosure K)
        (if j = i then 1 else 0) :
      AlgebraicClosure K)
⊢ Eq.{u_4 + 1} (α := K)
    ((((traceForm K L : (a : L) → L →ₗ[K] K)
              (HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑i : ℕ))
                ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)) :
            L →ₗ[K] K) :
          (a : L) → K)
        ((pb.basis : (a : Fin pb.dim) → L) j : L) :
      K)
    (if j = i then 1 else 0 : K)

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

Premises used: Algebra.algebraMap, RingHom.injective, AlgebraicClosure
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
⊢ Eq.{u_4 + 1} (α := AlgebraicClosure K)
    ((fun (x : (AlgebraicClosure K)[X]) ↦ x.coeff (↑i : ℕ))
      (∑ σ : L →ₐ[K] AlgebraicClosure K,
        Polynomial.map (↑σ : L →+* AlgebraicClosure K)
          (HSMul.hSMul (β := L[X])
            (HDiv.hDiv (β := L) (pb.gen ^ (↑j : ℕ))
              ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L))
            (minpolyDiv K pb.gen))))
    ((fun (x : (AlgebraicClosure K)[X]) ↦ x.coeff (↑i : ℕ)) (HPow.hPow (α := (AlgebraicClosure K)[X]) X (↑j : ℕ)))

Tactic:
have := congr_arg (coeff · i) (sum_smul_minpolyDiv_eq_X_pow (AlgebraicClosure K)
    pb.adjoin_gen_eq_top (r := j) (pb.finrank.symm ▸ j.prop))
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
this :
  Eq.{u_4 + 1} (α := AlgebraicClosure K)
    ((fun (x : (AlgebraicClosure K)[X]) ↦ x.coeff (↑i : ℕ))
      (∑ σ : L →ₐ[K] AlgebraicClosure K,
        Polynomial.map (↑σ : L →+* AlgebraicClosure K)
          (HSMul.hSMul (β := L[X])
            (HDiv.hDiv (β := L) (pb.gen ^ (↑j : ℕ))
              ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L))
            (minpolyDiv K pb.gen))))
    ((fun (x : (AlgebraicClosure K)[X]) ↦ x.coeff (↑i : ℕ)) (HPow.hPow (α := (AlgebraicClosure K)[X]) X (↑j : ℕ)))
⊢ Eq.{u_4 + 1} (α := AlgebraicClosure K)
    (∑ x : L →ₐ[K] AlgebraicClosure K,
      HMul.hMul (β := AlgebraicClosure K)
        (HDiv.hDiv (β := AlgebraicClosure K)
          (HPow.hPow (α := AlgebraicClosure K) ((x : (a : L) → AlgebraicClosure K) pb.gen : AlgebraicClosure K)
            (↑j : ℕ))
          ((x : (a : L) → AlgebraicClosure K)
              ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
            AlgebraicClosure K))
        ((x : (a : L) → AlgebraicClosure K) (coeff (minpolyDiv K pb.gen) (↑i : ℕ)) : AlgebraicClosure K))
    (if j = i then 1 else 0)

Tactic:
simp only [Polynomial.map_smul, map_div₀, map_pow, RingHom.coe_coe, finsetSum_coeff, coeff_smul,
    coeff_map, smul_eq_mul, coeff_X_pow, ← Fin.ext_iff, @eq_comm _ i] at this

Premises used: Fin.ext_iff, Polynomial.coeff_map, RingHom.coe_coe, Polynomial.coeff_X_pow, Polynomial.finsetSum_coeff, map_pow, eq_comm, Polynomial.coeff_smul, map_div₀, Polynomial.map_smul, smul_eq_mul
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
this :
  Eq.{u_4 + 1} (α := AlgebraicClosure K)
    (∑ x : L →ₐ[K] AlgebraicClosure K,
      HMul.hMul (β := AlgebraicClosure K)
        (HDiv.hDiv (β := AlgebraicClosure K)
          (HPow.hPow (α := AlgebraicClosure K) ((x : (a : L) → AlgebraicClosure K) pb.gen : AlgebraicClosure K)
            (↑j : ℕ))
          ((x : (a : L) → AlgebraicClosure K)
              ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
            AlgebraicClosure K))
        ((x : (a : L) → AlgebraicClosure K) (coeff (minpolyDiv K pb.gen) (↑i : ℕ)) : AlgebraicClosure K))
    (if j = i then 1 else 0)
a :
  Eq (α := AlgebraicClosure K)
    (((algebraMap K (AlgebraicClosure K) : K →+* AlgebraicClosure K) : (a : K) → AlgebraicClosure K)
      ((((traceForm K L : (a : L) → L →ₗ[K] K)
              (HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑i : ℕ))
                ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)) :
            L →ₗ[K] K) :
          (a : L) → K)
        ((fun (i : Fin pb.dim) ↦ pb.gen ^ (↑i : ℕ)) j)))
    (((algebraMap K (AlgebraicClosure K) : K →+* AlgebraicClosure K) : (a : K) → AlgebraicClosure K)
      (if j = i then 1 else 0))
⊢ Eq (α := AlgebraicClosure K)
    (((algebraMap K (AlgebraicClosure K) : K →+* AlgebraicClosure K) : (a : K) → AlgebraicClosure K)
        ((((traceForm K L : (a : L) → L →ₗ[K] K)
                (HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑i : ℕ))
                  ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)) :
              L →ₗ[K] K) :
            (a : L) → K)
          ((pb.basis : (a : Fin pb.dim) → L) j : L)) :
      AlgebraicClosure K)
    (((algebraMap K (AlgebraicClosure K) : K →+* AlgebraicClosure K) : (a : K) → AlgebraicClosure K)
        (if j = i then 1 else 0) :
      AlgebraicClosure K)

Tactic:
rw [PowerBasis.coe_basis]

Premises used: PowerBasis.coe_basis
-- Module: Mathlib.RingTheory.Trace.Basic
Goal:
K : Type u_4
L : Type u_5
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : FiniteDimensional K L
inst_4 : Algebra.IsSeparable K L
pb : PowerBasis K L
i j : Fin pb.dim
this :
  Eq.{u_4 + 1} (α := AlgebraicClosure K)
    (∑ x : L →ₐ[K] AlgebraicClosure K,
      HMul.hMul (β := AlgebraicClosure K)
        (HDiv.hDiv (β := AlgebraicClosure K)
          (HPow.hPow (α := AlgebraicClosure K) ((x : (a : L) → AlgebraicClosure K) pb.gen : AlgebraicClosure K)
            (↑j : ℕ))
          ((x : (a : L) → AlgebraicClosure K)
              ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
            AlgebraicClosure K))
        ((x : (a : L) → AlgebraicClosure K) (coeff (minpolyDiv K pb.gen) (↑i : ℕ)) : AlgebraicClosure K))
    (if j = i then 1 else 0)
a :
  Eq (α := AlgebraicClosure K)
    (((algebraMap K (AlgebraicClosure K) : K →+* AlgebraicClosure K) : (a : K) → AlgebraicClosure K)
        ((Algebra.trace K L : (a : L) → K)
          (HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑i : ℕ))
              ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L) *
            pb.gen ^ (↑j : ℕ))) :
      AlgebraicClosure K)
    (if j = i then 1 else 0 : AlgebraicClosure K)
⊢ Eq (α := AlgebraicClosure K)
    (((algebraMap K (AlgebraicClosure K) : K →+* AlgebraicClosure K) : (a : K) → AlgebraicClosure K)
      ((((traceForm K L : (a : L) → L →ₗ[K] K)
              (HDiv.hDiv (β := L) (coeff (minpolyDiv K pb.gen) (↑i : ℕ))
                ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)) :
            L →ₗ[K] K) :
          (a : L) → K)
        ((fun (i : Fin pb.dim) ↦ pb.gen ^ (↑i : ℕ)) j)))
    (((algebraMap K (AlgebraicClosure K) : K →+* AlgebraicClosure K) : (a : K) → AlgebraicClosure K)
      (if j = i then 1 else 0))

Tactic:
simp only [traceForm_apply, MonoidWithZeroHom.map_ite_one_zero]

Premises used: Algebra.traceForm_apply, MonoidWithZeroHom.map_ite_one_zero