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
ι' : 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)
⊢ 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)
have 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)
Tactic: rw [← Basis.coe_reindex, discr_def, traceMatrix_reindex, det_reindex_self, ← discr_def]
-- 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
ι' : 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)
⊢ 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)
have 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)
Tactic: rw [← Basis.coe_reindex, discr_def, traceMatrix_reindex, det_reindex_self, ← discr_def]
-- 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
ι' : 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)
⊢ 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)
have 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)
Tactic: rw [← Basis.coe_reindex, discr_def, traceMatrix_reindex, det_reindex_self, ← discr_def]
-- 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
ι' : 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)
⊢ 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)
have rw₄ : discr.{u, v, w} (ι := ι) A (B := B) (⇑b : (a : ι) → B) = discr.{u, v, w} (ι := ι) A (B := B) (⇑b : (a : ι) → B)
Tactic: rw [← Basis.coe_reindex, discr_def, traceMatrix_reindex, det_reindex_self, ← discr_def]
-- 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
ι' : Type u_1
inst_4 : Fintype ι'
inst_5 : Fintype ι
inst_6 : DecidableEq ι'
b : Basis ι A B
f : ι ≃ ι'
⊢ 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)
have classical : discr.{u, v, u_1} (ι := ι') A (B := B) (⇑(b.reindex f) : (a : ι') → B) =
  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]
-- 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
ι' : 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)
⊢ 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)
have 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)
Tactic: classical rw [← Basis.coe_reindex, discr_def, traceMatrix_reindex, det_reindex_self, ← discr_def]
-- 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
ι' : 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)
⊢ 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)
have 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)
Tactic: classical rw [← Basis.coe_reindex, discr_def, traceMatrix_reindex, det_reindex_self, ← discr_def]
-- 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
ι' : 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)
⊢ 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)
have 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)
Tactic: classical rw [← Basis.coe_reindex, discr_def, traceMatrix_reindex, det_reindex_self, ← discr_def]
-- 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
ι' : 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)
⊢ 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)
have classical₄ : discr.{u, v, w} (ι := ι) A (B := B) (⇑b : (a : ι) → B) = 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]
-- 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 ι
inst_5 : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
⊢ discr A b = 0
have obtain : ∀ (g : ι → A) (hg : Eq.{v + 1} (α := B) (∑ i : ι, g i • b i) 0) (i : ι) (hi : g i ≠ 0), discr A b = 0
Tactic: obtain ⟨g, hg, i, hi⟩ := Fintype.not_linearIndependent_iff.1 hli
-- 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 ι
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
have h : ∀ (i : ι), (traceMatrix A b *ᵥ g) i = 0 i
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (hypothesis)
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 : ι
⊢ (traceMatrix A b *ᵥ g) i = 0 i
have 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)
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]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (hypothesis)
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
⊢ discr A b = 0
have this : 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]
-- 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 ι
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
⊢ discr A b = 0
have by_contra : ∀ (h : ¬discr A b = 0), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (hypothesis)
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
⊢ False
have h₁ : ¬(traceMatrix A b).det = 0
Tactic: rw [discr_def] at h
Cleared hypotheses: h
-- 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 ι
inst_5 : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
⊢ discr A b = 0
have obtain : ∀ (g : ι → A) (hg : Eq.{v + 1} (α := B) (∑ i : ι, g i • b i) 0) (i : ι) (hi : g i ≠ 0), 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
-- 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 ι
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
have 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
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
-- 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 ι
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
⊢ discr A b = 0
have 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
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
-- 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 ι
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
⊢ discr A b = 0
have 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
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
-- 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 (b ᵥ* P.map (⇑(algebraMap A B) : (a : A) → B)) = HPow.hPow (β := ℕ) P.det 2 * discr A b
have rw : (traceMatrix A (b ᵥ* P.map (⇑(algebraMap A B) : (a : A) → B))).det = 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]
-- 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
⊢ discr A (b ᵥ* P.map (⇑(algebraMap A B) : (a : A) → 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_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
⊢ discr A (b ᵥ* P.map (⇑(algebraMap A B) : (a : A) → 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_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
⊢ discr A (b ᵥ* P.map (⇑(algebraMap A B) : (a : A) → 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_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
⊢ discr A (b ᵥ* P.map (⇑(algebraMap A B) : (a : A) → 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_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
⊢ 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 * 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]
-- 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
⊢ 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 * 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]