-- Mathlib/RingTheory/Trace/Basic.lean
theorem det_traceForm_ne_zero [Algebra.IsSeparable K L] [DecidableEq ι] (b : Basis ι K L) :
    det (BilinForm.toMatrix b (traceForm K L)) ≠ 0

Proof state:
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Fintype ι
inst✝¹ : Algebra.IsSeparable K L
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ b.toMatrix ⇑pb.basis * pb.basis.toMatrix ⇑b = 1

Tactic:
apply Basis.toMatrix_mul_toMatrix_flip

Result:
no goals

Proof state:
case refine_1
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Fintype ι
inst✝¹ : Algebra.IsSeparable K L
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ (pb.basis.toMatrix ⇑b * (pb.basis.toMatrix ⇑b)ᵀ).det * ((b.toMatrix ⇑pb.basis)ᵀ * b.toMatrix ⇑pb.basis).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]

Result:
no goals

Proof state:
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Fintype ι
inst✝¹ : Algebra.IsSeparable K L
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
⊢ ((BilinForm.toMatrix b) (traceForm K L)).det ≠ 0

Tactic:
let pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable _ _

Result:
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Fintype ι
inst✝¹ : Algebra.IsSeparable K L
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ ((BilinForm.toMatrix b) (traceForm K L)).det ≠ 0

Proof state:
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Fintype ι
inst✝¹ : Algebra.IsSeparable K L
inst✝ : DecidableEq ι
b : Basis ι K L
⊢ ((BilinForm.toMatrix b) (traceForm K L)).det ≠ 0

Tactic:
haveI : FiniteDimensional K L := FiniteDimensional.of_fintype_basis b

Result:
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Fintype ι
inst✝¹ : Algebra.IsSeparable K L
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
⊢ ((BilinForm.toMatrix b) (traceForm K L)).det ≠ 0

Proof state:
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Fintype ι
inst✝¹ : Algebra.IsSeparable K L
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ (pb.basis.toMatrix ⇑b * (pb.basis.toMatrix ⇑b)ᵀ).det * ((BilinForm.toMatrix pb.basis) (traceForm K L)).det ≠ 0

K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Fintype ι
inst✝¹ : Algebra.IsSeparable K L
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ b.toMatrix ⇑pb.basis * pb.basis.toMatrix ⇑b = 1

Tactic:
swap

Result:
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Fintype ι
inst✝¹ : Algebra.IsSeparable K L
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ b.toMatrix ⇑pb.basis * pb.basis.toMatrix ⇑b = 1

K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Fintype ι
inst✝¹ : Algebra.IsSeparable K L
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ (pb.basis.toMatrix ⇑b * (pb.basis.toMatrix ⇑b)ᵀ).det * ((BilinForm.toMatrix pb.basis) (traceForm K L)).det ≠ 0

Proof state:
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Fintype ι
inst✝¹ : Algebra.IsSeparable K L
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ (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

Tactic:
simp only [← det_mul, Matrix.mul_assoc, Matrix.transpose_mul]

Result:
no goals

Proof state:
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Fintype ι
inst✝¹ : Algebra.IsSeparable K L
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ ((BilinForm.toMatrix b) (traceForm K L)).det ≠ 0

Tactic:
rw [← BilinForm.toMatrix_mul_basis_toMatrix pb.basis b, ←
  det_comm' (pb.basis.toMatrix_mul_toMatrix_flip b) _, ← Matrix.mul_assoc, det_mul]

Result:
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Fintype ι
inst✝¹ : Algebra.IsSeparable K L
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ (pb.basis.toMatrix ⇑b * (pb.basis.toMatrix ⇑b)ᵀ).det * ((BilinForm.toMatrix pb.basis) (traceForm K L)).det ≠ 0

K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Fintype ι
inst✝¹ : Algebra.IsSeparable K L
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ b.toMatrix ⇑pb.basis * pb.basis.toMatrix ⇑b = 1

Proof state:
case refine_2
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Fintype ι
inst✝¹ : Algebra.IsSeparable K L
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ ((BilinForm.toMatrix pb.basis) (traceForm K L)).det ≠ 0

Tactic:
simpa only [traceMatrix_of_basis] using det_traceMatrix_ne_zero' pb

Result:
no goals

Proof state:
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Fintype ι
inst✝¹ : Algebra.IsSeparable K L
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ (pb.basis.toMatrix ⇑b * (pb.basis.toMatrix ⇑b)ᵀ).det * ((BilinForm.toMatrix pb.basis) (traceForm K L)).det ≠ 0

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

Result:
case refine_1
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Fintype ι
inst✝¹ : Algebra.IsSeparable K L
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ (pb.basis.toMatrix ⇑b * (pb.basis.toMatrix ⇑b)ᵀ).det * ((b.toMatrix ⇑pb.basis)ᵀ * b.toMatrix ⇑pb.basis).det = 1

case refine_2
K : Type u_4
L : Type u_5
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
ι : Type w
inst✝² : Fintype ι
inst✝¹ : Algebra.IsSeparable K L
inst✝ : DecidableEq ι
b : Basis ι K L
this : FiniteDimensional K L
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ ((BilinForm.toMatrix pb.basis) (traceForm K L)).det ≠ 0