awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
E : Type z
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Module.Finite K L
inst_6 : IsAlgClosed E
pb : PowerBasis K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst_7 : Algebra.IsSeparable K L
e_f :
  ∀ (i : Fin pb.dim),
    HPow.hPow (α := E) (β := ℕ)
        (∏ j ∈ Ioi i,
          HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
            ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
        2 =
      ∏ j ∈ Ioi i,
        HPow.hPow (β := ℕ)
          (HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
            ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
          2
⊢ Eq.{z + 1} (α := Fin pb.dim → E)
    (fun (x : Fin pb.dim) ↦
      HPow.hPow (α := E) (β := ℕ)
        (∏ j ∈ Ioi x,
          HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
            ((((e : (a : Fin pb.dim) → L →ₐ[K] E) x : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
        2)
    fun (i : Fin pb.dim) ↦
    ∏ j ∈ Ioi i,
      HPow.hPow (β := ℕ)
        (HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
          ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
        2

Tactic:
ext i
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
E : Type z
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Module.Finite K L
inst_6 : IsAlgClosed E
pb : PowerBasis K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst_7 : Algebra.IsSeparable K L
i : Fin pb.dim
e_f e_f₁ :
  Eq.{z + 1} (α := E)
    (∏ x ∈ Ioi i,
      HPow.hPow (β := ℕ)
        (HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) x : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
          ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
        2)
    (∏ j ∈ Ioi i,
      HPow.hPow (β := ℕ)
        (HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
          ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
        2)
⊢ HPow.hPow (α := E) (β := ℕ)
      (∏ j ∈ Ioi i,
        HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
          ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
      2 =
    ∏ j ∈ Ioi i,
      HPow.hPow (β := ℕ)
        (HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
          ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
        2

Tactic:
rw [← prod_pow]

Premises used: Finset.prod_pow
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
E : Type z
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Module.Finite K L
inst_6 : IsAlgClosed E
pb : PowerBasis K L
inst_7 : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
rw :
  Eq.{z + 1} (α := E)
    (∏ i : Fin pb.dim,
      ∏ j ∈ Ioi i,
        HPow.hPow (β := ℕ)
          (HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
            ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
          2)
    (∏ i : Fin pb.dim,
      ∏ j ∈ Ioi i,
        -(HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E) *
            HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)))
⊢ Eq.{z + 1} (α := E)
    ((algebraMap K E : (a : K) → E) (discr.{u, v, 0} (ι := Fin pb.dim) K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L)) :
      E)
    (∏ i : Fin pb.dim,
        ∏ j ∈ Ioi i,
          -(HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
                ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E) *
              HSub.hSub (α := E) (β := E)
                ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
                ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)) :
      E)

Tactic:
rw [discr_powerBasis_eq_prod _ _ _ e]

Premises used: Algebra.discr_powerBasis_eq_prod
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
E : Type z
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Module.Finite K L
inst_6 : IsAlgClosed E
pb : PowerBasis K L
inst_7 : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
e_f :
  Eq.{z + 1} (α := Fin pb.dim → E)
    (fun (i : Fin pb.dim) ↦
      ∏ j ∈ Ioi i,
        HPow.hPow (β := ℕ)
          (HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
            ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
          2)
    fun (i : Fin pb.dim) ↦
    ∏ j ∈ Ioi i,
      -(HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
            ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E) *
          HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
            ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
⊢ Eq.{z + 1} (α := E)
    (∏ i : Fin pb.dim,
      ∏ j ∈ Ioi i,
        HPow.hPow (β := ℕ)
          (HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
            ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
          2)
    (∏ i : Fin pb.dim,
      ∏ j ∈ Ioi i,
        -(HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E) *
            HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)))

Tactic:
congr
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
E : Type z
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Module.Finite K L
inst_6 : IsAlgClosed E
pb : PowerBasis K L
inst_7 : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
e_f :
  ∀ (i : Fin pb.dim),
    Eq.{z + 1} (α := E)
      (∏ j ∈ Ioi i,
        HPow.hPow (β := ℕ)
          (HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
            ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
          2)
      (∏ j ∈ Ioi i,
        -(HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E) *
            HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)))
⊢ Eq.{z + 1} (α := Fin pb.dim → E)
    (fun (i : Fin pb.dim) ↦
      ∏ j ∈ Ioi i,
        HPow.hPow (β := ℕ)
          (HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
            ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
          2)
    fun (i : Fin pb.dim) ↦
    ∏ j ∈ Ioi i,
      -(HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
            ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E) *
          HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
            ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E))

Tactic:
ext i
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
E : Type z
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Module.Finite K L
inst_6 : IsAlgClosed E
pb : PowerBasis K L
inst_7 : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
i : Fin pb.dim
e_f :
  Eq.{z + 1} (α := Fin pb.dim → E)
    (fun (j : Fin pb.dim) ↦
      HPow.hPow (β := ℕ)
        (HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
          ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
        2)
    fun (j : Fin pb.dim) ↦
    -(HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
          ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E) *
        HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
          ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
⊢ Eq.{z + 1} (α := E)
    (∏ j ∈ Ioi i,
      HPow.hPow (β := ℕ)
        (HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
          ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
        2)
    (∏ j ∈ Ioi i,
      -(HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
            ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E) *
          HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
            ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)))

Tactic:
congr
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
E : Type z
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Module.Finite K L
inst_6 : IsAlgClosed E
pb : PowerBasis K L
inst_7 : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
i : Fin pb.dim
e_f :
  ∀ (j : Fin pb.dim),
    HPow.hPow (β := ℕ)
        (HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
          ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
        2 =
      -(HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
            ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E) *
          HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
            ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
⊢ Eq.{z + 1} (α := Fin pb.dim → E)
    (fun (j : Fin pb.dim) ↦
      HPow.hPow (β := ℕ)
        (HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
          ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
        2)
    fun (j : Fin pb.dim) ↦
    -(HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
          ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E) *
        HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
          ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E))

Tactic:
ext j
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
E : Type z
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Module.Finite K L
inst_6 : IsAlgClosed E
pb : PowerBasis K L
inst_7 : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
i j : Fin pb.dim
⊢ HPow.hPow (β := ℕ)
      (HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
        ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
      2 =
    -(HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
          ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E) *
        HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
          ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E))

Tactic:
ring
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
E : Type z
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Module.Finite K L
inst_6 : IsAlgClosed E
pb : PowerBasis K L
inst_7 : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
rw :
  ∏ i : Fin pb.dim,
      ∏ j ∈ Ioi i,
        -(HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E) *
            HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)) =
    HPow.hPow (α := E) (-1) (n * (n - 1) / 2) *
      ∏ i : Fin pb.dim,
        ∏ j ∈ Ioi i,
          HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E) *
            HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
⊢ (algebraMap K E : (a : K) → E) (discr.{u, v, 0} (ι := Fin pb.dim) K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L)) =
    HPow.hPow (α := E) (-1) (n * (n - 1) / 2) *
      ∏ i : Fin pb.dim,
        ∏ j ∈ Ioi i,
          HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E) *
            HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)

Tactic:
rw [discr_powerBasis_eq_prod' _ _ _ e]

Premises used: Algebra.discr_powerBasis_eq_prod'
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
E : Type z
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Module.Finite K L
inst_6 : IsAlgClosed E
pb : PowerBasis K L
inst_7 : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
simp_rw :
  (∏ x : Fin pb.dim, ∏ x ∈ Ioi x, -1) *
      HMul.hMul (α := E)
        (∏ x : Fin pb.dim,
          ∏ x_1 ∈ Ioi x,
            HSub.hSub (α := E) (β := E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) x_1 : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) x : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
        (∏ x : Fin pb.dim,
          ∏ x_1 ∈ Ioi x,
            HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) x : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) x_1 : L →ₐ[K] E) : (a : L) → E) pb.gen : E)) =
    HPow.hPow (α := E) (-1) (n * (n - 1) / 2) *
      HMul.hMul (α := E)
        (∏ x : Fin pb.dim,
          ∏ x_1 ∈ Ioi x,
            HSub.hSub (α := E) (β := E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) x_1 : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) x : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
        (∏ x : Fin pb.dim,
          ∏ x_1 ∈ Ioi x,
            HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) x : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) x_1 : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
⊢ ∏ i : Fin pb.dim,
      ∏ j ∈ Ioi i,
        -(HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E) *
            HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)) =
    HPow.hPow (α := E) (-1) (n * (n - 1) / 2) *
      ∏ i : Fin pb.dim,
        ∏ j ∈ Ioi i,
          HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E) *
            HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)

Tactic:
simp_rw [fun i j => neg_eq_neg_one_mul ((e j pb.gen - e i pb.gen) * (e i pb.gen - e j pb.gen)),
    prod_mul_distrib]

Premises used: Finset.prod_mul_distrib, HMul.hMul, PowerBasis.gen, HSub.hSub, neg_eq_neg_one_mul, DFunLike.coe
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
E : Type z
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Module.Finite K L
inst_6 : IsAlgClosed E
pb : PowerBasis K L
inst_7 : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
e_a : ∏ x : Fin pb.dim, ∏ x ∈ Ioi x, -1 = HPow.hPow (α := E) (-1) (n * (n - 1) / 2)
⊢ (∏ x : Fin pb.dim, ∏ x ∈ Ioi x, -1) *
      HMul.hMul (α := E)
        (∏ x : Fin pb.dim,
          ∏ x_1 ∈ Ioi x,
            HSub.hSub (α := E) (β := E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) x_1 : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) x : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
        (∏ x : Fin pb.dim,
          ∏ x_1 ∈ Ioi x,
            HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) x : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) x_1 : L →ₐ[K] E) : (a : L) → E) pb.gen : E)) =
    HPow.hPow (α := E) (-1) (n * (n - 1) / 2) *
      HMul.hMul (α := E)
        (∏ x : Fin pb.dim,
          ∏ x_1 ∈ Ioi x,
            HSub.hSub (α := E) (β := E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) x_1 : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) x : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
        (∏ x : Fin pb.dim,
          ∏ x_1 ∈ Ioi x,
            HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) x : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) x_1 : L →ₐ[K] E) : (a : L) → E) pb.gen : E))

Tactic:
congr
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
E : Type z
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Module.Finite K L
inst_6 : IsAlgClosed E
pb : PowerBasis K L
inst_7 : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
e_a : HPow.hPow (α := E) (β := ℕ) (-1) (∑ i : Fin pb.dim, #(Ioi i)) = HPow.hPow (α := E) (-1) (n * (n - 1) / 2)
⊢ ∏ x : Fin pb.dim, ∏ x ∈ Ioi x, -1 = HPow.hPow (α := E) (-1) (n * (n - 1) / 2)

Tactic:
simp only [prod_pow_eq_pow_sum, prod_const]

Premises used: Finset.prod_const, Finset.prod_pow_eq_pow_sum
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
E : Type z
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Module.Finite K L
inst_6 : IsAlgClosed E
pb : PowerBasis K L
inst_7 : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
e_a : ∑ i : Fin pb.dim, #(Ioi i) = n * (n - 1) / 2
⊢ HPow.hPow (α := E) (β := ℕ) (-1) (∑ i : Fin pb.dim, #(Ioi i)) = HPow.hPow (α := E) (-1) (n * (n - 1) / 2)

Tactic:
congr
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
E : Type z
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Module.Finite K L
inst_6 : IsAlgClosed E
pb : PowerBasis K L
inst_7 : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
e_a : Eq (α := ℚ) (∑ x : Fin pb.dim, (↑(#(Ioi x)) : ℚ)) (↑(n * (n - 1) / 2) : ℚ)
⊢ ∑ i : Fin pb.dim, #(Ioi i) = n * (n - 1) / 2

Tactic:
rw [← @Nat.cast_inj ℚ, Nat.cast_sum]

Premises used: Nat.cast_inj, Nat.cast_sum
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
E : Type z
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Module.Finite K L
inst_6 : IsAlgClosed E
pb : PowerBasis K L
inst_7 : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ ∀ (x : Fin pb.dim), (↑x : ℕ) + 1 ≤ pb.dim

Tactic:
simp [Fin.is_lt]

Premises used: Fin.is_lt
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
E : Type z
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Module.Finite K L
inst_6 : IsAlgClosed E
pb : PowerBasis K L
inst_7 : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ ∀ (x : Fin pb.dim), (↑x : ℕ) + 1 ≤ pb.dim

Tactic:
have : ∀ x : Fin pb.dim, ↑x + 1 ≤ pb.dim := by simp [Fin.is_lt]
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
E : Type z
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Module.Finite K L
inst_6 : IsAlgClosed E
pb : PowerBasis K L
inst_7 : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), (↑x : ℕ) + 1 ≤ pb.dim
e_a : Eq (α := ℚ) (∑ x : Fin pb.dim, (↑(pb.dim - ((↑x : ℕ) + 1)) : ℚ)) (↑(n * (n - 1) / 2) : ℚ)
⊢ Eq (α := ℚ) (∑ x : Fin pb.dim, (↑(#(Ioi x)) : ℚ)) (↑(n * (n - 1) / 2) : ℚ)

Tactic:
simp_rw [Fin.card_Ioi, Nat.sub_sub, add_comm 1]

Premises used: Fin.card_Ioi, Nat.sub_sub, add_comm, OfNat.ofNat
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
E : Type z
inst : Field K
inst_1 : Field L
inst_2 : Field E
inst_3 : Algebra K L
inst_4 : Algebra K E
inst_5 : Module.Finite K L
inst_6 : IsAlgClosed E
pb : PowerBasis K L
inst_7 : Algebra.IsSeparable K L
e : Fin pb.dim ≃ (L →ₐ[K] E)
this : ∀ (x : Fin pb.dim), (↑x : ℕ) + 1 ≤ pb.dim
e_a :
  HMul.hMul (α := ℚ) (↑pb.dim : ℚ) (↑pb.dim : ℚ) -
      HAdd.hAdd (α := ℚ) (∑ x : Fin pb.dim, (↑(↑x : ℕ) : ℚ)) (↑pb.dim : ℚ) =
    (↑(n * (n - 1) / 2) : ℚ)
⊢ Eq (α := ℚ) (∑ x : Fin pb.dim, (↑(pb.dim - ((↑x : ℕ) + 1)) : ℚ)) (↑(n * (n - 1) / 2) : ℚ)

Tactic:
simp only [Nat.cast_sub, this, Finset.card_fin, nsmul_eq_mul, sum_const, sum_sub_distrib,
    Nat.cast_add, Nat.cast_one, sum_add_distrib, mul_one]

Premises used: Nat.cast_sub, Finset.sum_add_distrib, Nat.cast_add, Finset.sum_sub_distrib, Finset.card_fin, nsmul_eq_mul, mul_one, Nat.cast_one, Finset.sum_const