-- Mathlib/RingTheory/Trace/Basic.lean
theorem Algebra.trace_ne_zero [FiniteDimensional K L] [Algebra.IsSeparable K L] :
    Algebra.trace K L ≠ 0

Proof state:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
e : trace K L = 0
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ Nonempty (Fin pb.dim)

Tactic:
rw [← pb.finrank, ← Fin.pos_iff_nonempty]

Result:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
e : trace K L = 0
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ 0 < finrank K L

Proof state:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
⊢ trace K L ≠ 0

Tactic:
intro e

Result:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
e : trace K L = 0
⊢ False

Proof state:
case a
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
e : trace K L = 0
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
i✝ j✝ : Fin pb.dim
⊢ traceMatrix K (⇑pb.basis) i✝ j✝ = 0 i✝ j✝

Tactic:
simp [e]

Result:
no goals

Proof state:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
e : trace K L = 0
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ (traceMatrix K ⇑pb.basis).det = 0

Tactic:
rw [show traceMatrix K pb.basis = 0 by ext; simp [e], Matrix.det_zero]

Result:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
e : trace K L = 0
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ Nonempty (Fin pb.dim)

Proof state:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
e : trace K L = 0
⊢ False

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
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
e : trace K L = 0
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ False

Proof state:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
e : trace K L = 0
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ False

Tactic:
apply det_traceMatrix_ne_zero' pb

Result:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
e : trace K L = 0
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ (traceMatrix K ⇑pb.basis).det = 0

Proof state:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
e : trace K L = 0
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ traceMatrix K ⇑pb.basis = 0

Tactic:
ext

Result:
case a
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
e : trace K L = 0
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
i✝ j✝ : Fin pb.dim
⊢ traceMatrix K (⇑pb.basis) i✝ j✝ = 0 i✝ j✝

Proof state:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : Algebra.IsSeparable K L
e : trace K L = 0
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
⊢ 0 < finrank K L

Tactic:
exact finrank_pos

Result:
no goals