awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : PowerBasis R S
i j : Fin h.dim
a :
  Eq (α := R)
    ((trace R S : (a : S) → R)
        (HMul.hMul (α := S) (β := S) ((h.basis : (a : Fin h.dim) → S) i : S) ((h.basis : (a : Fin h.dim) → S) j : S)) :
      R)
    ((of : (a : Fin h.dim → Fin h.dim → R) → Matrix (Fin h.dim) (Fin h.dim) R)
        (fun (i j : Fin h.dim) ↦ (trace R S : (a : S) → R) (h.gen ^ ((↑i : ℕ) + (↑j : ℕ)))) i j :
      R)
a₁ :
  Eq.{u_1 + 1} (α := R)
    ((trace R S : (a : S) → R)
        (HMul.hMul (α := S) (β := S) ((h.basis : (a : Fin h.dim) → S) i : S) ((h.basis : (a : Fin h.dim) → S) j : S)) :
      R)
    ((trace R S : (a : S) → R) (h.gen ^ ((↑i : ℕ) + (↑j : ℕ))) : R)
a₂ :
  Eq.{u_1 + 1} (α := R)
    ((trace R S : (a : S) → R)
        (HMul.hMul (α := S) (β := S) ((h.basis : (a : Fin h.dim) → S) i : S) ((h.basis : (a : Fin h.dim) → S) j : S)) :
      R)
    ((trace R S : (a : S) → R) (h.gen ^ (↑i : ℕ) * h.gen ^ (↑j : ℕ)) : R)
⊢ Eq (α := R)
    ((LinearMap.BilinForm.toMatrix h.basis : (a : BilinForm R S) → Matrix (Fin h.dim) (Fin h.dim) R) (traceForm R S) i
        j :
      R)
    ((of : (a : Fin h.dim → Fin h.dim → R) → Matrix (Fin h.dim) (Fin h.dim) R)
        (fun (i j : Fin h.dim) ↦ (trace R S : (a : S) → R) (h.gen ^ ((↑i : ℕ) + (↑j : ℕ)))) i j :
      R)
have a₃ : Eq.{u_1 + 1} (α := R)
  ((trace R S : (a : S) → R) (HMul.hMul (β := S) (h.gen ^ (↑i : ℕ)) ((h.basis : (a : Fin h.dim) → S) j : S)) : R)
  ((trace R S : (a : S) → R) (h.gen ^ (↑i : ℕ) * h.gen ^ (↑j : ℕ)) : R)
Tactic: rw [traceForm_toMatrix, of_apply, pow_add, h.basis_eq_pow, h.basis_eq_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
h : PowerBasis R S
i j : Fin h.dim
a :
  Eq (α := R)
    ((trace R S : (a : S) → R)
        (HMul.hMul (α := S) (β := S) ((h.basis : (a : Fin h.dim) → S) i : S) ((h.basis : (a : Fin h.dim) → S) j : S)) :
      R)
    ((of : (a : Fin h.dim → Fin h.dim → R) → Matrix (Fin h.dim) (Fin h.dim) R)
        (fun (i j : Fin h.dim) ↦ (trace R S : (a : S) → R) (h.gen ^ ((↑i : ℕ) + (↑j : ℕ)))) i j :
      R)
a₁ :
  Eq.{u_1 + 1} (α := R)
    ((trace R S : (a : S) → R)
        (HMul.hMul (α := S) (β := S) ((h.basis : (a : Fin h.dim) → S) i : S) ((h.basis : (a : Fin h.dim) → S) j : S)) :
      R)
    ((trace R S : (a : S) → R) (h.gen ^ ((↑i : ℕ) + (↑j : ℕ))) : R)
a₂ :
  Eq.{u_1 + 1} (α := R)
    ((trace R S : (a : S) → R)
        (HMul.hMul (α := S) (β := S) ((h.basis : (a : Fin h.dim) → S) i : S) ((h.basis : (a : Fin h.dim) → S) j : S)) :
      R)
    ((trace R S : (a : S) → R) (h.gen ^ (↑i : ℕ) * h.gen ^ (↑j : ℕ)) : R)
a₃ :
  Eq.{u_1 + 1} (α := R)
    ((trace R S : (a : S) → R) (HMul.hMul (β := S) (h.gen ^ (↑i : ℕ)) ((h.basis : (a : Fin h.dim) → S) j : S)) : R)
    ((trace R S : (a : S) → R) (h.gen ^ (↑i : ℕ) * h.gen ^ (↑j : ℕ)) : R)
⊢ Eq (α := R)
    ((LinearMap.BilinForm.toMatrix h.basis : (a : BilinForm R S) → Matrix (Fin h.dim) (Fin h.dim) R) (traceForm R S) i
        j :
      R)
    ((of : (a : Fin h.dim → Fin h.dim → R) → Matrix (Fin h.dim) (Fin h.dim) R)
        (fun (i j : Fin h.dim) ↦ (trace R S : (a : S) → R) (h.gen ^ ((↑i : ℕ) + (↑j : ℕ)))) i j :
      R)
have a₄ : Eq.{u_1 + 1} (α := R) ((trace R S : (a : S) → R) (h.gen ^ (↑i : ℕ) * h.gen ^ (↑j : ℕ)) : R)
  ((trace R S : (a : S) → R) (h.gen ^ (↑i : ℕ) * h.gen ^ (↑j : ℕ)) : R)
Tactic: rw [traceForm_toMatrix, of_apply, pow_add, h.basis_eq_pow, h.basis_eq_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (hypothesis)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : Field K
inst_2 : Algebra K S
inst_3 : Nontrivial S
pb : PowerBasis K S
⊢ (Algebra.trace K S : (a : S) → K) pb.gen = -nextCoeff (minpoly K pb.gen)
have d_pos : 0 < pb.dim
Tactic: have d_pos : 0 < pb.dim := PowerBasis.dim_pos pb
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (hypothesis)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : Field K
inst_2 : Algebra K S
inst_3 : Nontrivial S
pb : PowerBasis K S
d_pos : 0 < pb.dim
⊢ (Algebra.trace K S : (a : S) → K) pb.gen = -nextCoeff (minpoly K pb.gen)
have d_pos' : 0 < natDegree (minpoly K pb.gen)
Tactic: have d_pos' : 0 < (minpoly K pb.gen).natDegree := by simpa
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (hypothesis)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : Field K
inst_2 : Algebra K S
inst_3 : Nontrivial S
pb : PowerBasis K S
d_pos : 0 < pb.dim
d_pos' : 0 < natDegree (minpoly K pb.gen)
⊢ (Algebra.trace K S : (a : S) → K) pb.gen = -nextCoeff (minpoly K pb.gen)
have this : Nonempty (Fin pb.dim)
Tactic: haveI : Nonempty (Fin pb.dim) := ⟨⟨0, d_pos⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : Field K
inst_2 : Algebra K S
inst_3 : Nontrivial S
pb : PowerBasis K S
d_pos : 0 < pb.dim
d_pos' : 0 < natDegree (minpoly K pb.gen)
this : Nonempty (Fin pb.dim)
⊢ (Algebra.trace K S : (a : S) → K) pb.gen = -nextCoeff (minpoly K pb.gen)
have rw : Matrix.trace (n := Fin pb.dim)
    (((leftMulMatrix pb.basis : S →ₐ[K] Matrix (Fin pb.dim) (Fin pb.dim) K) :
        (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) K)
      pb.gen) =
  -nextCoeff (minpoly K pb.gen)
Tactic: rw [trace_eq_matrix_trace pb.basis, trace_eq_neg_charpoly_coeff, charpoly_leftMulMatrix, ←
    pb.natDegree_minpoly, Fintype.card_fin, ← nextCoeff_of_natDegree_pos d_pos']
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : Field K
inst_2 : Algebra K S
inst_3 : Nontrivial S
pb : PowerBasis K S
d_pos : 0 < pb.dim
d_pos' : 0 < natDegree (minpoly K pb.gen)
this : Nonempty (Fin pb.dim)
rw :
  Matrix.trace (n := Fin pb.dim)
      (((leftMulMatrix pb.basis : S →ₐ[K] Matrix (Fin pb.dim) (Fin pb.dim) K) :
          (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) K)
        pb.gen) =
    -nextCoeff (minpoly K pb.gen)
⊢ (Algebra.trace K S : (a : S) → K) pb.gen = -nextCoeff (minpoly K pb.gen)
have rw₁ : -coeff
      (charpoly (n := Fin pb.dim)
        (((leftMulMatrix pb.basis : S →ₐ[K] Matrix (Fin pb.dim) (Fin pb.dim) K) :
            (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) K)
          pb.gen))
      (Fintype.card (Fin pb.dim) - 1) =
  -nextCoeff (minpoly K pb.gen)
Tactic: rw [trace_eq_matrix_trace pb.basis, trace_eq_neg_charpoly_coeff, charpoly_leftMulMatrix, ←
    pb.natDegree_minpoly, Fintype.card_fin, ← nextCoeff_of_natDegree_pos d_pos']
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : Field K
inst_2 : Algebra K S
inst_3 : Nontrivial S
pb : PowerBasis K S
d_pos : 0 < pb.dim
d_pos' : 0 < natDegree (minpoly K pb.gen)
this : Nonempty (Fin pb.dim)
rw :
  Matrix.trace (n := Fin pb.dim)
      (((leftMulMatrix pb.basis : S →ₐ[K] Matrix (Fin pb.dim) (Fin pb.dim) K) :
          (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) K)
        pb.gen) =
    -nextCoeff (minpoly K pb.gen)
rw₁ :
  -coeff
        (charpoly (n := Fin pb.dim)
          (((leftMulMatrix pb.basis : S →ₐ[K] Matrix (Fin pb.dim) (Fin pb.dim) K) :
              (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) K)
            pb.gen))
        (Fintype.card (Fin pb.dim) - 1) =
    -nextCoeff (minpoly K pb.gen)
⊢ (Algebra.trace K S : (a : S) → K) pb.gen = -nextCoeff (minpoly K pb.gen)
have rw₂ : -coeff (minpoly K pb.gen) (Fintype.card (Fin pb.dim) - 1) = -nextCoeff (minpoly K pb.gen)
Tactic: rw [trace_eq_matrix_trace pb.basis, trace_eq_neg_charpoly_coeff, charpoly_leftMulMatrix, ←
    pb.natDegree_minpoly, Fintype.card_fin, ← nextCoeff_of_natDegree_pos d_pos']
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : Field K
inst_2 : Algebra K S
inst_3 : Nontrivial S
pb : PowerBasis K S
d_pos : 0 < pb.dim
d_pos' : 0 < natDegree (minpoly K pb.gen)
this : Nonempty (Fin pb.dim)
rw :
  Matrix.trace (n := Fin pb.dim)
      (((leftMulMatrix pb.basis : S →ₐ[K] Matrix (Fin pb.dim) (Fin pb.dim) K) :
          (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) K)
        pb.gen) =
    -nextCoeff (minpoly K pb.gen)
rw₁ :
  -coeff
        (charpoly (n := Fin pb.dim)
          (((leftMulMatrix pb.basis : S →ₐ[K] Matrix (Fin pb.dim) (Fin pb.dim) K) :
              (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) K)
            pb.gen))
        (Fintype.card (Fin pb.dim) - 1) =
    -nextCoeff (minpoly K pb.gen)
rw₂ : -coeff (minpoly K pb.gen) (Fintype.card (Fin pb.dim) - 1) = -nextCoeff (minpoly K pb.gen)
⊢ (Algebra.trace K S : (a : S) → K) pb.gen = -nextCoeff (minpoly K pb.gen)
have rw₃ : -coeff (minpoly K pb.gen) (Fintype.card (Fin (natDegree (minpoly K pb.gen))) - 1) = -nextCoeff (minpoly K pb.gen)
Tactic: rw [trace_eq_matrix_trace pb.basis, trace_eq_neg_charpoly_coeff, charpoly_leftMulMatrix, ←
    pb.natDegree_minpoly, Fintype.card_fin, ← nextCoeff_of_natDegree_pos d_pos']
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : Field K
inst_2 : Algebra K S
inst_3 : Nontrivial S
pb : PowerBasis K S
d_pos : 0 < pb.dim
d_pos' : 0 < natDegree (minpoly K pb.gen)
this : Nonempty (Fin pb.dim)
rw :
  Matrix.trace (n := Fin pb.dim)
      (((leftMulMatrix pb.basis : S →ₐ[K] Matrix (Fin pb.dim) (Fin pb.dim) K) :
          (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) K)
        pb.gen) =
    -nextCoeff (minpoly K pb.gen)
rw₁ :
  -coeff
        (charpoly (n := Fin pb.dim)
          (((leftMulMatrix pb.basis : S →ₐ[K] Matrix (Fin pb.dim) (Fin pb.dim) K) :
              (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) K)
            pb.gen))
        (Fintype.card (Fin pb.dim) - 1) =
    -nextCoeff (minpoly K pb.gen)
rw₂ : -coeff (minpoly K pb.gen) (Fintype.card (Fin pb.dim) - 1) = -nextCoeff (minpoly K pb.gen)
rw₃ : -coeff (minpoly K pb.gen) (Fintype.card (Fin (natDegree (minpoly K pb.gen))) - 1) = -nextCoeff (minpoly K pb.gen)
⊢ (Algebra.trace K S : (a : S) → K) pb.gen = -nextCoeff (minpoly K pb.gen)
have rw₄ : -coeff (minpoly K pb.gen) (natDegree (minpoly K pb.gen) - 1) = -nextCoeff (minpoly K pb.gen)
Tactic: rw [trace_eq_matrix_trace pb.basis, trace_eq_neg_charpoly_coeff, charpoly_leftMulMatrix, ←
    pb.natDegree_minpoly, Fintype.card_fin, ← nextCoeff_of_natDegree_pos d_pos']
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : Field K
inst_2 : Algebra K S
inst_3 : Nontrivial S
pb : PowerBasis K S
d_pos : 0 < pb.dim
d_pos' : 0 < natDegree (minpoly K pb.gen)
this : Nonempty (Fin pb.dim)
rw :
  Matrix.trace (n := Fin pb.dim)
      (((leftMulMatrix pb.basis : S →ₐ[K] Matrix (Fin pb.dim) (Fin pb.dim) K) :
          (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) K)
        pb.gen) =
    -nextCoeff (minpoly K pb.gen)
rw₁ :
  -coeff
        (charpoly (n := Fin pb.dim)
          (((leftMulMatrix pb.basis : S →ₐ[K] Matrix (Fin pb.dim) (Fin pb.dim) K) :
              (a : S) → Matrix (Fin pb.dim) (Fin pb.dim) K)
            pb.gen))
        (Fintype.card (Fin pb.dim) - 1) =
    -nextCoeff (minpoly K pb.gen)
rw₂ : -coeff (minpoly K pb.gen) (Fintype.card (Fin pb.dim) - 1) = -nextCoeff (minpoly K pb.gen)
rw₃ : -coeff (minpoly K pb.gen) (Fintype.card (Fin (natDegree (minpoly K pb.gen))) - 1) = -nextCoeff (minpoly K pb.gen)
rw₄ : -coeff (minpoly K pb.gen) (natDegree (minpoly K pb.gen) - 1) = -nextCoeff (minpoly K pb.gen)
⊢ (Algebra.trace K S : (a : S) → K) pb.gen = -nextCoeff (minpoly K pb.gen)
have rw₅ : -nextCoeff (minpoly K pb.gen) = -nextCoeff (minpoly K pb.gen)
Tactic: rw [trace_eq_matrix_trace pb.basis, trace_eq_neg_charpoly_coeff, charpoly_leftMulMatrix, ←
    pb.natDegree_minpoly, Fintype.card_fin, ← nextCoeff_of_natDegree_pos d_pos']
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : Field K
F : Type u_6
inst_2 : Field F
inst_3 : Algebra K S
inst_4 : Algebra K F
inst_5 : Nontrivial S
pb : PowerBasis K S
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K pb.gen))
⊢ (algebraMap K F : (a : K) → F) ((Algebra.trace K S : (a : S) → K) pb.gen : K) = (aroots (minpoly K pb.gen) F).sum
have rw : (algebraMap K F : (a : K) → F) (-nextCoeff (minpoly K pb.gen)) = (aroots (minpoly K pb.gen) F).sum
Tactic: rw [PowerBasis.trace_gen_eq_nextCoeff_minpoly, map_neg,
    ← nextCoeff_map_eq, hf.nextCoeff_eq_neg_sum_roots_of_monic
      ((minpoly.monic (PowerBasis.isIntegral_gen _)).map _),
    neg_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : Field K
F : Type u_6
inst_2 : Field F
inst_3 : Algebra K S
inst_4 : Algebra K F
inst_5 : Nontrivial S
pb : PowerBasis K S
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K pb.gen))
rw : (algebraMap K F : (a : K) → F) (-nextCoeff (minpoly K pb.gen)) = (aroots (minpoly K pb.gen) F).sum
⊢ (algebraMap K F : (a : K) → F) ((Algebra.trace K S : (a : S) → K) pb.gen : K) = (aroots (minpoly K pb.gen) F).sum
have rw₁ : -(algebraMap K F : (a : K) → F) (nextCoeff (minpoly K pb.gen)) = (aroots (minpoly K pb.gen) F).sum
Tactic: rw [PowerBasis.trace_gen_eq_nextCoeff_minpoly, map_neg,
    ← nextCoeff_map_eq, hf.nextCoeff_eq_neg_sum_roots_of_monic
      ((minpoly.monic (PowerBasis.isIntegral_gen _)).map _),
    neg_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : Field K
F : Type u_6
inst_2 : Field F
inst_3 : Algebra K S
inst_4 : Algebra K F
inst_5 : Nontrivial S
pb : PowerBasis K S
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K pb.gen))
rw : (algebraMap K F : (a : K) → F) (-nextCoeff (minpoly K pb.gen)) = (aroots (minpoly K pb.gen) F).sum
rw₁ : -(algebraMap K F : (a : K) → F) (nextCoeff (minpoly K pb.gen)) = (aroots (minpoly K pb.gen) F).sum
⊢ (algebraMap K F : (a : K) → F) ((Algebra.trace K S : (a : S) → K) pb.gen : K) = (aroots (minpoly K pb.gen) F).sum
have rw₂ : -nextCoeff (Polynomial.map (algebraMap K F) (minpoly K pb.gen)) = (aroots (minpoly K pb.gen) F).sum
Tactic: rw [PowerBasis.trace_gen_eq_nextCoeff_minpoly, map_neg,
    ← nextCoeff_map_eq, hf.nextCoeff_eq_neg_sum_roots_of_monic
      ((minpoly.monic (PowerBasis.isIntegral_gen _)).map _),
    neg_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : Field K
F : Type u_6
inst_2 : Field F
inst_3 : Algebra K S
inst_4 : Algebra K F
inst_5 : Nontrivial S
pb : PowerBasis K S
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K pb.gen))
rw : (algebraMap K F : (a : K) → F) (-nextCoeff (minpoly K pb.gen)) = (aroots (minpoly K pb.gen) F).sum
rw₁ : -(algebraMap K F : (a : K) → F) (nextCoeff (minpoly K pb.gen)) = (aroots (minpoly K pb.gen) F).sum
rw₂ : -nextCoeff (Polynomial.map (algebraMap K F) (minpoly K pb.gen)) = (aroots (minpoly K pb.gen) F).sum
⊢ (algebraMap K F : (a : K) → F) ((Algebra.trace K S : (a : S) → K) pb.gen : K) = (aroots (minpoly K pb.gen) F).sum
have rw₃ : - -(roots (Polynomial.map (algebraMap K F) (minpoly K pb.gen))).sum = (aroots (minpoly K pb.gen) F).sum
Tactic: rw [PowerBasis.trace_gen_eq_nextCoeff_minpoly, map_neg,
    ← nextCoeff_map_eq, hf.nextCoeff_eq_neg_sum_roots_of_monic
      ((minpoly.monic (PowerBasis.isIntegral_gen _)).map _),
    neg_neg]
-- Lean 4 proof step from Mathlib.RingTheory.Trace.Basic (goal)
Goal:
S : Type u_2
inst : CommRing S
K : Type u_4
inst_1 : Field K
F : Type u_6
inst_2 : Field F
inst_3 : Algebra K S
inst_4 : Algebra K F
inst_5 : Nontrivial S
pb : PowerBasis K S
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K pb.gen))
rw : (algebraMap K F : (a : K) → F) (-nextCoeff (minpoly K pb.gen)) = (aroots (minpoly K pb.gen) F).sum
rw₁ : -(algebraMap K F : (a : K) → F) (nextCoeff (minpoly K pb.gen)) = (aroots (minpoly K pb.gen) F).sum
rw₂ : -nextCoeff (Polynomial.map (algebraMap K F) (minpoly K pb.gen)) = (aroots (minpoly K pb.gen) F).sum
rw₃ : - -(roots (Polynomial.map (algebraMap K F) (minpoly K pb.gen))).sum = (aroots (minpoly K pb.gen) F).sum
⊢ (algebraMap K F : (a : K) → F) ((Algebra.trace K S : (a : S) → K) pb.gen : K) = (aroots (minpoly K pb.gen) F).sum
have rw₄ : (roots (Polynomial.map (algebraMap K F) (minpoly K pb.gen))).sum = (aroots (minpoly K pb.gen) F).sum
Tactic: rw [PowerBasis.trace_gen_eq_nextCoeff_minpoly, map_neg,
    ← nextCoeff_map_eq, hf.nextCoeff_eq_neg_sum_roots_of_monic
      ((minpoly.monic (PowerBasis.isIntegral_gen _)).map _),
    neg_neg]
-- 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
x : L
hx : ¬IsIntegral K x
⊢ Eq.{u_4 + 1} (α := K) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (gen K x) : K) (0 : K)
have h : ¬∃ (s : Finset ↥K⟮x⟯), Nonempty (Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯)
Tactic: rw [trace_eq_zero_of_not_exists_basis, LinearMap.zero_apply]
-- 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
x : L
hx : ¬IsIntegral K x
⊢ ¬∃ (s : Finset ↥K⟮x⟯), Nonempty (Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯)
have h : ∀ (hx : ∃ (s : Finset ↥K⟮x⟯), Nonempty (Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯)), IsIntegral K x
Tactic: contrapose hx
Cleared hypotheses: hx
-- 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
x : L
hx : ∃ (s : Finset ↥K⟮x⟯), Nonempty (Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯)
⊢ IsIntegral K x
have h : ∀ (s : Finset ↥K⟮x⟯) (b : Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯), IsIntegral K x
Tactic: obtain ⟨s, ⟨b⟩⟩ := hx
Cleared hypotheses: hx
-- 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
x : L
s : Finset ↥K⟮x⟯
b : Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯
⊢ IsIntegral K x
have h : Submodule.FG.{u_4, u_5} (R := K) (M := L)
  ((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) (toSubalgebra K⟮x⟯))
Tactic: refine .of_mem_of_fg K⟮x⟯.toSubalgebra ?_ x ?_
-- 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
x : L
s : Finset ↥K⟮x⟯
b : Basis.{u_5, u_4, u_5} (↥s) K ↥K⟮x⟯
h :
  Submodule.FG.{u_4, u_5} (R := K) (M := L)
    ((Subalgebra.toSubmodule : (a : Subalgebra K L) → Submodule K L) (toSubalgebra K⟮x⟯))
⊢ IsIntegral K x
have h₁ : Membership.mem (γ := Subalgebra K L) (toSubalgebra K⟮x⟯) x
Tactic: refine .of_mem_of_fg K⟮x⟯.toSubalgebra ?_ x ?_
-- 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
F : Type u_6
inst_3 : Field F
inst_4 : Algebra K F
x : L
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
⊢ (algebraMap K F : (a : K) → F) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (gen K x) : K) =
    (aroots (minpoly K x) F).sum
have injKxL : Function.Injective (α := ↥K⟮x⟯) (β := L) (⇑(algebraMap (↥K⟮x⟯) L) : (a : ↥K⟮x⟯) → L)
Tactic: have injKxL := (algebraMap K⟮x⟯ L).injective
-- 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
F : Type u_6
inst_3 : Field F
inst_4 : Algebra K F
x : L
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
injKxL : Function.Injective (α := ↥K⟮x⟯) (β := L) (⇑(algebraMap (↥K⟮x⟯) L) : (a : ↥K⟮x⟯) → L)
⊢ (algebraMap K F : (a : K) → F) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (gen K x) : K) =
    (aroots (minpoly K x) F).sum
have pos : ∀ (hx : IsIntegral K x),
  (algebraMap K F : (a : K) → F) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (gen K x) : K) =
    (aroots (minpoly K x) F).sum
Tactic: by_cases hx : IsIntegral K x
-- 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
F : Type u_6
inst_3 : Field F
inst_4 : Algebra K F
x : L
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
injKxL : Function.Injective (α := ↥K⟮x⟯) (β := L) (⇑(algebraMap (↥K⟮x⟯) L) : (a : ↥K⟮x⟯) → L)
pos :
  ∀ (hx : IsIntegral K x),
    (algebraMap K F : (a : K) → F) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (gen K x) : K) =
      (aroots (minpoly K x) F).sum
⊢ (algebraMap K F : (a : K) → F) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (gen K x) : K) =
    (aroots (minpoly K x) F).sum
have neg : ∀ (hx : ¬IsIntegral K x),
  (algebraMap K F : (a : K) → F) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (gen K x) : K) =
    (aroots (minpoly K x) F).sum
Tactic: by_cases hx : IsIntegral K x
-- 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
F : Type u_6
inst_3 : Field F
inst_4 : Algebra K F
x : L
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
injKxL : Function.Injective (α := ↥K⟮x⟯) (β := L) (⇑(algebraMap (↥K⟮x⟯) L) : (a : ↥K⟮x⟯) → L)
hx : IsIntegral K x
⊢ (algebraMap K F : (a : K) → F) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (gen K x) : K) =
    (aroots (minpoly K x) F).sum
have pos : (aroots (minpoly K (adjoin.powerBasis hx).gen) F).sum = (aroots (minpoly K x) F).sum
Tactic: rw [← adjoin.powerBasis_gen hx, (adjoin.powerBasis hx).trace_gen_eq_sum_roots]
-- 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
F : Type u_6
inst_3 : Field F
inst_4 : Algebra K F
x : L
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
injKxL : Function.Injective (α := ↥K⟮x⟯) (β := L) (⇑(algebraMap (↥K⟮x⟯) L) : (a : ↥K⟮x⟯) → L)
hx : IsIntegral K x
pos : (aroots (minpoly K (adjoin.powerBasis hx).gen) F).sum = (aroots (minpoly K x) F).sum
⊢ (algebraMap K F : (a : K) → F) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (gen K x) : K) =
    (aroots (minpoly K x) F).sum
have pos₁ : Splits (Polynomial.map (algebraMap K F) (minpoly K (adjoin.powerBasis hx).gen))
Tactic: rw [← adjoin.powerBasis_gen hx, (adjoin.powerBasis hx).trace_gen_eq_sum_roots]
-- 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
F : Type u_6
inst_3 : Field F
inst_4 : Algebra K F
x : L
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
injKxL : Function.Injective (α := ↥K⟮x⟯) (β := L) (⇑(algebraMap (↥K⟮x⟯) L) : (a : ↥K⟮x⟯) → L)
hx : IsIntegral K x
⊢ (aroots (minpoly K (adjoin.powerBasis hx).gen) F).sum = (aroots (minpoly K x) F).sum
have pos : (aroots (minpoly K (B := L) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (gen K x) : L)) F).sum =
  (aroots (minpoly K x) F).sum
Tactic: rw [adjoin.powerBasis_gen hx, ← minpoly.algebraMap_eq injKxL]
-- 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
F : Type u_6
inst_3 : Field F
inst_4 : Algebra K F
x : L
hf : Splits (Polynomial.map (algebraMap K F) (minpoly K x))
injKxL : Function.Injective (α := ↥K⟮x⟯) (β := L) (⇑(algebraMap (↥K⟮x⟯) L) : (a : ↥K⟮x⟯) → L)
hx : IsIntegral K x
⊢ Splits (Polynomial.map (algebraMap K F) (minpoly K (adjoin.powerBasis hx).gen))
have pos : Splits (Polynomial.map (algebraMap K F) (minpoly K (B := L) ((algebraMap (↥K⟮x⟯) L : (a : ↥K⟮x⟯) → L) (gen K x) : L)))
Tactic: rw [adjoin.powerBasis_gen hx, ← minpoly.algebraMap_eq injKxL]
-- 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
x : L
⊢ (Algebra.trace K L : (a : L) → K) x =
    HSMul.hSMul (β := K) (finrank (↥K⟮x⟯) L) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K)
have rw : (Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) ((Algebra.trace (↥K⟮x⟯) L : (a : L) → ↥K⟮x⟯) x : ↥K⟮x⟯) =
  HSMul.hSMul (β := K) (finrank (↥K⟮x⟯) L) ((Algebra.trace K ↥K⟮x⟯ : (a : ↥K⟮x⟯) → K) (AdjoinSimple.gen K x) : K)
Tactic: rw [← trace_trace (S := K⟮x⟯)]