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
σ : (_ : L →ₐ[K] E) × E
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)
hσ :
  σ.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
⊢ Eq.{v + 1} (α := E) ((aeval (σ.snd (β := fun (i : L →ₐ[K] E) ↦ E)) : (a : K[X]) → E) (minpoly K pb.gen) : E) (0 : E)

Tactic:
simpa only [aeval_def, eval₂_eq_eval_map] using hσ.2.2

Premises used: Polynomial.aeval_def, And.right, Polynomial.eval₂_eq_eval_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),
    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)

Tactic:
fun a b hba ↦ ⟨fun h ↦ hba <| e.injective <| pb.algHom_ext h.symm, hroots _⟩

Premises used: And.intro, PowerBasis.algHom_ext, Equiv.injective, Eq.symm, DFunLike.coe
-- 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),
    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)

Tactic:
exact fun a b hba ↦ ⟨fun h ↦ hba <| e.injective <| pb.algHom_ext h.symm, hroots _⟩
-- 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_1 : ∀ (σ : L →ₐ[K] E), Membership.mem (α := E) (aroots (minpoly K pb.gen) E) ((σ : (a : L) → E) pb.gen : E)
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
hba :
  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
ha : a = pb.lift b ⋯
⊢ b ≠ b ∧
    Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
      eval b (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0

Tactic:
rw [ha, PowerBasis.lift_gen] at hba

Premises used: PowerBasis.lift_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_1 : ∀ (σ : L →ₐ[K] E), Membership.mem (α := E) (aroots (minpoly K pb.gen) E) ((σ : (a : L) → E) pb.gen : E)
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
hba :
  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
ha : a = pb.lift b ⋯
hba₁ :
  b ≠ b ∧
    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 ⋯

Tactic:
rw [ha, PowerBasis.lift_gen] at hba

Premises used: PowerBasis.lift_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_1 : ∀ (σ : L →ₐ[K] E), Membership.mem (α := E) (aroots (minpoly K pb.gen) E) ((σ : (a : L) → E) pb.gen : E)
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
hba_1 :
  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
hba :
  b ≠ b ∧
    Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
      eval b (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0
ha : a = pb.lift b ⋯
⊢ False

Tactic:
hba.1 rfl

Premises used: And.left, 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_1 : ∀ (σ : L →ₐ[K] E), Membership.mem (α := E) (aroots (minpoly K pb.gen) E) ((σ : (a : L) → E) pb.gen : E)
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
hba_1 :
  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
hba :
  b ≠ b ∧
    Polynomial.map (algebraMap K E) (minpoly K pb.gen) ≠ 0 ∧
      eval b (Polynomial.map (algebraMap K E) (minpoly K pb.gen)) = 0
ha : a = pb.lift b ⋯
⊢ False

Tactic:
exact hba.1 rfl

Premises used: And.left, 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)
⊢ ∀ (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)

Tactic:
fun a b _ ↦ pb.algHom_ext <| pb.lift_gen _ _

Premises used: Eq.mpr, Polynomial.eval, Algebra.algebraMap, _private.0.Algebra.discr_powerBasis_eq_norm._simp_7, congrArg, PowerBasis.gen, _private.0.Algebra.discr_powerBasis_eq_norm._simp_1, _private.0.Algebra.discr_powerBasis_eq_norm._simp_6, Eq.mp, id, _private.0.Algebra.discr_powerBasis_eq_norm._simp_2, Ne, Sigma.fst, minpoly, forall_prop_domain_congr, And, And.right, _private.0.Algebra.discr_powerBasis_eq_norm._simp_5, And.intro, congr, Multiset.Nodup.mem_erase_iff, propext, Eq.substr, congrFun', PowerBasis.algHom_ext, Polynomial.map, Equiv.injective, _private.0.Algebra.discr_powerBasis_eq_norm._simp_3, Sigma.mk, OfNat.ofNat, Eq.symm, Sigma.snd, PowerBasis.lift_gen, Eq, DFunLike.coe, _private.0.Algebra.discr_powerBasis_eq_norm._simp_4, Polynomial.eval₂_eq_eval_map, Not, _private.0.Algebra.discr_powerBasis_eq_norm._simp_8, true_and, Eq.trans, forall_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 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)

Tactic:
exact fun a b _ ↦ pb.algHom_ext <| pb.lift_gen _ _

Premises used: PowerBasis.gen, PowerBasis.algHom_ext, PowerBasis.lift_gen, DFunLike.coe
-- Module: Mathlib.RingTheory.Discriminant
Goal:
ι : Type w
inst : DecidableEq ι
inst_1 : Fintype ι
K : Type u
L : Type v
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : Module.Finite K L
R : Type z
inst_6 : CommRing R
inst_7 : Algebra R K
inst_8 : Algebra R L
inst_9 : IsScalarTower R K L
b : ι → L
h : ∀ (i : ι), IsIntegral R (b i)
⊢ IsIntegral R (traceMatrix K b).det

Tactic:
IsIntegral.det fun i j ↦ isIntegral_trace ((h i).mul (h j))

Premises used: IsIntegral.mul, Algebra.isIntegral_trace, IsIntegral.det
-- Module: Mathlib.RingTheory.Discriminant
Goal:
ι : Type w
inst : DecidableEq ι
inst_1 : Fintype ι
K : Type u
L : Type v
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : Module.Finite K L
R : Type z
inst_6 : CommRing R
inst_7 : Algebra R K
inst_8 : Algebra R L
inst_9 : IsScalarTower R K L
b : ι → L
h : ∀ (i : ι), IsIntegral R (b i)
⊢ IsIntegral R (traceMatrix K b).det

Tactic:
exact IsIntegral.det fun i j ↦ isIntegral_trace ((h i).mul (h j))

Premises used: IsIntegral.mul, Algebra.isIntegral_trace, IsIntegral.det
-- Module: Mathlib.RingTheory.Discriminant
Goal:
ι : Type w
inst : DecidableEq ι
inst_1 : Fintype ι
K : Type u
L : Type v
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : Module.Finite K L
R : Type z
inst_6 : CommRing R
inst_7 : Algebra R K
inst_8 : Algebra R L
inst_9 : IsScalarTower R K L
b : ι → L
h : ∀ (i : ι), IsIntegral R (b i)
rw rw₁ rw₂ : IsIntegral R (traceMatrix K b).det
⊢ IsIntegral R (discr K b)

Tactic:
classical
  rw [discr_def]
  exact IsIntegral.det fun i j ↦ isIntegral_trace ((h i).mul (h j))

Premises used: IsIntegral.mul, Algebra.isIntegral_trace, IsIntegral.det, Algebra.discr_def
-- 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
R : Type z
inst_4 : CommRing R
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : IsScalarTower R K L
inst_8 : Algebra.IsSeparable K L
inst_9 : IsIntegrallyClosed R
inst_10 : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
⊢ IsUnit (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))

Tactic:
simpa [← discr_def] using discr_isUnit_of_basis _ B.basis

Premises used: PowerBasis.basis, Algebra.discr_def, Algebra.discr_isUnit_of_basis
-- 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
R : Type z
inst_4 : CommRing R
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : IsScalarTower R K L
inst_8 : Algebra.IsSeparable K L
inst_9 : IsIntegrallyClosed R
inst_10 : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
⊢ IsUnit (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))

Tactic:
have hinv : IsUnit (traceMatrix K B.basis).det := by
    simpa [← discr_def] using discr_isUnit_of_basis _ B.basis
-- 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
R : Type z
inst_4 : CommRing R
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : IsScalarTower R K L
inst_8 : Algebra.IsSeparable K L
inst_9 : IsIntegrallyClosed R
inst_10 : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
e_a :
  Eq (α := Fin B.dim → K)
    (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
      (B.basis.equivFun : (a : L) → Fin B.dim → K) z)
    fun (i : Fin B.dim) ↦ (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))
⊢ HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
      (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
        (B.basis.equivFun : (a : L) → Fin B.dim → K) z) =
    HSMul.hSMul (β := (i : Fin B.dim) → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L))) fun (i : Fin B.dim) ↦
      (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))

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
R : Type z
inst_4 : CommRing R
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : IsScalarTower R K L
inst_8 : Algebra.IsSeparable K L
inst_9 : IsIntegrallyClosed R
inst_10 : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
⊢ Eq (α := Fin B.dim → K)
    (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
      (B.basis.equivFun : (a : L) → Fin B.dim → K) z)
    fun (i : Fin B.dim) ↦ (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))

Tactic:
traceMatrix_of_basis_mulVec _ _

Premises used: Algebra.traceMatrix_of_basis_mulVec
-- 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
R : Type z
inst_4 : CommRing R
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : IsScalarTower R K L
inst_8 : Algebra.IsSeparable K L
inst_9 : IsIntegrallyClosed R
inst_10 : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
⊢ Eq (α := Fin B.dim → K)
    (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
      (B.basis.equivFun : (a : L) → Fin B.dim → K) z)
    fun (i : Fin B.dim) ↦ (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))

Tactic:
exact traceMatrix_of_basis_mulVec _ _

Premises used: Algebra.traceMatrix_of_basis_mulVec
-- 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
R : Type z
inst_4 : CommRing R
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : IsScalarTower R K L
inst_8 : Algebra.IsSeparable K L
inst_9 : IsIntegrallyClosed R
inst_10 : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
⊢ HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
      (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
        (B.basis.equivFun : (a : L) → Fin B.dim → K) z) =
    HSMul.hSMul (β := (i : Fin B.dim) → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L))) fun (i : Fin B.dim) ↦
      (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))

Tactic:
have H :
    (traceMatrix K B.basis).det • (traceMatrix K B.basis) *ᵥ (B.basis.equivFun z) =
      (traceMatrix K B.basis).det • fun i => trace K L (z * B.basis i) := by
    congr; exact traceMatrix_of_basis_mulVec _ _
-- 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
R : Type z
inst_4 : CommRing R
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : IsScalarTower R K L
inst_8 : Algebra.IsSeparable K L
inst_9 : IsIntegrallyClosed R
inst_10 : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
H :
  HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
      (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
        (B.basis.equivFun : (a : L) → Fin B.dim → K) z) =
    HSMul.hSMul (β := (i : Fin B.dim) → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L))) fun (i : Fin B.dim) ↦
      (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))
⊢ (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
      (cramer (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)) : (a : Fin B.dim → K) → Fin B.dim → K)
        fun (i : Fin B.dim) ↦
        (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))) =
    HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L))) fun (i : Fin B.dim) ↦
      (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))

Tactic:
have cramer := mulVec_cramer (traceMatrix K B.basis) fun i => trace K L (z * B.basis i)
-- 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
R : Type z
inst_4 : CommRing R
inst_5 : Algebra R K
inst_6 : Algebra R L
inst_7 : IsScalarTower R K L
inst_8 : Algebra.IsSeparable K L
inst_9 : IsIntegrallyClosed R
inst_10 : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
H :
  HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
      (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
        (B.basis.equivFun : (a : L) → Fin B.dim → K) z) =
    HSMul.hSMul (β := (i : Fin B.dim) → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L))) fun (i : Fin B.dim) ↦
      (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))
cramer :
  (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L) *ᵥ
      (Matrix.cramer (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)) :
          (a : Fin B.dim → K) → Fin B.dim → K)
        fun (i : Fin B.dim) ↦
        (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))) =
    HSMul.hSMul (β := Fin B.dim → K)
      (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L))) fun (i : Fin B.dim) ↦
      (trace K L : (a : L) → K) (HMul.hMul (β := L) z ((B.basis : (a : Fin B.dim) → L) i : L))
this :
  ∀ (i : Fin B.dim),
    Membership.mem (γ := Subalgebra R K) ⊥
      (HSMul.hSMul (β := Fin B.dim → K)
        (det («n» := Fin B.dim) (traceMatrix.{u, v, 0} K (B := L) (⇑B.basis : (a : Fin B.dim) → L)))
        ((B.basis.equivFun : (a : L) → Fin B.dim → K) z : Fin B.dim → K) i)
rw :
  Membership.mem (γ := Subalgebra R L) R[B.gen]
    (∑ x : Fin B.dim,
      discr.{u, v, 0} (ι := Fin B.dim) K (B := L) (⇑B.basis : (a : Fin B.dim) → L) •
        HSMul.hSMul.{u, v, v} (α := K) (β := L)
          ((((B.basis.repr : (a : L) → Fin B.dim →₀ K) z : Fin B.dim →₀ K) : (a : Fin B.dim) → K) x : K)
          ((B.basis : (a : Fin B.dim) → L) x : L))
⊢ Membership.mem (γ := Subalgebra R L) R[B.gen]
    (discr.{u, v, 0} (ι := Fin B.dim) K (B := L) (⇑B.basis : (a : Fin B.dim) → L) • z)

Tactic:
rw [← B.basis.sum_repr z, Finset.smul_sum]

Premises used: PowerBasis.basis, Finset.smul_sum, Module.Basis.sum_repr