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
κ : 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
i j : κ
⊢ (traceMatrix K b).map (⇑(algebraMap K E) : (a : K) → E) i j =
    HMul.hMul (α := Matrix κ (L →ₐ[K] E) E) (β := Matrix (L →ₐ[K] E) κ E) (embeddingsMatrix K E b)
      (embeddingsMatrix K E b)ᵀ i j

Tactic:
simp [trace_eq_sum_embeddings, embeddingsMatrix, Matrix.mul_apply]

Premises used: Matrix.mul_apply, trace_eq_sum_embeddings, Algebra.embeddingsMatrix
-- 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
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

Tactic:
mt (fun ht => ?_) this

Premises used: mt
-- 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
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)
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)
⊢ det (n := Fin pb.dim) (traceMatrix.{u_4, u_5, 0} K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L)) ≠ 0

Tactic:
refine mt (fun ht => ?_) this

Premises used: mt
-- 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
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
rw₁ rw₂ : Eq.{u_5 + 1} (α := 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)

Tactic:
rw [ht, map_zero]

Premises used: map_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
pb : PowerBasis K L
inst_3 : Algebra.IsSeparable K L
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)
⊢ det (n := Fin pb.dim) (traceMatrix.{u_4, u_5, 0} K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L)) ≠ 0

Tactic:
suffices algebraMap K (AlgebraicClosure L) (det (traceMatrix K pb.basis)) ≠ 0 by
    refine mt (fun ht => ?_) this
    rw [ht, map_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
pb : PowerBasis K L
inst_3 : Algebra.IsSeparable K L
⊢ FiniteDimensional K L

Tactic:
haveI : FiniteDimensional K L := pb.finite
-- 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
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)
refine_1 : Fintype.card.{u_5} (L →ₐ[K] AlgebraicClosure L) = pb.dim
⊢ 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:
let e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?_).symm
-- 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
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 ⋯)
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
⊢ 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:
rw [RingHom.map_det, RingHom.mapMatrix_apply,
      traceMatrix_eq_embeddingsMatrixReindex_mul_trans K _ _ e,
      embeddingsMatrixReindex_eq_vandermonde, det_mul, det_transpose]

Premises used: Matrix.det_transpose, RingHom.mapMatrix_apply, Algebra.embeddingsMatrixReindex_eq_vandermonde, Matrix.det_mul, RingHom.map_det, Algebra.traceMatrix_eq_embeddingsMatrixReindex_mul_trans
-- 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
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

Tactic:
mt mul_self_eq_zero.mp ?_

Premises used: mul_self_eq_zero, mt, 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
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 ⋯)
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
⊢ 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:
refine mt mul_self_eq_zero.mp ?_

Premises used: mul_self_eq_zero, mt, 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
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 ⋯)
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))
⊢ ¬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:
simp only [det_vandermonde, Finset.prod_eq_zero_iff, not_exists, sub_eq_zero]

Premises used: Matrix.det_vandermonde, sub_eq_zero, not_exists, Finset.prod_eq_zero_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
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 ⋯)
i : Fin pb.dim
left : Membership.mem (γ := Finset (Fin pb.dim)) Finset.univ i
j : Fin pb.dim
hij : j ∈ Finset.Ioi i
h :
  Eq (α := AlgebraicClosure L)
    ((((e : (a : Fin pb.dim) → L →ₐ[K] AlgebraicClosure L) j : L →ₐ[K] AlgebraicClosure L) :
          (a : L) → AlgebraicClosure L)
        pb.gen :
      AlgebraicClosure L)
    ((((e : (a : Fin pb.dim) → L →ₐ[K] AlgebraicClosure L) i : L →ₐ[K] AlgebraicClosure L) :
          (a : L) → AlgebraicClosure L)
        pb.gen :
      AlgebraicClosure L)
⊢ False

Tactic:
(Finset.mem_Ioi.mp hij).ne' (e.injective <| pb.algHom_ext h)

Premises used: Finset.mem_Ioi, LT.lt.ne', Iff.mp, PowerBasis.algHom_ext, Equiv.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
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 ⋯)
i : Fin pb.dim
left : Membership.mem (γ := Finset (Fin pb.dim)) Finset.univ i
j : Fin pb.dim
hij : j ∈ Finset.Ioi i
h :
  Eq (α := AlgebraicClosure L)
    ((((e : (a : Fin pb.dim) → L →ₐ[K] AlgebraicClosure L) j : L →ₐ[K] AlgebraicClosure L) :
          (a : L) → AlgebraicClosure L)
        pb.gen :
      AlgebraicClosure L)
    ((((e : (a : Fin pb.dim) → L →ₐ[K] AlgebraicClosure L) i : L →ₐ[K] AlgebraicClosure L) :
          (a : L) → AlgebraicClosure L)
        pb.gen :
      AlgebraicClosure L)
⊢ False

Tactic:
exact (Finset.mem_Ioi.mp hij).ne' (e.injective <| pb.algHom_ext h)

Premises used: Finset.mem_Ioi, LT.lt.ne', Iff.mp, PowerBasis.algHom_ext, Equiv.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
pb : PowerBasis K L
inst_3 : Algebra.IsSeparable K L
this : FiniteDimensional K L
refine_1 : finrank K L = pb.dim
refine_1₁ refine_1₂ : pb.dim = pb.dim
⊢ Fintype.card.{u_5} (L →ₐ[K] AlgebraicClosure L) = pb.dim

Tactic:
rw [AlgHom.card, pb.finrank]

Premises used: PowerBasis.finrank, AlgHom.card
-- 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 : Algebra.IsSeparable K L
inst_4 : Fintype ι
inst_5 : DecidableEq ι
b : Basis ι K L
⊢ FiniteDimensional K L

Tactic:
haveI : FiniteDimensional K L := b.finiteDimensional_of_finite
-- 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 : 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
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
⊢ Ne.{u_4 + 1} (α := K)
    (det.{u_4, w} (n := ι) ((LinearMap.BilinForm.toMatrix b : (a : BilinForm K L) → Matrix ι ι 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]

Premises used: Matrix.mul_assoc, PowerBasis.basis, Matrix.det_mul, Module.Basis.toMatrix_mul_toMatrix_flip, LinearMap.BilinForm.toMatrix_mul_basis_toMatrix, Matrix.det_comm'
-- 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 : 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
⊢ 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:
apply Basis.toMatrix_mul_toMatrix_flip

Premises used: Module.Basis.toMatrix_mul_toMatrix_flip
-- 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 : 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

Tactic:
mul_ne_zero
      (IsUnit.of_mul_eq_one ((b.toMatrix pb.basis)ᵀ * b.toMatrix pb.basis).det ?_).ne_zero ?_

Premises used: HMul.hMul, IsUnit.of_mul_eq_one, Module.Basis.toMatrix, PowerBasis.basis, Matrix.transpose, IsUnit.ne_zero, mul_ne_zero, DFunLike.coe, Matrix.det
-- 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 : 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
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
⊢ (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:
refine
    mul_ne_zero
      (IsUnit.of_mul_eq_one ((b.toMatrix pb.basis)ᵀ * b.toMatrix pb.basis).det ?_).ne_zero ?_

Premises used: HMul.hMul, IsUnit.of_mul_eq_one, Module.Basis.toMatrix, PowerBasis.basis, Matrix.transpose, IsUnit.ne_zero, mul_ne_zero, DFunLike.coe, Matrix.det
-- 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 : 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 =
    (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:
simp only [← det_mul, Matrix.mul_assoc, Matrix.transpose_mul]

Premises used: Matrix.mul_assoc, Matrix.transpose_mul, Matrix.det_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
ι : 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
⊢ (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:
simp only [Basis.toMatrix_mul_toMatrix_flip, Matrix.transpose_one, Matrix.mul_one,
          Matrix.det_one]

Premises used: Module.Basis.toMatrix_mul_toMatrix_flip, Matrix.transpose_one, Matrix.det_one, Matrix.mul_one
-- 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 : 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
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
⊢ (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:
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]

Premises used: HMul.hMul, Module.Basis.toMatrix, PowerBasis.basis, Matrix.transpose, DFunLike.coe, Matrix.det
-- 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 : 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 (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:
simpa only [traceMatrix_of_basis] using det_traceMatrix_ne_zero' pb

Premises used: Algebra.traceMatrix_of_basis, det_traceMatrix_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
⊢ BilinForm.Nondegenerate (traceForm K L)

Tactic:
BilinForm.nondegenerate_of_det_ne_zero (traceForm K L) _
    (det_traceForm_ne_zero (Module.finBasis K L))

Premises used: Module.finBasis, LinearMap.BilinForm.nondegenerate_of_det_ne_zero, Algebra.traceForm, det_traceForm_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
⊢ 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
⊢ BilinForm.Nondegenerate (traceForm K L)

Tactic:
3

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
⊢ ∀ (a : Algebra.IsSeparable K L), BilinForm.Nondegenerate (traceForm K L)

Tactic:
1 → 3

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
⊢ ∀ (a : Algebra.IsSeparable K L), BilinForm.Nondegenerate (traceForm K L)

Tactic:
tfae_have 1 → 3 := fun _ ↦ traceForm_nondegenerate K L
-- 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)
⊢ BilinForm.Nondegenerate (traceForm K L)

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false