awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
σ : L →ₐ[K] E
f :
  ∏ 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
| ((σ : (a : L) → E) ((aeval pb.gen : (a : K[X]) → L) ((derivative : (a : K[X]) → K[X]) (minpoly K pb.gen) : K[X])) : E)

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 _)]

Premises used: minpoly.monic, PowerBasis.isIntegral_gen, Polynomial.Splits.eval_root_derivative, Finset.prod_mk, Multiset.Nodup.erase, IsAlgClosed.splits, Polynomial.eval_map_algebraMap, Polynomial.derivative_map, Polynomial.aeval_algHom_apply, Polynomial.Monic.map
-- 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),
    ∏ 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
| ∏ σ : 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
    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 _)]

Premises used: Finset.prod_mk, Multiset.Nodup.erase, Polynomial.eval_map_algebraMap, Polynomial.derivative_map, 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
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,
      ∏ 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)
⊢ 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:
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 _)]

Premises used: Finset.prod_mk, Multiset.Nodup.erase, Polynomial.eval_map_algebraMap, Polynomial.derivative_map, 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
hroots : ∀ (σ : L →ₐ[K] E), Membership.mem (α := E) (aroots (minpoly K pb.gen) E) ((σ : (a : L) → E) pb.gen : E)
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 := ⋯ },
      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)))
⊢ 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)

Tactic:
rw [Finset.prod_sigma', Finset.prod_sigma']

Premises used: Finset.prod_sigma'
-- 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)
i : (_ : Fin pb.dim) × Fin pb.dim
h :
  Membership.mem (γ := Finset ((_ : Fin pb.dim) × Fin pb.dim))
    (Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ) i
⊢ HSub.hSub (α := E) (β := E)
      ((((e : (a : Fin pb.dim) → L →ₐ[K] E) (i.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) (i.fst (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)) : L →ₐ[K] E) : (a : L) → E)
          pb.gen :
        E) =
    HSub.hSub (α := E) (β := E)
      ((Sigma.fst (β := fun (i : L →ₐ[K] E) ↦ E)
              ((fun (i : (_ : Fin pb.dim) × Fin pb.dim)
                    (x :
                      Membership.mem (γ := Finset ((_ : Fin pb.dim) × Fin pb.dim))
                        (Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ) i) ↦
                  (Sigma.mk (β := fun (i : L →ₐ[K] E) ↦ E)
                      ((e : (a : Fin pb.dim) → L →ₐ[K] E) (i.snd (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)))
                      ((((e : (a : Fin pb.dim) → L →ₐ[K] E) (i.fst (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)) :
                            L →ₐ[K] E) :
                          (a : L) → E)
                        pb.gen) :
                    (_ : L →ₐ[K] E) × E))
                i h) :
            (a : L) → E)
          pb.gen :
        E)
      (Sigma.snd (β := fun (i : L →ₐ[K] E) ↦ E)
          ((fun (i : (_ : Fin pb.dim) × Fin pb.dim)
                (x :
                  Membership.mem (γ := Finset ((_ : Fin pb.dim) × Fin pb.dim))
                    (Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ) i) ↦
              (Sigma.mk (β := fun (i : L →ₐ[K] E) ↦ E)
                  ((e : (a : Fin pb.dim) → L →ₐ[K] E) (i.snd (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)))
                  ((((e : (a : Fin pb.dim) → L →ₐ[K] E) (i.fst (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)) : L →ₐ[K] E) :
                      (a : L) → E)
                    pb.gen) :
                (_ : L →ₐ[K] E) × E))
            i h) :
        E)

Tactic:
simp
-- 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)
σ : (_ : 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 := ⋯ })
    σ
⊢ ∀ (σ : L →ₐ[K] E),
    Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
      Eq (α := E) (eval ((σ : (a : L) → E) pb.gen) (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) : E) (0 : E)

Tactic:
simp only [mem_sigma, mem_univ, Finset.mem_mk, hnodup.mem_erase_iff, IsRoot.def,
      mem_roots', mem_singleton, true_and, mem_compl, Sigma.forall, Equiv.apply_symm_apply,
      PowerBasis.lift_gen, implies_true, Equiv.symm_apply_apply,
      Sigma.ext_iff, Equiv.symm_apply_eq, heq_eq_eq, and_true] at *

Premises used: Finset.mem_univ, Finset.mem_singleton, Equiv.apply_symm_apply, Finset.mem_mk, and_true, Equiv.symm_apply_apply, heq_eq_eq, Polynomial.IsRoot.def, Sigma.ext_iff, Equiv.symm_apply_eq, Sigma.forall, Finset.mem_sigma, Finset.mem_compl, Polynomial.mem_roots', Multiset.Nodup.mem_erase_iff, implies_true, PowerBasis.lift_gen, true_and
-- 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)
σ : (_ : 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 := ⋯ })
    σ
hroots₁ :
  ∀ (σ : L →ₐ[K] E),
    Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
      Eq (α := E) (eval ((σ : (a : L) → E) pb.gen) (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) : E) (0 : E)
⊢ σ.snd (β := fun (i : L →ₐ[K] E) ↦ E) ≠ (σ.fst (β := fun (i : L →ₐ[K] E) ↦ E) : (a : L) → E) pb.gen ∧
    Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
      eval (σ.snd (β := fun (i : L →ₐ[K] E) ↦ E)) (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0

Tactic:
simp only [mem_sigma, mem_univ, Finset.mem_mk, hnodup.mem_erase_iff, IsRoot.def,
      mem_roots', mem_singleton, true_and, mem_compl, Sigma.forall, Equiv.apply_symm_apply,
      PowerBasis.lift_gen, implies_true, Equiv.symm_apply_apply,
      Sigma.ext_iff, Equiv.symm_apply_eq, heq_eq_eq, and_true] at *

Premises used: Finset.mem_univ, Finset.mem_singleton, Equiv.apply_symm_apply, Finset.mem_mk, and_true, Equiv.symm_apply_apply, heq_eq_eq, Polynomial.IsRoot.def, Sigma.ext_iff, Equiv.symm_apply_eq, Sigma.forall, Finset.mem_sigma, Finset.mem_compl, Polynomial.mem_roots', Multiset.Nodup.mem_erase_iff, implies_true, PowerBasis.lift_gen, true_and
-- 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 :
  ∀
    (hroots :
      ∀ (σ : L →ₐ[K] E),
        Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
          Eq (α := E) (eval ((σ : (a : L) → E) pb.gen) (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) : E)
            (0 : E))
    (a b : Fin pb.dim) (ha : ¬b = a),
    Ne (α := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) a : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
        ((((e : (a : Fin pb.dim) → L →ₐ[K] E) b : L →ₐ[K] E) : (a : L) → E) pb.gen : E) ∧
      Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
        Eq (α := E)
          (eval ((((e : (a : Fin pb.dim) → L →ₐ[K] E) a : L →ₐ[K] E) : (a : L) → E) pb.gen)
              (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) :
            E)
          (0 : E)
⊢ ∀ (a : (_ : Fin pb.dim) × Fin pb.dim)
    (ha :
      Membership.mem (γ := Finset ((_ : Fin pb.dim) × Fin pb.dim))
        (Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ) a),
    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 := ⋯ })
      ((fun (i : (_ : Fin pb.dim) × Fin pb.dim)
            (x :
              Membership.mem (γ := Finset ((_ : Fin pb.dim) × Fin pb.dim))
                (Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ) i) ↦
          (Sigma.mk (β := fun (i : L →ₐ[K] E) ↦ E)
              ((e : (a : Fin pb.dim) → L →ₐ[K] E) (i.snd (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)))
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) (i.fst (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)) : L →ₐ[K] E) :
                  (a : L) → E)
                pb.gen) :
            (_ : L →ₐ[K] E) × E))
        a ha)

Tactic:
simp only [mem_sigma, mem_univ, Finset.mem_mk, hnodup.mem_erase_iff, IsRoot.def,
      mem_roots', mem_singleton, true_and, mem_compl, Sigma.forall, Equiv.apply_symm_apply,
      PowerBasis.lift_gen, implies_true, Equiv.symm_apply_apply,
      Sigma.ext_iff, Equiv.symm_apply_eq, heq_eq_eq, and_true] at *

Premises used: Finset.mem_univ, Finset.mem_singleton, Equiv.apply_symm_apply, Finset.mem_mk, and_true, Equiv.symm_apply_apply, heq_eq_eq, Polynomial.IsRoot.def, Sigma.ext_iff, Equiv.symm_apply_eq, Sigma.forall, Finset.mem_sigma, Finset.mem_compl, Polynomial.mem_roots', Multiset.Nodup.mem_erase_iff, implies_true, PowerBasis.lift_gen, true_and
-- 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 :
  ∀
    (hroots :
      ∀ (σ : L →ₐ[K] E),
        Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
          Eq (α := E) (eval ((σ : (a : L) → E) pb.gen) (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) : E)
            (0 : E))
    (a : L →ₐ[K] E) (b : E)
    (ha :
      b ≠ (a : (a : L) → E) pb.gen ∧
        Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
          eval b (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0),
    ¬a = pb.lift b ⋯
⊢ ∀ (a : (_ : L →ₐ[K] E) × E)
    (ha :
      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 := ⋯ })
        a),
    Membership.mem (γ := Finset ((_ : Fin pb.dim) × Fin pb.dim))
      (Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ)
      ((fun (σ : (_ : 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 := ⋯ })
                σ) ↦
          (Sigma.mk (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)
              ((e.symm : (a : L →ₐ[K] E) → Fin pb.dim) (pb.lift (σ.snd (β := fun (i : L →ₐ[K] E) ↦ E)) ⋯))
              ((e.symm : (a : L →ₐ[K] E) → Fin pb.dim) (σ.fst (β := fun (i : L →ₐ[K] E) ↦ E))) :
            (_ : Fin pb.dim) × Fin pb.dim))
        a ha)

Tactic:
simp only [mem_sigma, mem_univ, Finset.mem_mk, hnodup.mem_erase_iff, IsRoot.def,
      mem_roots', mem_singleton, true_and, mem_compl, Sigma.forall, Equiv.apply_symm_apply,
      PowerBasis.lift_gen, implies_true, Equiv.symm_apply_apply,
      Sigma.ext_iff, Equiv.symm_apply_eq, heq_eq_eq, and_true] at *

Premises used: Finset.mem_univ, Finset.mem_singleton, Equiv.apply_symm_apply, Finset.mem_mk, and_true, Equiv.symm_apply_apply, heq_eq_eq, Polynomial.IsRoot.def, Sigma.ext_iff, Equiv.symm_apply_eq, Sigma.forall, Finset.mem_sigma, Finset.mem_compl, Polynomial.mem_roots', Multiset.Nodup.mem_erase_iff, implies_true, PowerBasis.lift_gen, true_and
-- 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 :
  ∀ (a b : Fin pb.dim) (ha : ¬b = a),
    Eq (α := L →ₐ[K] E)
      (pb.lift ((((e : (a : Fin pb.dim) → L →ₐ[K] E) a : L →ₐ[K] E) : (a : L) → E) pb.gen) ⋯ : L →ₐ[K] E)
      ((e : (a : Fin pb.dim) → L →ₐ[K] E) a : L →ₐ[K] E)
⊢ ∀ (a : (_ : Fin pb.dim) × Fin pb.dim)
    (ha :
      Membership.mem (γ := Finset ((_ : Fin pb.dim) × Fin pb.dim))
        (Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ) a),
    (fun (σ : (_ : 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 := ⋯ })
                σ) ↦
          (Sigma.mk (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)
              ((e.symm : (a : L →ₐ[K] E) → Fin pb.dim) (pb.lift (σ.snd (β := fun (i : L →ₐ[K] E) ↦ E)) ⋯))
              ((e.symm : (a : L →ₐ[K] E) → Fin pb.dim) (σ.fst (β := fun (i : L →ₐ[K] E) ↦ E))) :
            (_ : Fin pb.dim) × Fin pb.dim))
        ((fun (i : (_ : Fin pb.dim) × Fin pb.dim)
              (x :
                Membership.mem (γ := Finset ((_ : Fin pb.dim) × Fin pb.dim))
                  (Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ) i) ↦
            (Sigma.mk (β := fun (i : L →ₐ[K] E) ↦ E)
                ((e : (a : Fin pb.dim) → L →ₐ[K] E) (i.snd (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)))
                ((((e : (a : Fin pb.dim) → L →ₐ[K] E) (i.fst (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)) : L →ₐ[K] E) :
                    (a : L) → E)
                  pb.gen) :
              (_ : L →ₐ[K] E) × E))
          a ha)
        ⋯ =
      a

Tactic:
simp only [mem_sigma, mem_univ, Finset.mem_mk, hnodup.mem_erase_iff, IsRoot.def,
      mem_roots', mem_singleton, true_and, mem_compl, Sigma.forall, Equiv.apply_symm_apply,
      PowerBasis.lift_gen, implies_true, Equiv.symm_apply_apply,
      Sigma.ext_iff, Equiv.symm_apply_eq, heq_eq_eq, and_true] at *

Premises used: Finset.mem_univ, Finset.mem_singleton, Equiv.apply_symm_apply, Finset.mem_mk, and_true, Equiv.symm_apply_apply, heq_eq_eq, Polynomial.IsRoot.def, Sigma.ext_iff, Equiv.symm_apply_eq, Sigma.forall, Finset.mem_sigma, Finset.mem_compl, Polynomial.mem_roots', Multiset.Nodup.mem_erase_iff, implies_true, PowerBasis.lift_gen, true_and
-- 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 : (_ : L →ₐ[K] E) × E)
    (ha :
      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 := ⋯ })
        a),
    (fun (i : (_ : Fin pb.dim) × Fin pb.dim)
            (x :
              Membership.mem (γ := Finset ((_ : Fin pb.dim) × Fin pb.dim))
                (Finset.sigma (α := fun (a : Fin pb.dim) ↦ Fin pb.dim) univ fun (i : Fin pb.dim) ↦ {i}ᶜ) i) ↦
          (Sigma.mk (β := fun (i : L →ₐ[K] E) ↦ E)
              ((e : (a : Fin pb.dim) → L →ₐ[K] E) (i.snd (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)))
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) (i.fst (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)) : L →ₐ[K] E) :
                  (a : L) → E)
                pb.gen) :
            (_ : L →ₐ[K] E) × E))
        ((fun (σ : (_ : 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 := ⋯ })
                  σ) ↦
            (Sigma.mk (β := fun (i : Fin pb.dim) ↦ Fin pb.dim)
                ((e.symm : (a : L →ₐ[K] E) → Fin pb.dim) (pb.lift (σ.snd (β := fun (i : L →ₐ[K] E) ↦ E)) ⋯))
                ((e.symm : (a : L →ₐ[K] E) → Fin pb.dim) (σ.fst (β := fun (i : L →ₐ[K] E) ↦ E))) :
              (_ : Fin pb.dim) × Fin pb.dim))
          a ha)
        ⋯ =
      a

Tactic:
simp only [mem_sigma, mem_univ, Finset.mem_mk, hnodup.mem_erase_iff, IsRoot.def,
      mem_roots', mem_singleton, true_and, mem_compl, Sigma.forall, Equiv.apply_symm_apply,
      PowerBasis.lift_gen, implies_true, Equiv.symm_apply_apply,
      Sigma.ext_iff, Equiv.symm_apply_eq, heq_eq_eq, and_true] at *

Premises used: Finset.mem_univ, Finset.mem_singleton, Equiv.apply_symm_apply, Finset.mem_mk, and_true, Equiv.symm_apply_apply, heq_eq_eq, Polynomial.IsRoot.def, Sigma.ext_iff, Equiv.symm_apply_eq, Sigma.forall, Finset.mem_sigma, Finset.mem_compl, Polynomial.mem_roots', Multiset.Nodup.mem_erase_iff, implies_true, PowerBasis.lift_gen, true_and