-- Mathlib/RingTheory/Discriminant.lean
theorem discr_zero_of_not_linearIndependent [IsDomain A] {b : ι → B}
    (hli : ¬LinearIndependent A b) : discr A b = 0

Proof state:
A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i : ι
hi : g i ≠ 0
⊢ traceMatrix A b *ᵥ g = 0

Tactic:
ext i

Result:
case h
A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i✝ : ι
hi : g i✝ ≠ 0
i : ι
⊢ (traceMatrix A b *ᵥ g) i = 0 i

Proof state:
case intro.intro.intro
A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i : ι
hi : g i ≠ 0
⊢ discr A b = 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, LinearMap.map_zero]

Result:
case intro.intro.intro
A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i : ι
hi : g i ≠ 0
this : traceMatrix A b *ᵥ g = 0
⊢ discr A b = 0

Proof state:
case h
A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i✝ : ι
hi : g i✝ ≠ 0
i : ι
⊢ (traceMatrix A b *ᵥ g) i = 0 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]

Result:
case h
A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i✝ : ι
hi : g i✝ ≠ 0
i : ι
this : ∀ (j : ι), (trace A B) (b i * b j) * g j = (trace A B) (g j • b j * b i)
⊢ (traceMatrix A b *ᵥ g) i = 0 i

Proof state:
A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i✝ : ι
hi : g i✝ ≠ 0
i j : ι
⊢ (trace A B) (b i * b j) * g j = (trace A B) (g j • b j * b i)

Tactic:
simp [mul_comm]

Result:
no goals

Proof state:
A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
⊢ 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, LinearMap.map_zero]
by_contra h
rw [discr_def] at h
simp [Matrix.eq_zero_of_mulVec_eq_zero h this] at hi

Result:
no goals

Proof state:
case intro.intro.intro
A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i : ι
hi : g i ≠ 0
this : traceMatrix A b *ᵥ g = 0
h : ¬discr A b = 0
⊢ False

Tactic:
rw [discr_def] at h

Result:
case intro.intro.intro
A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i : ι
hi : g i ≠ 0
this : traceMatrix A b *ᵥ g = 0
h : ¬(traceMatrix A b).det = 0
⊢ False

Proof state:
case intro.intro.intro
A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ 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

Result:
no goals

Proof state:
A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i✝ : ι
hi : g i✝ ≠ 0
i : ι
⊢ ∀ (j : ι), (trace A B) (b i * b j) * g j = (trace A B) (g j • b j * b i)

Tactic:
intro j

Result:
A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i✝ : ι
hi : g i✝ ≠ 0
i j : ι
⊢ (trace A B) (b i * b j) * g j = (trace A B) (g j • b j * b i)

Proof state:
case intro.intro.intro
A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i : ι
hi : g i ≠ 0
this : traceMatrix A b *ᵥ g = 0
⊢ discr A b = 0

Tactic:
by_contra h

Result:
case intro.intro.intro
A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i : ι
hi : g i ≠ 0
this : traceMatrix A b *ᵥ g = 0
h : ¬discr A b = 0
⊢ False

Proof state:
case h
A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i✝ : ι
hi : g i✝ ≠ 0
i : ι
this : ∀ (j : ι), (trace A B) (b i * b j) * g j = (trace A B) (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, LinearMap.map_zero]

Result:
no goals

Proof state:
A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
⊢ discr A b = 0

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

Result:
case intro.intro.intro
A : Type u
B : Type v
ι : Type w
inst✝⁵ : DecidableEq ι
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Fintype ι
inst✝ : IsDomain A
b : ι → B
hli : ¬LinearIndependent A b
g : ι → A
hg : ∑ i : ι, g i • b i = 0
i : ι
hi : g i ≠ 0
⊢ discr A b = 0