awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
hne : Ne (α := ℚ) (↑2 : ℚ) 0
⊢ HMul.hMul (α := ℚ) (↑pb.dim : ℚ) (↑pb.dim : ℚ) - HAdd.hAdd (α := ℚ) (↑(pb.dim * (pb.dim - 1) / 2) : ℚ) (↑pb.dim : ℚ) =
    (↑(n * (n - 1) / 2) : ℚ)
have hle : 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
-- 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
hle : 1 ≤ pb.dim
⊢ HMul.hMul (α := ℚ) (↑pb.dim : ℚ) (↑pb.dim : ℚ) - HAdd.hAdd (α := ℚ) (↑(pb.dim * (pb.dim - 1) / 2) : ℚ) (↑pb.dim : ℚ) =
    (↑(n * (n - 1) / 2) : ℚ)
have 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 : ℚ)
Tactic: rw [hn, Nat.cast_div h₂ hne, Nat.cast_mul, Nat.cast_sub hle]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
⊢ Fin pb.dim ≃ (L →ₐ[K] E)
have refine : Fintype.card (Fin pb.dim) = Fintype.card.{v} (L →ₐ[K] E)
Tactic: refine equivOfCardEq ?_
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
⊢ Fintype.card (Fin pb.dim) = Fintype.card.{v} (L →ₐ[K] E)
have rw : pb.dim = n
Tactic: rw [Fintype.card_fin, AlgHom.card]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
⊢ 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)
have 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)
Tactic: have e : Fin pb.dim ≃ (L →ₐ[K] E) := by
    refine equivOfCardEq ?_
    rw [Fintype.card_fin, AlgHom.card]
    exact (PowerBasis.finrank pb).symm
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (hypothesis)
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)
⊢ 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)
have hnodup : (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))
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
have rw : Eq (α := E) ((σ : (a : L) → E) ((aeval pb.gen : (a : K[X]) → L) (minpoly K pb.gen)) : E) (0 : E)
Tactic: rw [mem_roots, IsRoot.def, eval_map_algebraMap, aeval_algHom_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
⊢ Membership.mem (α := E) (aroots (minpoly K pb.gen) E) ((σ : (a : L) → E) pb.gen : E)
have rw₁ : Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0
Tactic: rw [mem_roots, IsRoot.def, eval_map_algebraMap, aeval_algHom_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (hypothesis)
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
⊢ 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)
have hroots : ∀ (σ : 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]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
⊢ 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)
have 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)
Tactic: apply (algebraMap K E).injective
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
⊢ 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)
have 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)
Tactic: rw [map_mul, map_pow, map_neg, map_one, discr_powerBasis_eq_prod'' _ _ _ e]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
⊢ 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)
have 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)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
⊢ 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)
have 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])))
Tactic: rw [norm_eq_prod_embeddings, prod_prod_Ioi_mul_eq_prod_prod_off_diag]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
| ∏ σ : 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]))
have s : univ
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
| ∏ σ : 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]))
have 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]))
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
| 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]))
have 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)
Tactic: ext σ
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
σ : 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)
have f : ∏ x ∈ { val := (aroots (minpoly K pb.gen) E).erase ((σ : (a : L) → E) pb.gen), nodup := sorry : Finset E },
  HSub.hSub (α := E) ((σ : (a : L) → E) pb.gen : E) x
Tactic: rw [← aeval_algHom_apply, ← eval_map_algebraMap, ← derivative_map,
      (IsAlgClosed.splits _).eval_root_derivative ((minpoly.monic pb.isIntegral_gen).map _)
      (hroots σ), ← Finset.prod_mk _ (hnodup.erase _)]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
| ∏ σ : 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]))
have f : ∀ (σ : L →ₐ[K] E),
  ∏ x ∈ { val := (aroots (minpoly K pb.gen) E).erase ((σ : (a : L) → E) pb.gen), nodup := sorry : Finset E },
    HSub.hSub (α := E) ((σ : (a : L) → E) pb.gen : E) x
Tactic: congr
    rfl
    ext σ
    rw [← aeval_algHom_apply, ← eval_map_algebraMap, ← derivative_map,
      (IsAlgClosed.splits _).eval_root_derivative ((minpoly.monic pb.isIntegral_gen).map _)
      (hroots σ), ← Finset.prod_mk _ (hnodup.erase _)]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
⊢ 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])))
have 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,
    ∏ x ∈ { val := (aroots (minpoly K pb.gen) E).erase ((σ : (a : L) → E) pb.gen), nodup := sorry : Finset E },
      HSub.hSub (α := E) ((σ : (a : L) → E) pb.gen : E) x)
Tactic: conv_rhs =>
    congr
    rfl
    ext σ
    rw [← aeval_algHom_apply, ← eval_map_algebraMap, ← derivative_map,
      (IsAlgClosed.splits _).eval_root_derivative ((minpoly.monic pb.isIntegral_gen).map _)
      (hroots σ), ← Finset.prod_mk _ (hnodup.erase _)]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
⊢ 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,
      ∏ x ∈ { val := (aroots (minpoly K pb.gen) E).erase ((σ : (a : L) → E) pb.gen), nodup := ⋯ : Finset E },
        HSub.hSub (α := E) ((σ : (a : L) → E) pb.gen : E) x)
have a : Eq.{v + 1} (α := E)
  (∏ x ∈ Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ,
    HSub.hSub (α := E) (β := E)
      ((((e : (a : Fin pb.dim) → L →ₐ[K] E) (x.snd (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)) : L →ₐ[K] E) : (a : L) → E)
          pb.gen :
        E)
      ((((e : (a : Fin pb.dim) → L →ₐ[K] E) (x.fst (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)) : L →ₐ[K] E) : (a : L) → E)
          pb.gen :
        E))
  (∏
    x ∈
      Finset.sigma (α := fun (a : L →ₐ[K] E) ↦ E) univ fun (σ : L →ₐ[K] E) ↦
        { val := (aroots (minpoly K pb.gen) E).erase ((σ : (a : L) → E) pb.gen), nodup := sorry },
    HSub.hSub (α := E) ((x.fst (β := fun (i : L →ₐ[K] E) ↦ E) : (a : L) → E) pb.gen : E)
      (x.snd (β := fun (i : L →ₐ[K] E) ↦ E)))
Tactic: rw [Finset.prod_sigma', Finset.prod_sigma']
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
⊢ Eq.{v + 1} (α := E)
    (∏ x ∈ Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ,
      HSub.hSub (α := E) (β := E)
        ((((e : (a : Fin pb.dim) → L →ₐ[K] E) (x.snd (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)) : L →ₐ[K] E) :
              (a : L) → E)
            pb.gen :
          E)
        ((((e : (a : Fin pb.dim) → L →ₐ[K] E) (x.fst (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)) : L →ₐ[K] E) :
              (a : L) → E)
            pb.gen :
          E))
    (∏
      x ∈
        Finset.sigma (α := fun (a : L →ₐ[K] E) ↦ E) univ fun (σ : L →ₐ[K] E) ↦
          { val := (aroots (minpoly K pb.gen) E).erase ((σ : (a : L) → E) pb.gen), nodup := ⋯ },
      HSub.hSub (α := E) ((x.fst (β := fun (i : L →ₐ[K] E) ↦ E) : (a : L) → E) pb.gen : E)
        (x.snd (β := fun (i : L →ₐ[K] E) ↦ E)))
have a : ∀ (σ : (_ : L →ₐ[K] E) × E)
  (hσ :
    Membership.mem (γ := Finset ((_ : L →ₐ[K] E) × E))
      (Finset.sigma (α := fun (a : L →ₐ[K] E) ↦ E) univ fun (σ : L →ₐ[K] E) ↦
        { val := (aroots (minpoly K pb.gen) E).erase ((σ : (a : L) → E) pb.gen), nodup := sorry })
      σ),
  Eq.{v + 1} (α := E) ((aeval (σ.snd (β := fun (i : L →ₐ[K] E) ↦ E)) : (a : K[X]) → E) (minpoly K pb.gen) : E) (0 : E)
Tactic: refine prod_bij' (fun i _ ↦ ⟨e i.2, e i.1 pb.gen⟩)
    (fun σ hσ ↦ ⟨e.symm (PowerBasis.lift pb σ.2 ?_), e.symm σ.1⟩) ?_ ?_ ?_ ?_ (fun i _ ↦ by simp)