awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ discr A (b ᵥ* P.map (⇑(algebraMap A B) : (a : A) → B)) = HPow.hPow (β := ℕ) P.det 2 * discr A b
have rw₇ : P.det * P.det * (traceMatrix A b).det = HPow.hPow (β := ℕ) P.det 2 * (traceMatrix A b).det
Tactic: rw [discr_def, traceMatrix_of_matrix_vecMul, det_mul, det_mul, det_transpose, mul_comm, ←
    mul_assoc, discr_def, pow_two]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ discr A (b ᵥ* P.map (⇑(algebraMap A B) : (a : A) → B)) = HPow.hPow (β := ℕ) P.det 2 * discr A b
have rw₈ : P.det * P.det * (traceMatrix A b).det = P.det * P.det * (traceMatrix A b).det
Tactic: rw [discr_def, traceMatrix_of_matrix_vecMul, det_mul, det_mul, det_transpose, mul_comm, ←
    mul_assoc, discr_def, pow_two]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ discr A (P.map (⇑(algebraMap A B) : (a : A) → B) *ᵥ b) = HPow.hPow (β := ℕ) P.det 2 * discr A b
have rw : (traceMatrix A (P.map (⇑(algebraMap A B) : (a : A) → B) *ᵥ b)).det = 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]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ discr A (P.map (⇑(algebraMap A B) : (a : A) → B) *ᵥ b) = HPow.hPow (β := ℕ) P.det 2 * discr A b
have rw₁ : (P * traceMatrix A b * Pᵀ).det = 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]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ discr A (P.map (⇑(algebraMap A B) : (a : A) → B) *ᵥ b) = HPow.hPow (β := ℕ) P.det 2 * discr A b
have rw₂ : (P * traceMatrix A b).det * Pᵀ.det = 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]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ discr A (P.map (⇑(algebraMap A B) : (a : A) → B) *ᵥ b) = HPow.hPow (β := ℕ) P.det 2 * discr A b
have rw₃ : P.det * (traceMatrix A b).det * Pᵀ.det = 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]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ discr A (P.map (⇑(algebraMap A B) : (a : A) → B) *ᵥ b) = HPow.hPow (β := ℕ) P.det 2 * discr A b
have rw₄ : P.det * (traceMatrix A b).det * P.det = 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]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ discr A (P.map (⇑(algebraMap A B) : (a : A) → B) *ᵥ b) = HPow.hPow (β := ℕ) P.det 2 * discr A b
have rw₅ : P.det * (P.det * (traceMatrix A b).det) = 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]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ discr A (P.map (⇑(algebraMap A B) : (a : A) → B) *ᵥ b) = HPow.hPow (β := ℕ) P.det 2 * discr A b
have rw₆ : P.det * P.det * (traceMatrix A b).det = 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]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ discr A (P.map (⇑(algebraMap A B) : (a : A) → B) *ᵥ b) = HPow.hPow (β := ℕ) P.det 2 * discr A b
have rw₇ : P.det * P.det * (traceMatrix A b).det = HPow.hPow (β := ℕ) P.det 2 * (traceMatrix A b).det
Tactic: rw [discr_def, traceMatrix_of_matrix_mulVec, det_mul, det_mul, det_transpose, mul_comm, ←
    mul_assoc, discr_def, pow_two]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ discr A (P.map (⇑(algebraMap A B) : (a : A) → B) *ᵥ b) = HPow.hPow (β := ℕ) P.det 2 * discr A b
have rw₈ : P.det * P.det * (traceMatrix A b).det = P.det * P.det * (traceMatrix A b).det
Tactic: rw [discr_def, traceMatrix_of_matrix_mulVec, det_mul, det_mul, det_transpose, mul_comm, ←
    mul_assoc, discr_def, pow_two]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ discr.{u, v, w} (ι := ι) K (B := L) (⇑b : (a : ι) → L) ≠ 0
have rw : LinearMap.BilinForm.Nondegenerate (traceForm K L)
Tactic: rw [discr_def, traceMatrix_of_basis, ← LinearMap.BilinForm.nondegenerate_iff_det_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
⊢ (algebraMap K E : (a : K) → E) (discr K b) = HPow.hPow (β := ℕ) (embeddingsMatrixReindex K E b e).det 2
have rw : (algebraMap K E : (a : K) → E) (traceMatrix K b).det = 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]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ (algebraMap K E : (a : K) → E) (discr K b) = HPow.hPow (β := ℕ) (embeddingsMatrixReindex K E b e).det 2
have 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
Tactic: rw [discr_def, RingHom.map_det, RingHom.mapMatrix_apply,
    traceMatrix_eq_embeddingsMatrixReindex_mul_trans, det_mul, det_transpose, pow_two]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ (algebraMap K E : (a : K) → E) (discr K b) = HPow.hPow (β := ℕ) (embeddingsMatrixReindex K E b e).det 2
have rw₂ : det ((traceMatrix K b).map (⇑(algebraMap K E) : (a : K) → E)) =
  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]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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
⊢ (algebraMap K E : (a : K) → E) (discr K b) = HPow.hPow (β := ℕ) (embeddingsMatrixReindex K E b e).det 2
have rw₃ : (embeddingsMatrixReindex K E b e * (embeddingsMatrixReindex K E b e)ᵀ).det =
  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]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
⊢ (algebraMap K E : (a : K) → E) (discr K b) = HPow.hPow (β := ℕ) (embeddingsMatrixReindex K E b e).det 2
have rw₄ : (embeddingsMatrixReindex K E b e).det * (embeddingsMatrixReindex K E b e)ᵀ.det =
  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]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
⊢ (algebraMap K E : (a : K) → E) (discr K b) = HPow.hPow (β := ℕ) (embeddingsMatrixReindex K E b e).det 2
have rw₅ : (embeddingsMatrixReindex K E b e).det * (embeddingsMatrixReindex K E b e).det =
  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]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
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)
⊢ (algebraMap K E : (a : K) → E) (discr K b) = HPow.hPow (β := ℕ) (embeddingsMatrixReindex K E b e).det 2
have 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
Tactic: rw [discr_def, RingHom.map_det, RingHom.mapMatrix_apply,
    traceMatrix_eq_embeddingsMatrixReindex_mul_trans, det_mul, det_transpose, pow_two]
-- 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
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst_7 : Algebra.IsSeparable K L
⊢ 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)
have 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)
Tactic: rw [discr_eq_det_embeddingsMatrixReindex_pow_two K E pb.basis e,
    embeddingsMatrixReindex_eq_vandermonde, det_transpose, det_vandermonde, ← prod_pow]
-- 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
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst_7 : Algebra.IsSeparable K L
⊢ 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)
have 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
Tactic: congr
-- 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
e : Fin pb.dim ≃ (L →ₐ[K] E)
inst_7 : Algebra.IsSeparable K L
⊢ 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
have e_f : ∀ (i : Fin pb.dim),
  HPow.hPow (α := E) (β := ℕ)
      (∏ 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))
      2 =
    ∏ 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: ext i