-- Mathlib/RingTheory/Trace/Basic.lean
theorem det_traceMatrix_ne_zero' [Algebra.IsSeparable K L] : det (traceMatrix K pb.basis) ≠ 0

Proof state:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
⊢ (algebraMap K (AlgebraicClosure L)) (traceMatrix K ⇑pb.basis).det ≠ 0

Tactic:
haveI : FiniteDimensional K L := pb.finite

Result:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
⊢ (algebraMap K (AlgebraicClosure 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
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
⊢ (traceMatrix K ⇑pb.basis).det ≠ 0

Tactic:
suffices algebraMap K (AlgebraicClosure L) (det (traceMatrix K pb.basis)) ≠ 0 by
  refine mt (fun ht => ?_) this
  rw [ht, RingHom.map_zero]

Result:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
⊢ (algebraMap K (AlgebraicClosure L)) (traceMatrix K ⇑pb.basis).det ≠ 0

Proof state:
case refine_2
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?refine_1).symm
⊢ ∀ (x : Fin pb.dim), ¬(x ∈ Finset.univ ∧ ∃ a ∈ Finset.Ioi x, (e a) pb.gen = (e x) pb.gen)

Tactic:
rintro i ⟨_, j, hij, h⟩

Result:
case refine_2.intro.intro.intro
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?refine_1).symm
i : Fin pb.dim
left✝ : i ∈ Finset.univ
j : Fin pb.dim
hij : j ∈ Finset.Ioi i
h : (e j) pb.gen = (e i) pb.gen
⊢ False

Proof state:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
⊢ (algebraMap K (AlgebraicClosure L)) (traceMatrix K ⇑pb.basis).det ≠ 0

Tactic:
let e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?_).symm

Result:
case refine_2
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?refine_1).symm
⊢ (algebraMap K (AlgebraicClosure L)) (traceMatrix K ⇑pb.basis).det ≠ 0

case refine_1
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
⊢ Fintype.card (L →ₐ[K] AlgebraicClosure L) = pb.dim

Proof state:
case refine_2.intro.intro.intro
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?refine_1).symm
i : Fin pb.dim
left✝ : i ∈ Finset.univ
j : Fin pb.dim
hij : j ∈ Finset.Ioi i
h : (e j) pb.gen = (e i) pb.gen
⊢ False

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

Result:
no goals

Proof state:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : (algebraMap K (AlgebraicClosure L)) (traceMatrix K ⇑pb.basis).det ≠ 0
⊢ (traceMatrix K ⇑pb.basis).det ≠ 0

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

Result:
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : (algebraMap K (AlgebraicClosure L)) (traceMatrix K ⇑pb.basis).det ≠ 0
ht : (traceMatrix K ⇑pb.basis).det = 0
⊢ (algebraMap K (AlgebraicClosure 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
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : (algebraMap K (AlgebraicClosure L)) (traceMatrix K ⇑pb.basis).det ≠ 0
ht : (traceMatrix K ⇑pb.basis).det = 0
⊢ (algebraMap K (AlgebraicClosure L)) (traceMatrix K ⇑pb.basis).det = 0

Tactic:
rw [ht, RingHom.map_zero]

Result:
no goals

Proof state:
case refine_2
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?refine_1).symm
⊢ (vandermonde fun i => (e i) pb.gen).det * (vandermonde fun i => (e i) pb.gen)ᵀᵀ.det ≠ 0

Tactic:
refine mt mul_self_eq_zero.mp ?_

Result:
case refine_2
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?refine_1).symm
⊢ ¬(vandermonde fun i => (e i) pb.gen).det = 0

Proof state:
case refine_2
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?refine_1).symm
⊢ ¬(vandermonde fun i => (e i) pb.gen).det = 0

Tactic:
simp only [det_vandermonde, Finset.prod_eq_zero_iff, not_exists, sub_eq_zero]

Result:
case refine_2
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?refine_1).symm
⊢ ∀ (x : Fin pb.dim), ¬(x ∈ Finset.univ ∧ ∃ a ∈ Finset.Ioi x, (e a) pb.gen = (e x) pb.gen)

Proof state:
case refine_2
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?refine_1).symm
⊢ (algebraMap K (AlgebraicClosure L)) (traceMatrix K ⇑pb.basis).det ≠ 0

Tactic:
rw [RingHom.map_det, RingHom.mapMatrix_apply,
  traceMatrix_eq_embeddingsMatrixReindex_mul_trans K _ _ e,
  embeddingsMatrixReindex_eq_vandermonde, det_mul, det_transpose]

Result:
case refine_2
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?refine_1).symm
⊢ (vandermonde fun i => (e i) pb.gen).det * (vandermonde fun i => (e i) pb.gen)ᵀᵀ.det ≠ 0

Proof state:
case refine_1
K : Type u_4
L : Type u_5
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
pb : PowerBasis K L
inst✝ : Algebra.IsSeparable K L
this : FiniteDimensional K L
⊢ Fintype.card (L →ₐ[K] AlgebraicClosure L) = pb.dim

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

Result:
no goals