awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
h : ringKrullDim R < 1
this : KrullDimLE 0 R
⊢ False

Tactic:
exact IsDiscreteValuationRing.not_isField R KrullDimLE.isField_of_isDomain

Premises used: IsDiscreteValuationRing.not_isField, Ring.KrullDimLE.isField_of_isDomain
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
⊢ ¬KrullDimLE 0 R

Tactic:
simp [krullDimLE_iff, ringKrullDim_eq_one R]

Premises used: Ring.krullDimLE_iff, IsDiscreteValuationRing.ringKrullDim_eq_one
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsDiscreteValuationRing R
⊢ KrullDimLE 1 R

Tactic:
krullDimLE_iff.mpr (IsDiscreteValuationRing.ringKrullDim_eq_one R).le

Premises used: Iff.mpr, Ring.krullDimLE_iff, Eq.le, IsDiscreteValuationRing.ringKrullDim_eq_one
-- Module: Mathlib.RingTheory.DiscreteValuationRing.TFAE
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsDedekindDomain R
⊢ IsPrincipalIdealRing R

Tactic:
((tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain R).out 2 0).mp ‹_›

Premises used: tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain, List.TFAE.out, Iff.mp, OfNat.ofNat
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
B : Type v
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Fintype ι
b : ι → B
⊢ discr A b = (traceMatrix A b).det

Tactic:
rfl

Premises used: Algebra.discr, rfl
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
B : Type v
C : Type z
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : CommRing C
inst_5 : Algebra A C
inst_6 : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
e_M : traceMatrix A b = traceMatrix.{u, z, w} A (B := C) ((⇑f : (a : B) → C) ∘ b)
⊢ (traceMatrix A b).det = discr.{u, z, w} A (B := C) ((⇑f : (a : B) → C) ∘ b)

Tactic:
congr
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
B : Type v
C : Type z
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : CommRing C
inst_5 : Algebra A C
inst_6 : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
e_M : ∀ (i j : ι), traceMatrix A b i j = traceMatrix.{u, z, w} A (B := C) ((⇑f : (a : B) → C) ∘ b) i j
⊢ traceMatrix A b = traceMatrix.{u, z, w} A (B := C) ((⇑f : (a : B) → C) ∘ b)

Tactic:
ext
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
B : Type v
C : Type z
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : CommRing C
inst_5 : Algebra A C
inst_6 : Fintype ι
b : ι → B
f : B ≃ₐ[A] C
i j : ι
e_M :
  Eq.{u + 1} (α := A) ((((traceForm A B : (a : B) → B →ₗ[A] A) (b i) : B →ₗ[A] A) : (a : B) → A) (b j) : A)
    (((traceForm A C : (a : C) → C →ₗ[A] A) (((⇑f : (a : B) → C) ∘ b) i) : (a : C) → A) (((⇑f : (a : B) → C) ∘ b) j) :
      A)
e_M₁ :
  Eq.{u + 1} (α := A) ((trace A B : (a : B) → A) (b i * b j) : A)
    ((trace A C : (a : C) → A) (HMul.hMul (α := C) (((⇑f : (a : B) → C) ∘ b) i) (((⇑f : (a : B) → C) ∘ b) j)) : A)
e_M₂ :
  Eq.{u + 1} (α := A) ((trace A B : (a : B) → A) (b i * b j) : A)
    ((trace A C : (a : C) → A)
        (HMul.hMul (α := C) (β := C) ((f : (a : B) → C) (b i) : C) ((f : (a : B) → C) (b j) : C)) :
      A)
e_M₃ :
  Eq.{u + 1} (α := A) ((trace A B : (a : B) → A) (b i * b j) : A)
    ((trace A C : (a : C) → A) ((f : (a : B) → C) (b i * b j) : C) : A)
⊢ traceMatrix A b i j = traceMatrix.{u, z, w} A (B := C) ((⇑f : (a : B) → C) ∘ b) i j

Tactic:
simp_rw [traceMatrix_apply, traceForm_apply, Function.comp, ← map_mul f, trace_eq_of_algEquiv]

Premises used: Algebra.traceMatrix_apply, Algebra.trace_eq_of_algEquiv, Algebra.traceForm_apply, Function.comp, map_mul
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
B : Type v
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
ι' : Type u_1
inst_4 : Fintype ι'
inst_5 : Fintype ι
inst_6 : DecidableEq ι'
b : Basis ι A B
f : ι ≃ ι'
rw :
  discr.{u, v, u_1} (ι := ι') A (B := B) (⇑(b.reindex f) : (a : ι') → B) =
    discr.{u, v, w} (ι := ι) A (B := B) (⇑b : (a : ι) → B)
rw₁ :
  det.{u, u_1} (n := ι') (traceMatrix.{u, v, u_1} A (B := B) (⇑(b.reindex f) : (a : ι') → B)) =
    discr.{u, v, w} (ι := ι) A (B := B) (⇑b : (a : ι) → B)
rw₂ :
  det.{u, u_1} (n := ι')
      ((reindex f f : (a : Matrix ι ι A) → Matrix ι' ι' A) (traceMatrix.{u, v, w} A (B := B) (⇑b : (a : ι) → B))) =
    discr.{u, v, w} (ι := ι) A (B := B) (⇑b : (a : ι) → B)
rw₃ :
  det.{u, w} (n := ι) (traceMatrix.{u, v, w} A (B := B) (⇑b : (a : ι) → B)) =
    discr.{u, v, w} (ι := ι) A (B := B) (⇑b : (a : ι) → B)
rw₄ rw₅ :
  discr.{u, v, w} (ι := ι) A (B := B) (⇑b : (a : ι) → B) = discr.{u, v, w} (ι := ι) A (B := B) (⇑b : (a : ι) → B)
⊢ discr.{u, v, u_1} (ι := ι') A (B := B)
      (Function.comp.{u_1 + 1, w + 1, v + 1} (β := ι) (⇑b : (a : ι) → B) (⇑f.symm : (a : ι') → ι)) =
    discr.{u, v, w} (ι := ι) A (B := B) (⇑b : (a : ι) → B)

Tactic:
rw [← Basis.coe_reindex, discr_def, traceMatrix_reindex, det_reindex_self, ← discr_def]

Premises used: Algebra.traceMatrix_reindex, Module.Basis.coe_reindex, Matrix.det_reindex_self, Algebra.discr_def
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
B : Type v
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
ι' : Type u_1
inst_4 : Fintype ι'
inst_5 : Fintype ι
inst_6 : DecidableEq ι'
b : Basis ι A B
f : ι ≃ ι'
classical :
  discr.{u, v, u_1} (ι := ι') A (B := B) (⇑(b.reindex f) : (a : ι') → B) =
    discr.{u, v, w} (ι := ι) A (B := B) (⇑b : (a : ι) → B)
classical₁ :
  det.{u, u_1} (n := ι') (traceMatrix.{u, v, u_1} A (B := B) (⇑(b.reindex f) : (a : ι') → B)) =
    discr.{u, v, w} (ι := ι) A (B := B) (⇑b : (a : ι) → B)
classical₂ :
  det.{u, u_1} (n := ι')
      ((reindex f f : (a : Matrix ι ι A) → Matrix ι' ι' A) (traceMatrix.{u, v, w} A (B := B) (⇑b : (a : ι) → B))) =
    discr.{u, v, w} (ι := ι) A (B := B) (⇑b : (a : ι) → B)
classical₃ :
  det.{u, w} (n := ι) (traceMatrix.{u, v, w} A (B := B) (⇑b : (a : ι) → B)) =
    discr.{u, v, w} (ι := ι) A (B := B) (⇑b : (a : ι) → B)
classical₄ classical₅ :
  discr.{u, v, w} (ι := ι) A (B := B) (⇑b : (a : ι) → B) = discr.{u, v, w} (ι := ι) A (B := B) (⇑b : (a : ι) → B)
⊢ discr.{u, v, u_1} (ι := ι') A (B := B)
      (Function.comp.{u_1 + 1, w + 1, v + 1} (β := ι) (⇑b : (a : ι) → B) (⇑f.symm : (a : ι') → ι)) =
    discr.{u, v, w} (ι := ι) A (B := B) (⇑b : (a : ι) → B)

Tactic:
classical rw [← Basis.coe_reindex, discr_def, traceMatrix_reindex, det_reindex_self, ← discr_def]

Premises used: Algebra.traceMatrix_reindex, Module.Basis.coe_reindex, Matrix.det_reindex_self, Algebra.discr_def
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
B : Type v
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Fintype ι
inst_5 : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
obtain : ∀ (g : ι → A) (hg : Eq.{v + 1} (α := B) (∑ i : ι, g i • b i) 0) (i : ι) (hi : g i ≠ 0), discr A b = 0
⊢ discr A b = 0

Tactic:
obtain ⟨g, hg, i, hi⟩ := Fintype.not_linearIndependent_iff.1 hli

Premises used: Fintype.not_linearIndependent_iff, Iff.mp
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
B : Type v
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Fintype ι
inst_5 : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : Eq.{v + 1} (α := B) (∑ i : ι, g i • b i) 0
i : ι
hi : g i ≠ 0
h : ∀ (i : ι), (traceMatrix A b *ᵥ g) i = 0 i
⊢ traceMatrix A b *ᵥ g = 0

Tactic:
ext i
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
B : Type v
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Fintype ι
inst_5 : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : Eq.{v + 1} (α := B) (∑ i : ι, g i • b i) 0
i_1 : ι
hi : g i_1 ≠ 0
i j : ι
⊢ HMul.hMul (α := A) ((trace A B : (a : B) → A) (b i * b j) : A) (g j) = (trace A B : (a : B) → A) (g j • b j * b i)

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
B : Type v
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Fintype ι
inst_5 : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : Eq.{v + 1} (α := B) (∑ i : ι, g i • b i) 0
i_1 : ι
hi : g i_1 ≠ 0
i : ι
⊢ ∀ (j : ι),
    HMul.hMul (α := A) ((trace A B : (a : B) → A) (b i * b j) : A) (g j) = (trace A B : (a : B) → A) (g j • b j * b i)

Tactic:
have : ∀ j, (trace A B) (b i * b j) * g j = (trace A B) (g j • b j * b i) := by
      intro j
      simp [mul_comm]
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
B : Type v
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Fintype ι
inst_5 : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : Eq.{v + 1} (α := B) (∑ i : ι, g i • b i) 0
i_1 : ι
hi : g i_1 ≠ 0
i : ι
this :
  ∀ (j : ι),
    HMul.hMul (α := A) ((trace A B : (a : B) → A) (b i * b j) : A) (g j) = (trace A B : (a : B) → A) (g j • b j * b i)
⊢ (traceMatrix A b *ᵥ g) i = 0 i

Tactic:
simp only [mulVec, dotProduct, traceMatrix_apply, Pi.zero_apply, traceForm_apply, fun j =>
      this j, ← map_sum, ← sum_mul, hg, zero_mul, map_zero]

Premises used: Algebra.traceMatrix_apply, dotProduct, Algebra.traceForm_apply, MulZeroClass.zero_mul, Pi.zero_apply, map_zero, map_sum, Matrix.mulVec, Finset.sum_mul
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
B : Type v
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Fintype ι
inst_5 : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : Eq.{v + 1} (α := B) (∑ i : ι, g i • b i) 0
i : ι
hi : g i ≠ 0
⊢ traceMatrix A b *ᵥ g = 0

Tactic:
have : (traceMatrix A b) *ᵥ g = 0 := by
    ext i
    have : ∀ j, (trace A B) (b i * b j) * g j = (trace A B) (g j • b j * b i) := by
      intro j
      simp [mul_comm]
    simp only [mulVec, dotProduct, traceMatrix_apply, Pi.zero_apply, traceForm_apply, fun j =>
      this j, ← map_sum, ← sum_mul, hg, zero_mul, map_zero]
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
B : Type v
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Fintype ι
inst_5 : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : Eq.{v + 1} (α := B) (∑ i : ι, g i • b i) 0
i : ι
hi : g i ≠ 0
this : traceMatrix A b *ᵥ g = 0
by_contra : ∀ (h : ¬discr A b = 0), False
⊢ discr A b = 0

Tactic:
by_contra h
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
B : Type v
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Fintype ι
inst_5 : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : Eq.{v + 1} (α := B) (∑ i : ι, g i • b i) 0
i : ι
hi : g i ≠ 0
this : traceMatrix A b *ᵥ g = 0
h : ¬discr A b = 0
⊢ ¬(traceMatrix A b).det = 0

Tactic:
rw [discr_def] at h

Premises used: Algebra.discr_def
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
B : Type v
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Fintype ι
inst_5 : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : Eq.{v + 1} (α := B) (∑ i : ι, g i • b i) 0
i : ι
hi : g i ≠ 0
this : traceMatrix A b *ᵥ g = 0
h : ¬(traceMatrix A b).det = 0
⊢ False

Tactic:
simp [Matrix.eq_zero_of_mulVec_eq_zero h this] at hi

Premises used: Matrix.eq_zero_of_mulVec_eq_zero
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
B : Type v
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Fintype ι
inst_5 : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
obtain : ∀ (g : ι → A) (hg : Eq.{v + 1} (α := B) (∑ i : ι, g i • b i) 0) (i : ι) (hi : g i ≠ 0), discr A b = 0
obtain₁ :
  ∀ (g : ι → A) (hg : Eq.{v + 1} (α := B) (∑ i : ι, g i • b i) 0) (i : ι) (hi : g i ≠ 0)
    (this : traceMatrix A b *ᵥ g = 0), discr A b = 0
obtain₂ :
  ∀ (g : ι → A) (hg : Eq.{v + 1} (α := B) (∑ i : ι, g i • b i) 0) (i : ι) (hi : g i ≠ 0)
    (this : traceMatrix A b *ᵥ g = 0) (h : ¬discr A b = 0), False
obtain₃ :
  ∀ (g : ι → A) (hg : Eq.{v + 1} (α := B) (∑ i : ι, g i • b i) 0) (i : ι) (hi : g i ≠ 0)
    (this : traceMatrix A b *ᵥ g = 0) (h : ¬(traceMatrix A b).det = 0), False
⊢ discr A b = 0

Tactic:
classical
  obtain ⟨g, hg, i, hi⟩ := Fintype.not_linearIndependent_iff.1 hli
  have : (traceMatrix A b) *ᵥ g = 0 := by
    ext i
    have : ∀ j, (trace A B) (b i * b j) * g j = (trace A B) (g j • b j * b i) := by
      intro j
      simp [mul_comm]
    simp only [mulVec, dotProduct, traceMatrix_apply, Pi.zero_apply, traceForm_apply, fun j =>
      this j, ← map_sum, ← sum_mul, hg, zero_mul, map_zero]
  by_contra h
  rw [discr_def] at h
  simp [Matrix.eq_zero_of_mulVec_eq_zero h this] at hi

Premises used: Fintype.not_linearIndependent_iff, Algebra.discr_def, Iff.mp
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
B : Type v
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Fintype ι
b : ι → B
P : Matrix ι ι A
rw : (traceMatrix A (b ᵥ* P.map (⇑(algebraMap A B) : (a : A) → B))).det = HPow.hPow (β := ℕ) P.det 2 * discr A b
rw₁ : (Pᵀ * traceMatrix A b * P).det = HPow.hPow (β := ℕ) P.det 2 * discr A b
rw₂ : (Pᵀ * traceMatrix A b).det * P.det = HPow.hPow (β := ℕ) P.det 2 * discr A b
rw₃ : Pᵀ.det * (traceMatrix A b).det * P.det = HPow.hPow (β := ℕ) P.det 2 * discr A b
rw₄ : P.det * (traceMatrix A b).det * P.det = HPow.hPow (β := ℕ) P.det 2 * discr A b
rw₅ : P.det * (P.det * (traceMatrix A b).det) = HPow.hPow (β := ℕ) P.det 2 * discr A b
rw₆ : P.det * P.det * (traceMatrix A b).det = HPow.hPow (β := ℕ) P.det 2 * discr A b
rw₇ : P.det * P.det * (traceMatrix A b).det = HPow.hPow (β := ℕ) P.det 2 * (traceMatrix A b).det
rw₈ rw₉ : P.det * P.det * (traceMatrix A b).det = P.det * P.det * (traceMatrix A b).det
⊢ discr A (b ᵥ* P.map (⇑(algebraMap A B) : (a : A) → B)) = HPow.hPow (β := ℕ) P.det 2 * discr A b

Tactic:
rw [discr_def, traceMatrix_of_matrix_vecMul, det_mul, det_mul, det_transpose, mul_comm, ←
    mul_assoc, discr_def, pow_two]

Premises used: Matrix.det_transpose, pow_two, Algebra.traceMatrix_of_matrix_vecMul, mul_assoc, Matrix.det_mul, Algebra.discr_def, mul_comm
-- Module: Mathlib.RingTheory.Discriminant
Goal:
A : Type u
B : Type v
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Fintype ι
b : ι → B
P : Matrix ι ι A
rw : (traceMatrix A (P.map (⇑(algebraMap A B) : (a : A) → B) *ᵥ b)).det = HPow.hPow (β := ℕ) P.det 2 * discr A b
rw₁ : (P * traceMatrix A b * Pᵀ).det = HPow.hPow (β := ℕ) P.det 2 * discr A b
rw₂ : (P * traceMatrix A b).det * Pᵀ.det = HPow.hPow (β := ℕ) P.det 2 * discr A b
rw₃ : P.det * (traceMatrix A b).det * Pᵀ.det = HPow.hPow (β := ℕ) P.det 2 * discr A b
rw₄ : P.det * (traceMatrix A b).det * P.det = HPow.hPow (β := ℕ) P.det 2 * discr A b
rw₅ : P.det * (P.det * (traceMatrix A b).det) = HPow.hPow (β := ℕ) P.det 2 * discr A b
rw₆ : P.det * P.det * (traceMatrix A b).det = HPow.hPow (β := ℕ) P.det 2 * discr A b
rw₇ : P.det * P.det * (traceMatrix A b).det = HPow.hPow (β := ℕ) P.det 2 * (traceMatrix A b).det
rw₈ rw₉ : P.det * P.det * (traceMatrix A b).det = P.det * P.det * (traceMatrix A b).det
⊢ discr A (P.map (⇑(algebraMap A B) : (a : A) → B) *ᵥ b) = HPow.hPow (β := ℕ) P.det 2 * discr A b

Tactic:
rw [discr_def, traceMatrix_of_matrix_mulVec, det_mul, det_mul, det_transpose, mul_comm, ←
    mul_assoc, discr_def, pow_two]

Premises used: Matrix.det_transpose, pow_two, mul_assoc, Matrix.det_mul, Algebra.discr_def, mul_comm, Algebra.traceMatrix_of_matrix_mulVec
-- 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
inst_6 : Algebra.IsSeparable K L
b : Basis ι K L
rw : LinearMap.BilinForm.Nondegenerate (traceForm K L)
⊢ discr.{u, v, w} (ι := ι) K (B := L) (⇑b : (a : ι) → L) ≠ 0

Tactic:
rw [discr_def, traceMatrix_of_basis, ← LinearMap.BilinForm.nondegenerate_iff_det_ne_zero]

Premises used: Algebra.traceMatrix_of_basis, Algebra.discr_def, LinearMap.BilinForm.nondegenerate_iff_det_ne_zero
-- 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
inst_6 : Algebra.IsSeparable K L
b : Basis ι K L
⊢ LinearMap.BilinForm.Nondegenerate (traceForm K L)

Tactic:
traceForm_nondegenerate _ _

Premises used: traceForm_nondegenerate
-- 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
inst_6 : Algebra.IsSeparable K L
b : Basis ι K L
⊢ LinearMap.BilinForm.Nondegenerate (traceForm K L)

Tactic:
exact traceForm_nondegenerate _ _

Premises used: traceForm_nondegenerate
-- 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
inst_6 : Algebra.IsSeparable K L
b : Basis ι K L
⊢ IsUnit (discr.{u, v, w} (ι := ι) K (B := L) (⇑b : (a : ι) → L))

Tactic:
IsUnit.mk0 _ (discr_not_zero_of_basis _ _)

Premises used: IsUnit.mk0, Algebra.discr_not_zero_of_basis
-- Module: Mathlib.RingTheory.Discriminant
Goal:
ι : Type w
inst : DecidableEq ι
inst_1 : Fintype ι
K : Type u
L : Type v
E : Type z
inst_2 : Field K
inst_3 : Field L
inst_4 : Field E
inst_5 : Algebra K L
inst_6 : Algebra K E
inst_7 : Module.Finite K L
inst_8 : IsAlgClosed E
b : ι → L
inst_9 : Algebra.IsSeparable K L
e : ι ≃ (L →ₐ[K] E)
rw : (algebraMap K E : (a : K) → E) (traceMatrix K b).det = HPow.hPow (β := ℕ) (embeddingsMatrixReindex K E b e).det 2
rw₁ :
  det.{z, w} (n := ι) ((RingHom.mapMatrix (algebraMap K E) : (a : Matrix ι ι K) → Matrix ι ι E) (traceMatrix K b)) =
    HPow.hPow (β := ℕ) (embeddingsMatrixReindex K E b e).det 2
rw₂ :
  det ((traceMatrix K b).map (⇑(algebraMap K E) : (a : K) → E)) =
    HPow.hPow (β := ℕ) (embeddingsMatrixReindex K E b e).det 2
rw₃ :
  (embeddingsMatrixReindex K E b e * (embeddingsMatrixReindex K E b e)ᵀ).det =
    HPow.hPow (β := ℕ) (embeddingsMatrixReindex K E b e).det 2
e₁ : ι ≃ (L →ₐ[K] E)
rw₄ :
  (embeddingsMatrixReindex K E b e).det * (embeddingsMatrixReindex K E b e)ᵀ.det =
    HPow.hPow (β := ℕ) (embeddingsMatrixReindex K E b e).det 2
e₂ : ι ≃ (L →ₐ[K] E)
rw₅ :
  (embeddingsMatrixReindex K E b e).det * (embeddingsMatrixReindex K E b e).det =
    HPow.hPow (β := ℕ) (embeddingsMatrixReindex K E b e).det 2
e₃ : ι ≃ (L →ₐ[K] E)
rw₆ :
  (embeddingsMatrixReindex K E b e).det * (embeddingsMatrixReindex K E b e).det =
    (embeddingsMatrixReindex K E b e).det * (embeddingsMatrixReindex K E b e).det
e₄ : ι ≃ (L →ₐ[K] E)
rw₇ :
  (embeddingsMatrixReindex K E b e).det * (embeddingsMatrixReindex K E b e).det =
    (embeddingsMatrixReindex K E b e).det * (embeddingsMatrixReindex K E b e).det
e₅ : ι ≃ (L →ₐ[K] E)
⊢ (algebraMap K E : (a : K) → E) (discr K b) = HPow.hPow (β := ℕ) (embeddingsMatrixReindex K E b e).det 2

Tactic:
rw [discr_def, RingHom.map_det, RingHom.mapMatrix_apply,
    traceMatrix_eq_embeddingsMatrixReindex_mul_trans, det_mul, det_transpose, pow_two]

Premises used: Matrix.det_transpose, RingHom.mapMatrix_apply, pow_two, Matrix.det_mul, RingHom.map_det, Algebra.discr_def, Algebra.traceMatrix_eq_embeddingsMatrixReindex_mul_trans
-- 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
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst_7 : Algebra.IsSeparable K L
rw :
  Eq.{z + 1} (α := E)
    (∏ x : Fin pb.dim,
      HPow.hPow (α := E) (β := ℕ)
        (∏ j ∈ Ioi x,
          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) x : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
        2)
    (∏ i : Fin pb.dim,
      ∏ j ∈ Ioi i,
        HPow.hPow (β := ℕ)
          (HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
            ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
          2)
⊢ Eq.{z + 1} (α := E)
    ((algebraMap K E : (a : K) → E) (discr.{u, v, 0} (ι := Fin pb.dim) K (B := L) (⇑pb.basis : (a : Fin pb.dim) → L)) :
      E)
    (∏ i : Fin pb.dim,
        ∏ j ∈ Ioi i,
          HPow.hPow (β := ℕ)
            (HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
              ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
            2 :
      E)

Tactic:
rw [discr_eq_det_embeddingsMatrixReindex_pow_two K E pb.basis e,
    embeddingsMatrixReindex_eq_vandermonde, det_transpose, det_vandermonde, ← prod_pow]

Premises used: Matrix.det_vandermonde, Matrix.det_transpose, Algebra.embeddingsMatrixReindex_eq_vandermonde, PowerBasis.basis, Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two, Finset.prod_pow, DFunLike.coe
-- 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
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst_7 : Algebra.IsSeparable K L
e_f :
  Eq.{z + 1} (α := Fin pb.dim → E)
    (fun (x : Fin pb.dim) ↦
      HPow.hPow (α := E) (β := ℕ)
        (∏ j ∈ Ioi x,
          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) x : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
        2)
    fun (i : Fin pb.dim) ↦
    ∏ j ∈ Ioi i,
      HPow.hPow (β := ℕ)
        (HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
          ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
        2
⊢ Eq.{z + 1} (α := E)
    (∏ x : Fin pb.dim,
      HPow.hPow (α := E) (β := ℕ)
        (∏ j ∈ Ioi x,
          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) x : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
        2)
    (∏ i : Fin pb.dim,
      ∏ j ∈ Ioi i,
        HPow.hPow (β := ℕ)
          (HSub.hSub (α := E) (β := E) ((((e : (a : Fin pb.dim) → L →ₐ[K] E) j : L →ₐ[K] E) : (a : L) → E) pb.gen : E)
            ((((e : (a : Fin pb.dim) → L →ₐ[K] E) i : L →ₐ[K] E) : (a : L) → E) pb.gen : E))
          2)

Tactic:
congr