awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ 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
have 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)
Tactic: rw [← prod_pow]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
⊢ 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)
have 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)))
Tactic: rw [discr_powerBasis_eq_prod _ _ _ e]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
⊢ 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)))
have 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))
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
⊢ 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))
have 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)))
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ 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)))
have 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))
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ 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))
have 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))
Tactic: ext j
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
⊢ (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)
have 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)
Tactic: rw [discr_powerBasis_eq_prod' _ _ _ e]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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,
      ∏ 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)
have 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))
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]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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 ∈ 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))
have e_a : ∏ x : Fin pb.dim, ∏ x ∈ Ioi x, -1 = HPow.hPow (α := E) (-1) (n * (n - 1) / 2)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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 ∈ Ioi x, -1 = HPow.hPow (α := E) (-1) (n * (n - 1) / 2)
have e_a : HPow.hPow (α := E) (β := ℕ) (-1) (∑ i : Fin pb.dim, #(Ioi i)) = HPow.hPow (α := E) (-1) (n * (n - 1) / 2)
Tactic: simp only [prod_pow_eq_pow_sum, prod_const]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
⊢ HPow.hPow (α := E) (β := ℕ) (-1) (∑ i : Fin pb.dim, #(Ioi i)) = HPow.hPow (α := E) (-1) (n * (n - 1) / 2)
have e_a : ∑ i : Fin pb.dim, #(Ioi i) = n * (n - 1) / 2
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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, #(Ioi i) = n * (n - 1) / 2
have e_a : Eq (α := ℚ) (∑ x : Fin pb.dim, (↑(#(Ioi x)) : ℚ)) (↑(n * (n - 1) / 2) : ℚ)
Tactic: rw [← @Nat.cast_inj ℚ, Nat.cast_sum]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (hypothesis)
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)
⊢ Eq (α := ℚ) (∑ x : Fin pb.dim, (↑(#(Ioi x)) : ℚ)) (↑(n * (n - 1) / 2) : ℚ)
have this : ∀ (x : Fin pb.dim), (↑x : ℕ) + 1 ≤ pb.dim
Tactic: have : ∀ x : Fin pb.dim, ↑x + 1 ≤ pb.dim := by simp [Fin.is_lt]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ Eq (α := ℚ) (∑ x : Fin pb.dim, (↑(#(Ioi x)) : ℚ)) (↑(n * (n - 1) / 2) : ℚ)
have e_a : Eq (α := ℚ) (∑ x : Fin pb.dim, (↑(pb.dim - ((↑x : ℕ) + 1)) : ℚ)) (↑(n * (n - 1) / 2) : ℚ)
Tactic: simp_rw [Fin.card_Ioi, Nat.sub_sub, add_comm 1]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ Eq (α := ℚ) (∑ x : Fin pb.dim, (↑(pb.dim - ((↑x : ℕ) + 1)) : ℚ)) (↑(n * (n - 1) / 2) : ℚ)
have e_a : HMul.hMul (α := ℚ) (↑pb.dim : ℚ) (↑pb.dim : ℚ) - HAdd.hAdd (α := ℚ) (∑ x : Fin pb.dim, (↑(↑x : ℕ) : ℚ)) (↑pb.dim : ℚ) =
  (↑(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]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ HMul.hMul (α := ℚ) (↑pb.dim : ℚ) (↑pb.dim : ℚ) -
      HAdd.hAdd (α := ℚ) (∑ x : Fin pb.dim, (↑(↑x : ℕ) : ℚ)) (↑pb.dim : ℚ) =
    (↑(n * (n - 1) / 2) : ℚ)
have e_a : HMul.hMul (α := ℚ) (↑pb.dim : ℚ) (↑pb.dim : ℚ) - HAdd.hAdd (α := ℚ) (↑(pb.dim * (pb.dim - 1) / 2) : ℚ) (↑pb.dim : ℚ) =
  (↑(n * (n - 1) / 2) : ℚ)
Tactic: rw [← Nat.cast_sum, ← @Finset.sum_range ℕ _ pb.dim fun i => i, sum_range_id]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ n = pb.dim
have rw : Fintype.card (L →ₐ[K] E) = Fintype.card (Fin pb.dim)
Tactic: rw [← AlgHom.card K L E, ← Fintype.card_fin pb.dim]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (hypothesis)
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
⊢ HMul.hMul (α := ℚ) (↑pb.dim : ℚ) (↑pb.dim : ℚ) - HAdd.hAdd (α := ℚ) (↑(pb.dim * (pb.dim - 1) / 2) : ℚ) (↑pb.dim : ℚ) =
    (↑(n * (n - 1) / 2) : ℚ)
have hn : n = pb.dim
Tactic: have hn : n = pb.dim := by
    rw [← AlgHom.card K L E, ← Fintype.card_fin pb.dim]
    -- FIXME: Without the `Fintype` namespace, why does it complain about `Finset.card_congr` being
    -- deprecated?
    exact Fintype.card_congr e.symm
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (hypothesis)
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
hn : n = pb.dim
⊢ HMul.hMul (α := ℚ) (↑pb.dim : ℚ) (↑pb.dim : ℚ) - HAdd.hAdd (α := ℚ) (↑(pb.dim * (pb.dim - 1) / 2) : ℚ) (↑pb.dim : ℚ) =
    (↑(n * (n - 1) / 2) : ℚ)
have h₂ : 2 ∣ pb.dim * (pb.dim - 1)
Tactic: have h₂ : 2 ∣ pb.dim * (pb.dim - 1) := pb.dim.even_mul_pred_self.two_dvd
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (hypothesis)
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
hn : n = pb.dim
h₂ : 2 ∣ pb.dim * (pb.dim - 1)
⊢ HMul.hMul (α := ℚ) (↑pb.dim : ℚ) (↑pb.dim : ℚ) - HAdd.hAdd (α := ℚ) (↑(pb.dim * (pb.dim - 1) / 2) : ℚ) (↑pb.dim : ℚ) =
    (↑(n * (n - 1) / 2) : ℚ)
have hne : Ne (α := ℚ) (↑2 : ℚ) 0
Tactic: have hne : ((2 : ℕ) : ℚ) ≠ 0 := by simp
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
hn : n = pb.dim
h₂ : 2 ∣ pb.dim * (pb.dim - 1)
hne : Ne (α := ℚ) (↑2 : ℚ) 0
⊢ 1 ≤ pb.dim
have rw : Nontrivial L
Tactic: rw [← hn, Nat.one_le_iff_ne_zero, ← zero_lt_iff, Module.finrank_pos_iff]