awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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 (α := Ideal K) (range (trace K L)) ⊥
have rw : ¬Eq (α := L →ₗ[K] K) (trace K L) 0
Tactic: rw [LinearMap.range_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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
⊢ (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)
have 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)
Tactic: revert i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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),
    (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)
have 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)
Tactic: rw [← funext_iff, Basis.traceDual_eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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} (α := 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)
have 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)
Tactic: apply (algebraMap K (AlgebraicClosure K)).injective
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (hypothesis)
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 (α := 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)
have 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 : ℕ)))
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))
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (hypothesis)
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 (α := 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)
have 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)
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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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)
⊢ 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)
have 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))
Tactic: rw [PowerBasis.coe_basis]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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)
⊢ 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))
have 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)
Tactic: simp only [traceForm_apply, MonoidWithZeroHom.map_ite_one_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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)
⊢ 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)
have a : Eq.{u_4 + 1} (α := AlgebraicClosure K)
  (∑ σ : L →ₐ[K] AlgebraicClosure K,
    (σ : (a : L) → AlgebraicClosure 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 : ℕ)))
  (∑ 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))
Tactic: rw [← this, trace_eq_sum_embeddings (E := AlgebraicClosure K)]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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)
⊢ Eq.{u_4 + 1} (α := AlgebraicClosure K)
    (∑ σ : L →ₐ[K] AlgebraicClosure K,
      (σ : (a : L) → AlgebraicClosure 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 : ℕ)))
    (∑ 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))
have a : ∀ (x : L →ₐ[K] AlgebraicClosure K),
  Membership.mem (γ := Finset (L →ₐ[K] AlgebraicClosure K)) Finset.univ x →
    (x : (a : L) → AlgebraicClosure 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 : ℕ)) =
      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)
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
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)
σ : L →ₐ[K] AlgebraicClosure K
h : Membership.mem (γ := Finset (L →ₐ[K] AlgebraicClosure K)) Finset.univ σ
⊢ (σ : (a : L) → AlgebraicClosure 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 : ℕ)) =
    HMul.hMul (β := AlgebraicClosure K)
      (HDiv.hDiv (β := AlgebraicClosure K)
        (HPow.hPow (α := AlgebraicClosure K) ((σ : (a : L) → AlgebraicClosure K) pb.gen : AlgebraicClosure K) (↑j : ℕ))
        ((σ : (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))
      ((σ : (a : L) → AlgebraicClosure K) (coeff (minpolyDiv K pb.gen) (↑i : ℕ)) : AlgebraicClosure K)
have a : HDiv.hDiv (α := AlgebraicClosure K) (β := AlgebraicClosure K)
      ((σ : (a : L) → AlgebraicClosure K) (coeff (minpolyDiv K pb.gen) (↑i : ℕ)) : AlgebraicClosure K)
      ((σ : (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) *
    HPow.hPow (α := AlgebraicClosure K) ((σ : (a : L) → AlgebraicClosure K) pb.gen : AlgebraicClosure K) (↑j : ℕ) =
  HMul.hMul (β := AlgebraicClosure K)
    (HDiv.hDiv (β := AlgebraicClosure K)
      (HPow.hPow (α := AlgebraicClosure K) ((σ : (a : L) → AlgebraicClosure K) pb.gen : AlgebraicClosure K) (↑j : ℕ))
      ((σ : (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))
    ((σ : (a : L) → AlgebraicClosure K) (coeff (minpolyDiv K pb.gen) (↑i : ℕ)) : AlgebraicClosure K)
Tactic: simp only [map_mul, map_div₀, map_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : ¬∃ (s : Finset S), Nonempty (Basis (↥s) R S)
⊢ Eq (α := S →ₗ[R] R) (trace R S) 0
have h₁ : ∀ (s : S), Eq.{u_1 + 1} (α := R) ((trace R S : (a : S) → R) s : R) ((0 : (a : S) → R) s : R)
Tactic: ext s
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type w
inst_3 : Fintype ι
inst_4 : DecidableEq ι
b : Basis ι R S
s : S
⊢ Eq.{u_1 + 1} (α := R) ((trace R S : (a : S) → R) s : R)
    (Matrix.trace.{w, u_1} (n := ι) ((leftMulMatrix b : (a : S) → Matrix ι ι R) s) : R)
have rw : Eq.{u_1 + 1} (α := R)
  (Matrix.trace.{w, u_1} (n := ι) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix ι ι R) ((lmul R S : (a : S) → End R S) s)))
  (Matrix.trace.{w, u_1} (n := ι) ((toMatrix b b : (a : S →ₗ[R] S) → Matrix ι ι R) (mulLeft R s)))
Tactic: rw [trace_apply, LinearMap.trace_eq_matrix_trace _ b, ← toMatrix_lmul_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type w
inst_3 : Fintype ι
b : Basis ι R S
x : R
⊢ (trace R S : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = Fintype.card ι • x
have haveI : ∀ (this : DecidableEq ι), (trace R S : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = Fintype.card ι • x
Tactic: haveI := Classical.decEq ι
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type w
inst_3 : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
⊢ (trace R S : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = Fintype.card ι • x
have rw : ∑ i : ι,
    Matrix.diag
      ((toMatrix b b : (a : S →ₗ[R] S) → Matrix ι ι R)
        ((lmul R S : (a : S) → End R S) ((algebraMap R S : (a : R) → S) x : S)))
      i =
  Fintype.card ι • x
Tactic: rw [trace_apply, LinearMap.trace_eq_matrix_trace R b, Matrix.trace]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
ι : Type w
inst_3 : Fintype ι
b : Basis ι R S
x : R
this : DecidableEq ι
⊢ ∑ i : ι,
      Matrix.diag
        ((toMatrix b b : (a : S →ₗ[R] S) → Matrix ι ι R)
          ((lmul R S : (a : S) → End R S) ((algebraMap R S : (a : R) → S) x : S)))
        i =
    Fintype.card ι • x
have h : ∀ (x_1 : ι),
  Membership.mem (γ := Finset ι) Finset.univ x_1 →
    Matrix.diag
        ((toMatrix b b : (a : S →ₗ[R] S) → Matrix ι ι R)
          ((lmul R S : (a : S) → End R S) ((algebraMap R S : (a : R) → S) x : S)))
        x_1 =
      x
Tactic: convert! Finset.sum_const x
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
Goal:
R : Type u_1
inst : CommRing R
⊢ Eq (α := R →ₗ[R] R) (trace R R) LinearMap.id
have h : Eq (α := R) ((trace R R : (a : R) → R) 1 : R) ((LinearMap.id : (a : R) → R) 1 : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : StrongRankCondition R
inst_4 : Free R S
x : R
⊢ (trace R S : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = finrank R S • x
have pos : ∀ (H : ∃ (s : Finset S), Nonempty (Basis (↥s) R S)),
  (trace R S : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = finrank R S • x
Tactic: by_cases H : ∃ s : Finset S, Nonempty (Basis s R S)
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : StrongRankCondition R
inst_4 : Free R S
x : R
pos :
  ∀ (H : ∃ (s : Finset S), Nonempty (Basis (↥s) R S)),
    (trace R S : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = finrank R S • x
⊢ (trace R S : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = finrank R S • x
have neg : ∀ (H : ¬∃ (s : Finset S), Nonempty (Basis (↥s) R S)),
  (trace R S : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = finrank R S • x
Tactic: by_cases H : ∃ s : Finset S, Nonempty (Basis s R S)
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Defs (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : StrongRankCondition R
inst_4 : Free R S
x : R
H : ∃ (s : Finset S), Nonempty (Basis (↥s) R S)
⊢ (trace R S : (a : S) → R) ((algebraMap R S : (a : R) → S) x : S) = finrank R S • x
have pos : Fintype.card.{u_2} ↥(H.choose (p := fun (s : Finset S) ↦ Nonempty (Basis (↥s) R S))) • x = finrank R S • x
Tactic: rw [trace_algebraMap_of_basis H.choose_spec.some, finrank_eq_card_basis H.choose_spec.some]