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

Proof state:
case e_f.h.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
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
i j : Fin pb.dim
⊢ ((e j) pb.gen - (e i) pb.gen) ^ 2 = -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))

Tactic:
ring

Result:
no goals

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
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ (algebraMap K E) (discr K ⇑pb.basis) =
    ∏ i : Fin pb.dim, ∏ j ∈ Ioi i, -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))

Tactic:
rw [discr_powerBasis_eq_prod _ _ _ e]

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
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ ∏ i : Fin pb.dim, ∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen) ^ 2 =
    ∏ i : Fin pb.dim, ∏ j ∈ Ioi i, -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))

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
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ ∏ i : Fin pb.dim, ∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen) ^ 2 =
    ∏ i : Fin pb.dim, ∏ j ∈ Ioi i, -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))

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
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ (fun i => ∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen) ^ 2) = fun i =>
    ∏ j ∈ Ioi i, -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))

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
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
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) * ((e i) pb.gen - (e j) pb.gen))

Tactic:
congr

Result:
case e_f.h.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
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
i : Fin pb.dim
⊢ (fun j => ((e j) pb.gen - (e i) pb.gen) ^ 2) = fun j =>
    -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))

Proof state:
case e_f.h.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
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
i : Fin pb.dim
⊢ (fun j => ((e j) pb.gen - (e i) pb.gen) ^ 2) = fun j =>
    -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))

Tactic:
ext j

Result:
case e_f.h.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
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
i j : Fin pb.dim
⊢ ((e j) pb.gen - (e i) pb.gen) ^ 2 = -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))

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
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ (fun i => ∏ j ∈ Ioi i, ((e j) pb.gen - (e i) pb.gen) ^ 2) = fun i =>
    ∏ j ∈ Ioi i, -(((e j) pb.gen - (e i) pb.gen) * ((e i) pb.gen - (e j) pb.gen))

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
inst✝ : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
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) * ((e i) pb.gen - (e j) pb.gen))