-- Mathlib/RingTheory/Norm/Basic.lean
theorem norm_eq_norm_adjoin [FiniteDimensional K L] [Algebra.IsSeparable K L] (x : L) :
    norm K x = norm K (AdjoinSimple.gen K x) ^ finrank K⟮x⟯ 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
x : L
this : Algebra.IsSeparable (↥K⟮x⟯) L := isSeparable_tower_top_of_isSeparable K (↥K⟮x⟯) L
pbL : PowerBasis (↥K⟮x⟯) L := Field.powerBasisOfFiniteOfSeparable (↥K⟮x⟯) L
⊢ (norm K) x = (norm K) (AdjoinSimple.gen K x) ^ finrank (↥K⟮x⟯) L

Tactic:
let pbx := IntermediateField.adjoin.powerBasis (Algebra.IsSeparable.isIntegral K x)

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
x : L
this : Algebra.IsSeparable (↥K⟮x⟯) L := isSeparable_tower_top_of_isSeparable K (↥K⟮x⟯) L
pbL : PowerBasis (↥K⟮x⟯) L := Field.powerBasisOfFiniteOfSeparable (↥K⟮x⟯) L
pbx : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis ⋯
⊢ (norm K) x = (norm K) (AdjoinSimple.gen K x) ^ finrank (↥K⟮x⟯) 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
x : L
this : Algebra.IsSeparable (↥K⟮x⟯) L := isSeparable_tower_top_of_isSeparable K (↥K⟮x⟯) L
⊢ (norm K) x = (norm K) (AdjoinSimple.gen K x) ^ finrank (↥K⟮x⟯) L

Tactic:
let pbL := Field.powerBasisOfFiniteOfSeparable K⟮x⟯ L

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
x : L
this : Algebra.IsSeparable (↥K⟮x⟯) L := isSeparable_tower_top_of_isSeparable K (↥K⟮x⟯) L
pbL : PowerBasis (↥K⟮x⟯) L := Field.powerBasisOfFiniteOfSeparable (↥K⟮x⟯) L
⊢ (norm K) x = (norm K) (AdjoinSimple.gen K x) ^ finrank (↥K⟮x⟯) L

Proof state:
case e_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
x : L
this : Algebra.IsSeparable (↥K⟮x⟯) L := isSeparable_tower_top_of_isSeparable K (↥K⟮x⟯) L
pbL : PowerBasis (↥K⟮x⟯) L := Field.powerBasisOfFiniteOfSeparable (↥K⟮x⟯) L
pbx : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis ⋯
⊢ pbL.dim = finrank (↥K⟮(algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)⟯) L

Tactic:
rw [← PowerBasis.finrank, AdjoinSimple.algebraMap_gen K x]

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
x : L
this : Algebra.IsSeparable (↥K⟮x⟯) L := isSeparable_tower_top_of_isSeparable K (↥K⟮x⟯) L
pbL : PowerBasis (↥K⟮x⟯) L := Field.powerBasisOfFiniteOfSeparable (↥K⟮x⟯) L
pbx : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis ⋯
⊢ (norm K) x = (norm K) (AdjoinSimple.gen K x) ^ finrank (↥K⟮x⟯) L

Tactic:
erw [← AdjoinSimple.algebraMap_gen K x, norm_eq_matrix_det (pbx.basis.smulTower pbL.basis) _,
  smulTower_leftMulMatrix_algebraMap, det_blockDiagonal, norm_eq_matrix_det pbx.basis]

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
x : L
this : Algebra.IsSeparable (↥K⟮x⟯) L := isSeparable_tower_top_of_isSeparable K (↥K⟮x⟯) L
pbL : PowerBasis (↥K⟮x⟯) L := Field.powerBasisOfFiniteOfSeparable (↥K⟮x⟯) L
pbx : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis ⋯
⊢ ∏ k : Fin pbL.dim, ((leftMulMatrix pbx.basis) (AdjoinSimple.gen K x)).det =
    ((leftMulMatrix pbx.basis) (AdjoinSimple.gen K ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)))).det ^
      finrank (↥K⟮(algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)⟯) 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
x : L
this : Algebra.IsSeparable (↥K⟮x⟯) L := isSeparable_tower_top_of_isSeparable K (↥K⟮x⟯) L
pbL : PowerBasis (↥K⟮x⟯) L := Field.powerBasisOfFiniteOfSeparable (↥K⟮x⟯) L
pbx : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis ⋯
⊢ ((leftMulMatrix pbx.basis) (AdjoinSimple.gen K x)).det ^ pbL.dim =
    ((leftMulMatrix pbx.basis) (AdjoinSimple.gen K ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)))).det ^
      finrank (↥K⟮(algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)⟯) L

Tactic:
congr

Result:
case e_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
x : L
this : Algebra.IsSeparable (↥K⟮x⟯) L := isSeparable_tower_top_of_isSeparable K (↥K⟮x⟯) L
pbL : PowerBasis (↥K⟮x⟯) L := Field.powerBasisOfFiniteOfSeparable (↥K⟮x⟯) L
pbx : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis ⋯
⊢ pbL.dim = finrank (↥K⟮(algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)⟯) 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
x : L
this : Algebra.IsSeparable (↥K⟮x⟯) L := isSeparable_tower_top_of_isSeparable K (↥K⟮x⟯) L
pbL : PowerBasis (↥K⟮x⟯) L := Field.powerBasisOfFiniteOfSeparable (↥K⟮x⟯) L
pbx : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis ⋯
⊢ ∏ k : Fin pbL.dim, ((leftMulMatrix pbx.basis) (AdjoinSimple.gen K x)).det =
    ((leftMulMatrix pbx.basis) (AdjoinSimple.gen K ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)))).det ^
      finrank (↥K⟮(algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)⟯) L

Tactic:
simp only [Finset.card_fin, Finset.prod_const]

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
x : L
this : Algebra.IsSeparable (↥K⟮x⟯) L := isSeparable_tower_top_of_isSeparable K (↥K⟮x⟯) L
pbL : PowerBasis (↥K⟮x⟯) L := Field.powerBasisOfFiniteOfSeparable (↥K⟮x⟯) L
pbx : PowerBasis K ↥K⟮x⟯ := adjoin.powerBasis ⋯
⊢ ((leftMulMatrix pbx.basis) (AdjoinSimple.gen K x)).det ^ pbL.dim =
    ((leftMulMatrix pbx.basis) (AdjoinSimple.gen K ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)))).det ^
      finrank (↥K⟮(algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)⟯) 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
x : L
⊢ (norm K) x = (norm K) (AdjoinSimple.gen K x) ^ finrank (↥K⟮x⟯) L

Tactic:
letI := Algebra.isSeparable_tower_top_of_isSeparable K K⟮x⟯ L

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
x : L
this : Algebra.IsSeparable (↥K⟮x⟯) L := isSeparable_tower_top_of_isSeparable K (↥K⟮x⟯) L
⊢ (norm K) x = (norm K) (AdjoinSimple.gen K x) ^ finrank (↥K⟮x⟯) L