-- Mathlib/RingTheory/Discriminant.lean
theorem discr_powerBasis_eq_prod (e : Fin pb.dim ≃ (L →ₐ[K] E)) [Algebra.IsSeparable K L] :
    algebraMap K E (discr K pb.basis) =
      ∏ i : Fin pb.dim, ∏ j ∈ Ioi i, (e j pb.gen - e i pb.gen) ^ 2

Proof state:
case e_f.h
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst✝ : Algebra.IsSeparable K L
i : Fin pb.dim
⊢ (∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen)) ^ 2 = ∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen) ^ 2

Tactic:
rw [← prod_pow]

Result:
no goals

Proof state:
case e_f
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst✝ : Algebra.IsSeparable K L
⊢ (fun x => (∏ j ∈ Ioi x, ((e j) pb.gen - (e x) pb.gen)) ^ 2) = fun i => ∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen) ^ 2

Tactic:
ext i

Result:
case e_f.h
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst✝ : Algebra.IsSeparable K L
i : Fin pb.dim
⊢ (∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen)) ^ 2 = ∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen) ^ 2

Proof state:
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst✝ : Algebra.IsSeparable K L
⊢ (algebraMap K E) (discr K ⇑pb.basis) = ∏ i : Fin pb.dim, ∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen) ^ 2

Tactic:
rw [discr_eq_det_embeddingsMatrixReindex_pow_two K E pb.basis e,
  embeddingsMatrixReindex_eq_vandermonde, det_transpose, det_vandermonde, ← prod_pow]

Result:
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst✝ : Algebra.IsSeparable K L
⊢ ∏ x : Fin pb.dim, (∏ j ∈ Ioi x, ((e j) pb.gen - (e x) pb.gen)) ^ 2 =
    ∏ i : Fin pb.dim, ∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen) ^ 2

Proof state:
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst✝ : Algebra.IsSeparable K L
⊢ ∏ x : Fin pb.dim, (∏ j ∈ Ioi x, ((e j) pb.gen - (e x) pb.gen)) ^ 2 =
    ∏ i : Fin pb.dim, ∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen) ^ 2

Tactic:
congr

Result:
case e_f
K : Type u
L : Type v
E : Type z
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Field E
inst✝⁴ : Algebra K L
inst✝³ : Algebra K E
inst✝² : Module.Finite K L
inst✝¹ : IsAlgClosed E
pb : PowerBasis K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst✝ : Algebra.IsSeparable K L
⊢ (fun x => (∏ j ∈ Ioi x, ((e j) pb.gen - (e x) pb.gen)) ^ 2) = fun i => ∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen) ^ 2