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
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 (α := ℚ) (↑(pb.dim * (pb.dim - 1) / 2) : ℚ) (↑pb.dim : ℚ) =
    (↑(n * (n - 1) / 2) : ℚ)
⊢ HMul.hMul (α := ℚ) (↑pb.dim : ℚ) (↑pb.dim : ℚ) -
      HAdd.hAdd (α := ℚ) (∑ x : Fin pb.dim, (↑(↑x : ℕ) : ℚ)) (↑pb.dim : ℚ) =
    (↑(n * (n - 1) / 2) : ℚ)

Tactic:
rw [← Nat.cast_sum, ← @Finset.sum_range ℕ _ pb.dim fun i => i, sum_range_id]

Premises used: Finset.sum_range, Nat.cast_sum, Finset.sum_range_id
-- 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
rw : Fintype.card (L →ₐ[K] E) = Fintype.card (Fin pb.dim)
⊢ n = pb.dim

Tactic:
rw [← AlgHom.card K L E, ← Fintype.card_fin pb.dim]

Premises used: Fintype.card_fin, PowerBasis.dim, AlgHom.card
-- 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
⊢ Fintype.card (L →ₐ[K] E) = Fintype.card (Fin pb.dim)

Tactic:
Fintype.card_congr e.symm

Premises used: Fintype.card_congr, Equiv.symm
-- 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
⊢ Fintype.card (L →ₐ[K] E) = Fintype.card (Fin pb.dim)

Tactic:
exact Fintype.card_congr e.symm

Premises used: Fintype.card_congr, Equiv.symm
-- 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
⊢ 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
-- 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
hn : n = pb.dim
⊢ 2 ∣ pb.dim * (pb.dim - 1)

Tactic:
have h₂ : 2 ∣ pb.dim * (pb.dim - 1) := pb.dim.even_mul_pred_self.two_dvd
-- 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
hn : n = pb.dim
h₂ : 2 ∣ pb.dim * (pb.dim - 1)
⊢ Ne (α := ℚ) (↑2 : ℚ) 0

Tactic:
simp
-- 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
hn : n = pb.dim
h₂ : 2 ∣ pb.dim * (pb.dim - 1)
⊢ Ne (α := ℚ) (↑2 : ℚ) 0

Tactic:
have hne : ((2 : ℕ) : ℚ) ≠ 0 := by simp
-- 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
hn : n = pb.dim
h₂ : 2 ∣ pb.dim * (pb.dim - 1)
hne : Ne (α := ℚ) (↑2 : ℚ) 0
rw : Nontrivial L
⊢ 1 ≤ pb.dim

Tactic:
rw [← hn, Nat.one_le_iff_ne_zero, ← zero_lt_iff, Module.finrank_pos_iff]

Premises used: Module.finrank_pos_iff, Nat.one_le_iff_ne_zero, zero_lt_iff
-- 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
hn : n = pb.dim
h₂ : 2 ∣ pb.dim * (pb.dim - 1)
hne : Ne (α := ℚ) (↑2 : ℚ) 0
⊢ Nontrivial L

Tactic:
infer_instance
-- 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
hn : n = pb.dim
h₂ : 2 ∣ pb.dim * (pb.dim - 1)
hne : Ne (α := ℚ) (↑2 : ℚ) 0
⊢ 1 ≤ pb.dim

Tactic:
have hle : 1 ≤ pb.dim := by
    rw [← hn, Nat.one_le_iff_ne_zero, ← zero_lt_iff, Module.finrank_pos_iff]
    infer_instance
-- 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
hn : n = pb.dim
h₂ : 2 ∣ pb.dim * (pb.dim - 1)
hne : Ne (α := ℚ) (↑2 : ℚ) 0
hle : 1 ≤ pb.dim
e_a :
  HMul.hMul (α := ℚ) (↑pb.dim : ℚ) (↑pb.dim : ℚ) -
      ((↑pb.dim : ℚ) * HSub.hSub (α := ℚ) (↑pb.dim : ℚ) (↑1 : ℚ) / (↑2 : ℚ) + (↑pb.dim : ℚ)) =
    (↑pb.dim : ℚ) * HSub.hSub (α := ℚ) (↑pb.dim : ℚ) (↑1 : ℚ) / (↑2 : ℚ)
⊢ HMul.hMul (α := ℚ) (↑pb.dim : ℚ) (↑pb.dim : ℚ) - HAdd.hAdd (α := ℚ) (↑(pb.dim * (pb.dim - 1) / 2) : ℚ) (↑pb.dim : ℚ) =
    (↑(n * (n - 1) / 2) : ℚ)

Tactic:
rw [hn, Nat.cast_div h₂ hne, Nat.cast_mul, Nat.cast_sub hle]

Premises used: Nat.cast_sub, Nat.cast_div, Nat.cast_mul
-- 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
hn : n = pb.dim
h₂ : 2 ∣ pb.dim * (pb.dim - 1)
hne : Ne (α := ℚ) (↑2 : ℚ) 0
hle : 1 ≤ pb.dim
⊢ HMul.hMul (α := ℚ) (↑pb.dim : ℚ) (↑pb.dim : ℚ) -
      ((↑pb.dim : ℚ) * HSub.hSub (α := ℚ) (↑pb.dim : ℚ) (↑1 : ℚ) / (↑2 : ℚ) + (↑pb.dim : ℚ)) =
    (↑pb.dim : ℚ) * HSub.hSub (α := ℚ) (↑pb.dim : ℚ) (↑1 : ℚ) / (↑2 : ℚ)

Tactic:
ring
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
refine : Fintype.card (Fin pb.dim) = Fintype.card.{v} (L →ₐ[K] E)
⊢ Fin pb.dim ≃ (L →ₐ[K] E)

Tactic:
refine equivOfCardEq ?_

Premises used: Finset.equivOfCardEq
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
rw : pb.dim = n
⊢ Fintype.card (Fin pb.dim) = Fintype.card.{v} (L →ₐ[K] E)

Tactic:
rw [Fintype.card_fin, AlgHom.card]

Premises used: Fintype.card_fin, AlgHom.card
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
⊢ pb.dim = n

Tactic:
(PowerBasis.finrank pb).symm

Premises used: PowerBasis.finrank, Eq.symm
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
⊢ pb.dim = n

Tactic:
exact (PowerBasis.finrank pb).symm

Premises used: PowerBasis.finrank, Eq.symm
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
have :
  ∀ (e : Fin pb.dim ≃ (L →ₐ[K] E)),
    discr.{u, v, 0} (ι := Fin pb.dim) K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L) =
      HMul.hMul (β := K) (HPow.hPow (α := K) (-1) (n * (n - 1) / 2))
        ((norm K : (a : L) → K)
            ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L) :
          K)
⊢ discr.{u, v, 0} (ι := Fin pb.dim) K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L) =
    HMul.hMul (β := K) (HPow.hPow (α := K) (-1) (n * (n - 1) / 2))
      ((norm K : (a : L) → K)
          ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L) :
        K)

Tactic:
have e : Fin pb.dim ≃ (L →ₐ[K] E) := by
    refine equivOfCardEq ?_
    rw [Fintype.card_fin, AlgHom.card]
    exact (PowerBasis.finrank pb).symm
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
⊢ (aroots (minpoly K pb.gen) E).Nodup

Tactic:
have hnodup : ((minpoly K pb.gen).aroots E).Nodup :=
    nodup_roots (Separable.map (Algebra.IsSeparable.isSeparable K pb.gen))
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : (aroots (minpoly K pb.gen) E).Nodup
σ : L →ₐ[K] E
rw : Eq (α := E) ((σ : (a : L) → E) ((aeval pb.gen : (a : K[X]) → L) (minpoly K pb.gen)) : E) (0 : E)
rw₁ : Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0
⊢ Membership.mem (α := E) (aroots (minpoly K pb.gen) E) ((σ : (a : L) → E) pb.gen : E)

Tactic:
rw [mem_roots, IsRoot.def, eval_map_algebraMap, aeval_algHom_apply]

Premises used: Polynomial.IsRoot.def, Polynomial.mem_roots, Polynomial.eval_map_algebraMap, Polynomial.aeval_algHom_apply
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : (aroots (minpoly K pb.gen) E).Nodup
σ : L →ₐ[K] E
⊢ Eq (α := E) ((σ : (a : L) → E) ((aeval pb.gen : (a : K[X]) → L) (minpoly K pb.gen)) : E) (0 : E)

Tactic:
simp [minpoly.ne_zero pb.isIntegral_gen]

Premises used: PowerBasis.isIntegral_gen, minpoly.ne_zero
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : (aroots (minpoly K pb.gen) E).Nodup
σ : L →ₐ[K] E
⊢ Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0

Tactic:
simp [minpoly.ne_zero pb.isIntegral_gen]

Premises used: PowerBasis.isIntegral_gen, minpoly.ne_zero
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : (aroots (minpoly K pb.gen) E).Nodup
⊢ ∀ (σ : L →ₐ[K] E), Membership.mem (α := E) (aroots (minpoly K pb.gen) E) ((σ : (a : L) → E) pb.gen : E)

Tactic:
have hroots : ∀ σ : L →ₐ[K] E, σ pb.gen ∈ (minpoly K pb.gen).aroots E := by
    intro σ
    rw [mem_roots, IsRoot.def, eval_map_algebraMap, aeval_algHom_apply]
    repeat' simp [minpoly.ne_zero pb.isIntegral_gen]
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : (aroots (minpoly K pb.gen) E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), Membership.mem (α := E) (aroots (minpoly K pb.gen) E) ((σ : (a : L) → E) pb.gen : E)
a :
  Eq.{v + 1} (α := E)
    (((algebraMap K E : K →+* E) : (a : K) → E)
        (discr.{u, v, 0} (ι := Fin pb.dim) K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L)) :
      E)
    (((algebraMap K E : K →+* E) : (a : K) → E)
        (HMul.hMul (β := K) (HPow.hPow (α := K) (-1) (n * (n - 1) / 2))
          ((norm K : (a : L) → K)
              ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L) :
            K)) :
      E)
⊢ discr.{u, v, 0} (ι := Fin pb.dim) K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L) =
    HMul.hMul (β := K) (HPow.hPow (α := K) (-1) (n * (n - 1) / 2))
      ((norm K : (a : L) → K)
          ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L) :
        K)

Tactic:
apply (algebraMap K E).injective

Premises used: Algebra.algebraMap, RingHom.injective
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : (aroots (minpoly K pb.gen) E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), Membership.mem (α := E) (aroots (minpoly K pb.gen) E) ((σ : (a : L) → E) pb.gen : E)
a :
  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) =
    HMul.hMul (β := E) (HPow.hPow (α := E) (-1) (n * (n - 1) / 2))
      (((algebraMap K E : K →+* E) : (a : K) → E)
          ((norm K : (a : L) → K)
            ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)) :
        E)
⊢ Eq.{v + 1} (α := E)
    (((algebraMap K E : K →+* E) : (a : K) → E)
        (discr.{u, v, 0} (ι := Fin pb.dim) K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L)) :
      E)
    (((algebraMap K E : K →+* E) : (a : K) → E)
        (HMul.hMul (β := K) (HPow.hPow (α := K) (-1) (n * (n - 1) / 2))
          ((norm K : (a : L) → K)
              ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L) :
            K)) :
      E)

Tactic:
rw [map_mul, map_pow, map_neg, map_one, discr_powerBasis_eq_prod'' _ _ _ e]

Premises used: map_neg, map_pow, map_mul, map_one, Algebra.discr_powerBasis_eq_prod''
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : (aroots (minpoly K pb.gen) E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), Membership.mem (α := E) (aroots (minpoly K pb.gen) E) ((σ : (a : L) → E) pb.gen : E)
a :
  Eq.{v + 1} (α := 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)
    (((algebraMap K E : K →+* E) : (a : K) → E)
        ((norm K : (a : L) → K)
          ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)) :
      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) =
    HMul.hMul (β := E) (HPow.hPow (α := E) (-1) (n * (n - 1) / 2))
      (((algebraMap K E : K →+* E) : (a : K) → E)
          ((norm K : (a : L) → K)
            ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)) :
        E)

Tactic:
congr
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : (aroots (minpoly K pb.gen) E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), Membership.mem (α := E) (aroots (minpoly K pb.gen) E) ((σ : (a : L) → E) pb.gen : E)
a :
  Eq.{v + 1} (α := E)
    (∏ i : Fin pb.dim,
      ∏ j ∈ {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))
    (∏ σ : L →ₐ[K] E,
      (σ : (a : L) → E) ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])))
⊢ Eq.{v + 1} (α := 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)
    (((algebraMap K E : K →+* E) : (a : K) → E)
        ((norm K : (a : L) → K)
          ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]) : L)) :
      E)

Tactic:
rw [norm_eq_prod_embeddings, prod_prod_Ioi_mul_eq_prod_prod_off_diag]

Premises used: Algebra.norm_eq_prod_embeddings, Finset.prod_prod_Ioi_mul_eq_prod_prod_off_diag
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : (aroots (minpoly K pb.gen) E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), Membership.mem (α := E) (aroots (minpoly K pb.gen) E) ((σ : (a : L) → E) pb.gen : E)
s : univ
f :
  fun (σ : L →ₐ[K] E) ↦
    (σ : (a : L) → E) ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]))
| ∏ σ : L →ₐ[K] E,
    (σ : (a : L) → E) ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]))

Tactic:
congr
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : (aroots (minpoly K pb.gen) E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), Membership.mem (α := E) (aroots (minpoly K pb.gen) E) ((σ : (a : L) → E) pb.gen : E)
| univ

Tactic:
rfl
-- Module: Mathlib.RingTheory.Discriminant
Goal:
K : Type u
L : Type v
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Module.Finite K L
pb : PowerBasis K L
inst_4 : Algebra.IsSeparable K L
E : Type v := AlgebraicClosure L
this : (a b : E) → Decidable (a = b) := fun (a b : E) ↦ Classical.propDecidable (a = b)
e : Fin pb.dim ≃ (L →ₐ[K] E)
hnodup : (aroots (minpoly K pb.gen) E).Nodup
hroots : ∀ (σ : L →ₐ[K] E), Membership.mem (α := E) (aroots (minpoly K pb.gen) E) ((σ : (a : L) → E) pb.gen : E)
f :
  ∀ (σ : L →ₐ[K] E),
    ((σ : (a : L) → E) ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) :
      E)
| fun (σ : L →ₐ[K] E) ↦
    (σ : (a : L) → E) ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X]))

Tactic:
ext σ