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
κ : Type w
E : Type z
inst_3 : Field E
inst_4 : Algebra K E
inst_5 : Module.Finite K L
inst_6 : Algebra.IsSeparable K L
inst_7 : IsAlgClosed E
b : κ → L
inst_8 : Fintype κ
e : κ ≃ (L →ₐ[K] E)
rw :
  HMul.hMul (α := Matrix κ (L →ₐ[K] E) E) (β := Matrix (L →ₐ[K] E) κ E) (embeddingsMatrix K E b)
      (embeddingsMatrix K E b)ᵀ =
    embeddingsMatrixReindex K E b e * (embeddingsMatrixReindex K E b e)ᵀ
rw₁ :
  HMul.hMul (α := Matrix κ (L →ₐ[K] E) E) (β := Matrix (L →ₐ[K] E) κ E) (embeddingsMatrix K E b)
      (embeddingsMatrix K E b)ᵀ =
    HMul.hMul (α := Matrix κ κ E) (β := Matrix κ κ E)
      ((reindex (Equiv.refl κ) e.symm : (a : Matrix κ (L →ₐ[K] E) E) → Matrix κ κ E) (embeddingsMatrix K E b) :
        Matrix κ κ E)
      ((reindex (Equiv.refl κ) e.symm : (a : Matrix κ (L →ₐ[K] E) E) → Matrix κ κ E) (embeddingsMatrix K E b))ᵀ
rw₂ :
  HMul.hMul (α := Matrix κ (L →ₐ[K] E) E) (β := Matrix (L →ₐ[K] E) κ E) (embeddingsMatrix K E b)
      (embeddingsMatrix K E b)ᵀ =
    HMul.hMul (α := Matrix κ κ E)
      (submatrix (n := L →ₐ[K] E) (embeddingsMatrix K E b) (⇑(Equiv.refl κ).symm : (a : κ) → κ)
        (⇑e.symm.symm : (a : κ) → L →ₐ[K] E))
      (submatrix (n := L →ₐ[K] E) (embeddingsMatrix K E b) (⇑(Equiv.refl κ).symm : (a : κ) → κ)
          (⇑e.symm.symm : (a : κ) → L →ₐ[K] E))ᵀ
rw₃ :
  HMul.hMul (α := Matrix κ (L →ₐ[K] E) E) (β := Matrix (L →ₐ[K] E) κ E) (embeddingsMatrix K E b)
      (embeddingsMatrix K E b)ᵀ =
    HMul.hMul (α := Matrix κ κ E)
      (submatrix (n := L →ₐ[K] E) (embeddingsMatrix K E b) (⇑(Equiv.refl κ).symm : (a : κ) → κ)
        (⇑e.symm.symm : (a : κ) → L →ₐ[K] E))
      (submatrix (m := L →ₐ[K] E) (embeddingsMatrix K E b)ᵀ (⇑e.symm.symm : (a : κ) → L →ₐ[K] E)
        (⇑(Equiv.refl κ).symm : (a : κ) → κ))
⊢ (traceMatrix K b).map (⇑(algebraMap K E) : (a : K) → E) =
    embeddingsMatrixReindex K E b e * (embeddingsMatrixReindex K E b e)ᵀ
have rw₄ : submatrix (n := L →ₐ[K] E) (embeddingsMatrix K E b) _root_.id (⇑e.symm.symm : (a : κ) → L →ₐ[K] E) *
    submatrix (m := L →ₐ[K] E) (embeddingsMatrix K E b)ᵀ (⇑e.symm.symm : (a : κ) → L →ₐ[K] E) _root_.id =
  HMul.hMul (α := Matrix κ κ E)
    (submatrix (n := L →ₐ[K] E) (embeddingsMatrix K E b) (⇑(Equiv.refl κ).symm : (a : κ) → κ)
      (⇑e.symm.symm : (a : κ) → L →ₐ[K] E))
    (submatrix (m := L →ₐ[K] E) (embeddingsMatrix K E b)ᵀ (⇑e.symm.symm : (a : κ) → L →ₐ[K] E)
      (⇑(Equiv.refl κ).symm : (a : κ) → κ))
Tactic: rw [traceMatrix_eq_embeddingsMatrix_mul_trans, embeddingsMatrixReindex, reindex_apply,
    transpose_submatrix, ← submatrix_mul_transpose_submatrix, ← Equiv.coe_refl, Equiv.refl_symm]
-- 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
pb : PowerBasis K L
inst_3 : Algebra.IsSeparable K L
this :
  Ne.{u_5 + 1} (α := AlgebraicClosure L)
    ((algebraMap K (AlgebraicClosure L) : (a : K) → AlgebraicClosure L)
        (det (n := Fin pb.dim) (traceMatrix.{u_4, u_5, 0} K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L))) :
      AlgebraicClosure L)
    (0 : AlgebraicClosure L)
⊢ det (n := Fin pb.dim) (traceMatrix.{u_4, u_5, 0} K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L)) ≠ 0
have refine : ∀ (ht : det (n := Fin pb.dim) (traceMatrix.{u_4, u_5, 0} K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L)) = 0),
  Eq.{u_5 + 1} (α := AlgebraicClosure L)
    ((algebraMap K (AlgebraicClosure L) : (a : K) → AlgebraicClosure L)
        (det (n := Fin pb.dim) (traceMatrix.{u_4, u_5, 0} K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L))) :
      AlgebraicClosure L)
    (0 : AlgebraicClosure L)
Tactic: refine mt (fun ht => ?_) 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
pb : PowerBasis K L
inst_3 : Algebra.IsSeparable K L
this :
  Ne.{u_5 + 1} (α := AlgebraicClosure L)
    ((algebraMap K (AlgebraicClosure L) : (a : K) → AlgebraicClosure L)
        (det (n := Fin pb.dim) (traceMatrix.{u_4, u_5, 0} K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L))) :
      AlgebraicClosure L)
    (0 : AlgebraicClosure L)
ht : det (n := Fin pb.dim) (traceMatrix.{u_4, u_5, 0} K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L)) = 0
⊢ Eq.{u_5 + 1} (α := AlgebraicClosure L)
    ((algebraMap K (AlgebraicClosure L) : (a : K) → AlgebraicClosure L)
        (det (n := Fin pb.dim) (traceMatrix.{u_4, u_5, 0} K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L))) :
      AlgebraicClosure L)
    (0 : AlgebraicClosure L)
have rw : Eq.{u_5 + 1} (α := AlgebraicClosure L) ((algebraMap K (AlgebraicClosure L) : (a : K) → AlgebraicClosure L) 0) 0
Tactic: rw [ht, map_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
pb : PowerBasis K L
inst_3 : Algebra.IsSeparable K L
this :
  Ne.{u_5 + 1} (α := AlgebraicClosure L)
    ((algebraMap K (AlgebraicClosure L) : (a : K) → AlgebraicClosure L)
        (det (n := Fin pb.dim) (traceMatrix.{u_4, u_5, 0} K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L))) :
      AlgebraicClosure L)
    (0 : AlgebraicClosure L)
ht : det (n := Fin pb.dim) (traceMatrix.{u_4, u_5, 0} K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L)) = 0
rw : Eq.{u_5 + 1} (α := AlgebraicClosure L) ((algebraMap K (AlgebraicClosure L) : (a : K) → AlgebraicClosure L) 0) 0
⊢ Eq.{u_5 + 1} (α := AlgebraicClosure L)
    ((algebraMap K (AlgebraicClosure L) : (a : K) → AlgebraicClosure L)
        (det (n := Fin pb.dim) (traceMatrix.{u_4, u_5, 0} K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L))) :
      AlgebraicClosure L)
    (0 : AlgebraicClosure L)
have rw₁ : Eq.{u_5 + 1} (α := AlgebraicClosure L) 0 0
Tactic: rw [ht, map_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
pb : PowerBasis K L
inst_3 : Algebra.IsSeparable K L
⊢ det (n := Fin pb.dim) (traceMatrix.{u_4, u_5, 0} K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L)) ≠ 0
have suffices : Ne.{u_5 + 1} (α := AlgebraicClosure L)
  ((algebraMap K (AlgebraicClosure L) : (a : K) → AlgebraicClosure L)
      (det (n := Fin pb.dim) (traceMatrix.{u_4, u_5, 0} K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L))) :
    AlgebraicClosure L)
  (0 : AlgebraicClosure L)
Tactic: suffices algebraMap K (AlgebraicClosure L) (det (traceMatrix K pb.basis)) ≠ 0 by
    refine mt (fun ht => ?_) this
    rw [ht, map_zero]
-- 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
pb : PowerBasis K L
inst_3 : Algebra.IsSeparable K L
⊢ Ne.{u_5 + 1} (α := AlgebraicClosure L)
    ((algebraMap K (AlgebraicClosure L) : (a : K) → AlgebraicClosure L)
        (det (n := Fin pb.dim) (traceMatrix.{u_4, u_5, 0} K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L))) :
      AlgebraicClosure L)
    (0 : AlgebraicClosure L)
have this : FiniteDimensional K L
Tactic: haveI : FiniteDimensional K L := pb.finite
-- 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
pb : PowerBasis K L
inst_3 : Algebra.IsSeparable K L
this : FiniteDimensional K L
refine_2 :
  Ne.{u_5 + 1} (α := AlgebraicClosure L)
    ((algebraMap K (AlgebraicClosure L) : (a : K) → AlgebraicClosure L)
        (det (n := Fin pb.dim) (traceMatrix.{u_4, u_5, 0} K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L))) :
      AlgebraicClosure L)
    (0 : AlgebraicClosure L)
⊢ Ne.{u_5 + 1} (α := AlgebraicClosure L)
    ((algebraMap K (AlgebraicClosure L) : (a : K) → AlgebraicClosure L)
        (det (n := Fin pb.dim) (traceMatrix.{u_4, u_5, 0} K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L))) :
      AlgebraicClosure L)
    (0 : AlgebraicClosure L)
have refine_1 : Fintype.card.{u_5} (L →ₐ[K] AlgebraicClosure L) = pb.dim
Tactic: let e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?_).symm
-- 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
pb : PowerBasis K L
inst_3 : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := Equiv.symm (Fintype.equivFinOfCardEq ⋯)
⊢ Ne.{u_5 + 1} (α := AlgebraicClosure L)
    ((algebraMap K (AlgebraicClosure L) : (a : K) → AlgebraicClosure L)
        (det (n := Fin pb.dim) (traceMatrix.{u_4, u_5, 0} K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L))) :
      AlgebraicClosure L)
    (0 : AlgebraicClosure L)
have refine_2 : HMul.hMul (α := AlgebraicClosure L)
    (det (n := Fin pb.dim)
      (vandermonde fun (i : Fin pb.dim) ↦
        (((e : (a : Fin pb.dim) → L →ₐ[K] AlgebraicClosure L) i : L →ₐ[K] AlgebraicClosure L) :
            (a : L) → AlgebraicClosure L)
          pb.gen))
    (det (n := Fin pb.dim)
      (vandermonde fun (i : Fin pb.dim) ↦
            (((e : (a : Fin pb.dim) → L →ₐ[K] AlgebraicClosure L) i : L →ₐ[K] AlgebraicClosure L) :
                (a : L) → AlgebraicClosure L)
              pb.gen)ᵀᵀ) ≠
  0
Tactic: rw [RingHom.map_det, RingHom.mapMatrix_apply,
      traceMatrix_eq_embeddingsMatrixReindex_mul_trans K _ _ e,
      embeddingsMatrixReindex_eq_vandermonde, det_mul, det_transpose]
-- 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
pb : PowerBasis K L
inst_3 : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := Equiv.symm (Fintype.equivFinOfCardEq ⋯)
⊢ HMul.hMul (α := AlgebraicClosure L)
      (det (n := Fin pb.dim)
        (vandermonde fun (i : Fin pb.dim) ↦
          (((e : (a : Fin pb.dim) → L →ₐ[K] AlgebraicClosure L) i : L →ₐ[K] AlgebraicClosure L) :
              (a : L) → AlgebraicClosure L)
            pb.gen))
      (det (n := Fin pb.dim)
        (vandermonde fun (i : Fin pb.dim) ↦
              (((e : (a : Fin pb.dim) → L →ₐ[K] AlgebraicClosure L) i : L →ₐ[K] AlgebraicClosure L) :
                  (a : L) → AlgebraicClosure L)
                pb.gen)ᵀᵀ) ≠
    0
have refine_2 : ¬Eq.{u_5 + 1} (α := AlgebraicClosure L)
    (det (n := Fin pb.dim)
      (vandermonde fun (i : Fin pb.dim) ↦
        (((e : (a : Fin pb.dim) → L →ₐ[K] AlgebraicClosure L) i : L →ₐ[K] AlgebraicClosure L) :
            (a : L) → AlgebraicClosure L)
          pb.gen))
    0
Tactic: refine mt mul_self_eq_zero.mp ?_
-- 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
pb : PowerBasis K L
inst_3 : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := Equiv.symm (Fintype.equivFinOfCardEq ⋯)
⊢ ¬Eq.{u_5 + 1} (α := AlgebraicClosure L)
      (det (n := Fin pb.dim)
        (vandermonde fun (i : Fin pb.dim) ↦
          (((e : (a : Fin pb.dim) → L →ₐ[K] AlgebraicClosure L) i : L →ₐ[K] AlgebraicClosure L) :
              (a : L) → AlgebraicClosure L)
            pb.gen))
      0
have refine_2 : ∀ (x : Fin pb.dim),
  ¬(Membership.mem (γ := Finset (Fin pb.dim)) Finset.univ x ∧
      ∃ a ∈ Finset.Ioi x,
        Eq (α := AlgebraicClosure L)
          ((((e : (a : Fin pb.dim) → L →ₐ[K] AlgebraicClosure L) a : L →ₐ[K] AlgebraicClosure L) :
                (a : L) → AlgebraicClosure L)
              pb.gen :
            AlgebraicClosure L)
          ((((e : (a : Fin pb.dim) → L →ₐ[K] AlgebraicClosure L) x : L →ₐ[K] AlgebraicClosure L) :
                (a : L) → AlgebraicClosure L)
              pb.gen :
            AlgebraicClosure L))
Tactic: simp only [det_vandermonde, Finset.prod_eq_zero_iff, not_exists, sub_eq_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
pb : PowerBasis K L
inst_3 : Algebra.IsSeparable K L
this : FiniteDimensional K L
⊢ Fintype.card.{u_5} (L →ₐ[K] AlgebraicClosure L) = pb.dim
have refine_1 : finrank K L = pb.dim
Tactic: rw [AlgHom.card, pb.finrank]
-- 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
pb : PowerBasis K L
inst_3 : Algebra.IsSeparable K L
this : FiniteDimensional K L
refine_1 : finrank K L = pb.dim
⊢ Fintype.card.{u_5} (L →ₐ[K] AlgebraicClosure L) = pb.dim
have refine_1₁ : pb.dim = pb.dim
Tactic: rw [AlgHom.card, pb.finrank]
-- 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
ι : Type w
inst_3 : Algebra.IsSeparable K L
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis ι K L
⊢ Ne.{u_4 + 1} (α := K)
    (det.{u_4, w} (n := ι) ((LinearMap.BilinForm.toMatrix b : (a : BilinForm K L) → Matrix ι ι K) (traceForm K L))) 0
have this : FiniteDimensional K L
Tactic: haveI : FiniteDimensional K L := b.finiteDimensional_of_finite
-- 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
ι : Type w
inst_3 : Algebra.IsSeparable K L
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ Ne.{u_4 + 1} (α := K)
    (det.{u_4, w} (n := ι) ((LinearMap.BilinForm.toMatrix b : (a : BilinForm K L) → Matrix ι ι K) (traceForm K L))) 0
have rw : (pb.basis.toMatrix (⇑b : (a : ι) → L) * (pb.basis.toMatrix (⇑b : (a : ι) → L))ᵀ).det *
    det (n := Fin pb.dim)
      ((LinearMap.BilinForm.toMatrix pb.basis : (a : BilinForm K L) → Matrix (Fin pb.dim) (Fin pb.dim) K)
        (traceForm K L)) ≠
  0
Tactic: rw [← LinearMap.BilinForm.toMatrix_mul_basis_toMatrix pb.basis b, ←
    det_comm' (pb.basis.toMatrix_mul_toMatrix_flip b) _, ← Matrix.mul_assoc, det_mul]
-- 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
ι : Type w
inst_3 : Algebra.IsSeparable K L
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
rw :
  (pb.basis.toMatrix (⇑b : (a : ι) → L) * (pb.basis.toMatrix (⇑b : (a : ι) → L))ᵀ).det *
      det (n := Fin pb.dim)
        ((LinearMap.BilinForm.toMatrix pb.basis : (a : BilinForm K L) → Matrix (Fin pb.dim) (Fin pb.dim) K)
          (traceForm K L)) ≠
    0
⊢ Ne.{u_4 + 1} (α := K)
    (det.{u_4, w} (n := ι) ((LinearMap.BilinForm.toMatrix b : (a : BilinForm K L) → Matrix ι ι K) (traceForm K L))) 0
have rw₁ : HMul.hMul (α := Matrix ι (Fin pb.dim) K) (β := Matrix (Fin pb.dim) ι K) (b.toMatrix (⇑pb.basis : (a : Fin pb.dim) → L))
    (pb.basis.toMatrix (⇑b : (a : ι) → L)) =
  1
Tactic: rw [← LinearMap.BilinForm.toMatrix_mul_basis_toMatrix pb.basis b, ←
    det_comm' (pb.basis.toMatrix_mul_toMatrix_flip b) _, ← Matrix.mul_assoc, det_mul]
-- 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
ι : Type w
inst_3 : Algebra.IsSeparable K L
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ (pb.basis.toMatrix (⇑b : (a : ι) → L) * (pb.basis.toMatrix (⇑b : (a : ι) → L))ᵀ).det *
      det (n := Fin pb.dim)
        ((LinearMap.BilinForm.toMatrix pb.basis : (a : BilinForm K L) → Matrix (Fin pb.dim) (Fin pb.dim) K)
          (traceForm K L)) ≠
    0
have refine_1 : (pb.basis.toMatrix (⇑b : (a : ι) → L) * (pb.basis.toMatrix (⇑b : (a : ι) → L))ᵀ).det *
    (HMul.hMul (α := Matrix (Fin pb.dim) ι K) (β := Matrix ι (Fin pb.dim) K)
        (b.toMatrix (⇑pb.basis : (a : Fin pb.dim) → L))ᵀ (b.toMatrix (⇑pb.basis : (a : Fin pb.dim) → L))).det =
  1
Tactic: refine
    mul_ne_zero
      (IsUnit.of_mul_eq_one ((b.toMatrix pb.basis)ᵀ * b.toMatrix pb.basis).det ?_).ne_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
ι : Type w
inst_3 : Algebra.IsSeparable K L
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
refine_1 :
  (pb.basis.toMatrix (⇑b : (a : ι) → L) * (pb.basis.toMatrix (⇑b : (a : ι) → L))ᵀ).det *
      (HMul.hMul (α := Matrix (Fin pb.dim) ι K) (β := Matrix ι (Fin pb.dim) K)
          (b.toMatrix (⇑pb.basis : (a : Fin pb.dim) → L))ᵀ (b.toMatrix (⇑pb.basis : (a : Fin pb.dim) → L))).det =
    1
⊢ (pb.basis.toMatrix (⇑b : (a : ι) → L) * (pb.basis.toMatrix (⇑b : (a : ι) → L))ᵀ).det *
      det (n := Fin pb.dim)
        ((LinearMap.BilinForm.toMatrix pb.basis : (a : BilinForm K L) → Matrix (Fin pb.dim) (Fin pb.dim) K)
          (traceForm K L)) ≠
    0
have refine_2 : Ne.{u_4 + 1} (α := K)
  (det (n := Fin pb.dim)
    ((LinearMap.BilinForm.toMatrix pb.basis : (a : BilinForm K L) → Matrix (Fin pb.dim) (Fin pb.dim) K)
      (traceForm K L)))
  0
Tactic: refine
    mul_ne_zero
      (IsUnit.of_mul_eq_one ((b.toMatrix pb.basis)ᵀ * b.toMatrix pb.basis).det ?_).ne_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
ι : Type w
inst_3 : Algebra.IsSeparable K L
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ (pb.basis.toMatrix (⇑b : (a : ι) → L) * (pb.basis.toMatrix (⇑b : (a : ι) → L))ᵀ).det *
      (HMul.hMul (α := Matrix (Fin pb.dim) ι K) (β := Matrix ι (Fin pb.dim) K)
          (b.toMatrix (⇑pb.basis : (a : Fin pb.dim) → L))ᵀ (b.toMatrix (⇑pb.basis : (a : Fin pb.dim) → L))).det =
    1
have b₁ : (pb.basis.toMatrix (⇑b : (a : ι) → L) * (pb.basis.toMatrix (⇑b : (a : ι) → L))ᵀ).det *
    (HMul.hMul (α := Matrix (Fin pb.dim) ι K) (β := Matrix ι (Fin pb.dim) K)
        (b.toMatrix (⇑pb.basis : (a : Fin pb.dim) → L))ᵀ (b.toMatrix (⇑pb.basis : (a : Fin pb.dim) → L))).det =
  (HMul.hMul (β := Matrix ι (Fin pb.dim) K)
      (HMul.hMul (α := Matrix (Fin pb.dim) ι K) (pb.basis.toMatrix (⇑b : (a : ι) → L))
        (HMul.hMul (α := Matrix ι (Fin pb.dim) K) (β := Matrix (Fin pb.dim) ι K)
            (b.toMatrix (⇑pb.basis : (a : Fin pb.dim) → L)) (pb.basis.toMatrix (⇑b : (a : ι) → L)))ᵀ)
      (b.toMatrix (⇑pb.basis : (a : Fin pb.dim) → L))).det
Tactic: calc
      (pb.basis.toMatrix b * (pb.basis.toMatrix b)ᵀ).det *
            ((b.toMatrix pb.basis)ᵀ * b.toMatrix pb.basis).det =
          (pb.basis.toMatrix b * (b.toMatrix pb.basis * pb.basis.toMatrix b)ᵀ *
              b.toMatrix pb.basis).det := by
        simp only [← det_mul, Matrix.mul_assoc, Matrix.transpose_mul]
      _ = 1 := by
        simp only [Basis.toMatrix_mul_toMatrix_flip, Matrix.transpose_one, Matrix.mul_one,
          Matrix.det_one]
-- 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
ι : Type w
inst_3 : Algebra.IsSeparable K L
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
b₁ :
  (pb.basis.toMatrix (⇑b : (a : ι) → L) * (pb.basis.toMatrix (⇑b : (a : ι) → L))ᵀ).det *
      (HMul.hMul (α := Matrix (Fin pb.dim) ι K) (β := Matrix ι (Fin pb.dim) K)
          (b.toMatrix (⇑pb.basis : (a : Fin pb.dim) → L))ᵀ (b.toMatrix (⇑pb.basis : (a : Fin pb.dim) → L))).det =
    (HMul.hMul (β := Matrix ι (Fin pb.dim) K)
        (HMul.hMul (α := Matrix (Fin pb.dim) ι K) (pb.basis.toMatrix (⇑b : (a : ι) → L))
          (HMul.hMul (α := Matrix ι (Fin pb.dim) K) (β := Matrix (Fin pb.dim) ι K)
              (b.toMatrix (⇑pb.basis : (a : Fin pb.dim) → L)) (pb.basis.toMatrix (⇑b : (a : ι) → L)))ᵀ)
        (b.toMatrix (⇑pb.basis : (a : Fin pb.dim) → L))).det
⊢ (pb.basis.toMatrix (⇑b : (a : ι) → L) * (pb.basis.toMatrix (⇑b : (a : ι) → L))ᵀ).det *
      (HMul.hMul (α := Matrix (Fin pb.dim) ι K) (β := Matrix ι (Fin pb.dim) K)
          (b.toMatrix (⇑pb.basis : (a : Fin pb.dim) → L))ᵀ (b.toMatrix (⇑pb.basis : (a : Fin pb.dim) → L))).det =
    1
have b₂ : (HMul.hMul (β := Matrix ι (Fin pb.dim) K)
      (HMul.hMul (α := Matrix (Fin pb.dim) ι K) (pb.basis.toMatrix (⇑b : (a : ι) → L))
        (HMul.hMul (α := Matrix ι (Fin pb.dim) K) (β := Matrix (Fin pb.dim) ι K)
            (b.toMatrix (⇑pb.basis : (a : Fin pb.dim) → L)) (pb.basis.toMatrix (⇑b : (a : ι) → L)))ᵀ)
      (b.toMatrix (⇑pb.basis : (a : Fin pb.dim) → L))).det =
  1
Tactic: calc
      (pb.basis.toMatrix b * (pb.basis.toMatrix b)ᵀ).det *
            ((b.toMatrix pb.basis)ᵀ * b.toMatrix pb.basis).det =
          (pb.basis.toMatrix b * (b.toMatrix pb.basis * pb.basis.toMatrix b)ᵀ *
              b.toMatrix pb.basis).det := by
        simp only [← det_mul, Matrix.mul_assoc, Matrix.transpose_mul]
      _ = 1 := by
        simp only [Basis.toMatrix_mul_toMatrix_flip, Matrix.transpose_one, Matrix.mul_one,
          Matrix.det_one]
-- 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
⊢ [Algebra.IsSeparable K L, Ne (α := L →ₗ[K] K) (Algebra.trace K L) 0, BilinForm.Nondegenerate (traceForm K L)].TFAE
have tfae_1_to_3 : ∀ (a : Algebra.IsSeparable K L), BilinForm.Nondegenerate (traceForm K L)
Tactic: tfae_have 1 → 3 := fun _ ↦ traceForm_nondegenerate K L
-- 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
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
⊢ Eq (α := BilinForm K L) (traceForm K L) 0
have 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)
Tactic: ext
-- 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
tfae_1_to_3 : ∀ (a : Algebra.IsSeparable K L), BilinForm.Nondegenerate (traceForm K L)
⊢ [Algebra.IsSeparable K L, Ne (α := L →ₗ[K] K) (Algebra.trace K L) 0, BilinForm.Nondegenerate (traceForm K L)].TFAE
have tfae_3_to_2 : ∀ (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₂])
-- 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
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, Ne (α := L →ₗ[K] K) (Algebra.trace K L) 0, BilinForm.Nondegenerate (traceForm K L)].TFAE
have tfae_2_to_1 : ∀ (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
-- 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
⊢ Function.Surjective.{u_5 + 1, u_4 + 1} (α := L) (β := K) (⇑(trace K L) : (a : L) → K)
have rw : Eq (α := Submodule K K) (range (trace K L)) ⊤
Tactic: rw [← LinearMap.range_eq_top]
-- 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 (α := Submodule K K) (range (trace K L)) ⊤
have apply : ¬Eq (α := Ideal K) (range (trace K L)) ⊥
Tactic: apply (IsSimpleOrder.eq_bot_or_eq_top (α := Ideal K) _).resolve_left