chore(LinearAlgebra): golf (#10569)

- rename `span_eq_top_of_linearIndependent_of_card_eq_finrank`
  to `LinearIndependent.span_eq_top_of_card_eq_finrank`;
- add a version `LinearIndependent.span_eq_top_of_card_eq_finrank'`
  with different typeclass assumptions;
- use `rfl` to prove `Algebra.discr_def`;
- golf `Algebra.discr_not_zero_of_basis`.

Author: urkud

Mathlib/LinearAlgebra/FiniteDimensional.lean

@@ -933,29 +933,30 @@ end Span
 
 section Basis
 
-theorem span_eq_top_of_linearIndependent_of_card_eq_finrank {ι : Type*} [hι : Nonempty ι]
-    [Fintype ι] {b : ι → V} (lin_ind : LinearIndependent K b)
+theorem LinearIndependent.span_eq_top_of_card_eq_finrank' {ι : Type*}
+    [Fintype ι] [FiniteDimensional K V] {b : ι → V} (lin_ind : LinearIndependent K b)
     (card_eq : Fintype.card ι = finrank K V) : span K (Set.range b) = ⊤ := by
-  by_cases fin : FiniteDimensional K V
-  · by_contra ne_top
-    have lt_top : span K (Set.range b) < ⊤ := lt_of_le_of_ne le_top ne_top
-    exact ne_of_lt (Submodule.finrank_lt lt_top)
-      (_root_.trans (finrank_span_eq_card lin_ind) card_eq)
-  · exfalso
-    apply ne_of_lt (Fintype.card_pos_iff.mpr hι)
-    symm
-    replace fin := (not_iff_not.2 IsNoetherian.iff_fg).2 fin
-    calc
-      Fintype.card ι = finrank K V := card_eq
-      _ = 0 := dif_neg (mt IsNoetherian.iff_rank_lt_aleph0.mpr fin)
-#align span_eq_top_of_linear_independent_of_card_eq_finrank span_eq_top_of_linearIndependent_of_card_eq_finrank
+  by_contra ne_top
+  rw [← finrank_span_eq_card lin_ind] at card_eq
+  exact ne_of_lt (Submodule.finrank_lt <| lt_top_iff_ne_top.2 ne_top) card_eq
+
+theorem LinearIndependent.span_eq_top_of_card_eq_finrank {ι : Type*} [Nonempty ι]
+    [Fintype ι] {b : ι → V} (lin_ind : LinearIndependent K b)
+    (card_eq : Fintype.card ι = finrank K V) : span K (Set.range b) = ⊤ :=
+  have : FiniteDimensional K V := .of_finrank_pos <| card_eq ▸ Fintype.card_pos
+  lin_ind.span_eq_top_of_card_eq_finrank' card_eq
+#align span_eq_top_of_linear_independent_of_card_eq_finrank LinearIndependent.span_eq_top_of_card_eq_finrank
+
+@[deprecated] -- 2024-02-14
+alias span_eq_top_of_linearIndependent_of_card_eq_finrank :=
+  LinearIndependent.span_eq_top_of_card_eq_finrank
 
 /-- A linear independent family of `finrank K V` vectors forms a basis. -/
 @[simps! repr_apply]
 noncomputable def basisOfLinearIndependentOfCardEqFinrank {ι : Type*} [Nonempty ι] [Fintype ι]
     {b : ι → V} (lin_ind : LinearIndependent K b) (card_eq : Fintype.card ι = finrank K V) :
     Basis ι K V :=
-  Basis.mk lin_ind <| (span_eq_top_of_linearIndependent_of_card_eq_finrank lin_ind card_eq).ge
+  Basis.mk lin_ind <| (lin_ind.span_eq_top_of_card_eq_finrank card_eq).ge
 #align basis_of_linear_independent_of_card_eq_finrank basisOfLinearIndependentOfCardEqFinrank
 
 @[simp]

Mathlib/RingTheory/Discriminant.lean

@@ -70,10 +70,7 @@ noncomputable def discr (A : Type u) {B : Type v} [CommRing A] [CommRing B] [Alg
     [Fintype ι] (b : ι → B) := (traceMatrix A b).det
 #align algebra.discr Algebra.discr
 
-theorem discr_def [Fintype ι] (b : ι → B) : discr A b = (traceMatrix A b).det := by
--- Porting note: `unfold discr` was not necessary. `rfl` still does not work.
-  unfold discr
-  convert rfl
+theorem discr_def [Fintype ι] (b : ι → B) : discr A b = (traceMatrix A b).det := rfl
 
 variable {A C} in
 /-- Mapping a family of vectors along an `AlgEquiv` preserves the discriminant. -/
@@ -141,19 +138,8 @@ variable [Module.Finite K L] [IsAlgClosed E]
 /-- If `b` is a basis of a finite separable field extension `L/K`, then `Algebra.discr K b ≠ 0`. -/
 theorem discr_not_zero_of_basis [IsSeparable K L] (b : Basis ι K L) :
     discr K b ≠ 0 := by
-  cases isEmpty_or_nonempty ι
--- Porting note: the following proof was `simp [discr]`. Variations like `exact this` do not work.
-  · have : det (traceMatrix K ↑b) ≠ 0 := by simp
-    unfold discr
-    convert this
-  · have :=
-      span_eq_top_of_linearIndependent_of_card_eq_finrank b.linearIndependent
-        (finrank_eq_card_basis b).symm
-    classical
-    rw [discr_def, traceMatrix]
-    simp_rw [← Basis.mk_apply b.linearIndependent this.ge]
-    rw [← traceMatrix, traceMatrix_of_basis, ← BilinForm.nondegenerate_iff_det_ne_zero]
-    exact traceForm_nondegenerate _ _
+  rw [discr_def, traceMatrix_of_basis, ← BilinForm.nondegenerate_iff_det_ne_zero]
+  exact traceForm_nondegenerate _ _
 #align algebra.discr_not_zero_of_basis Algebra.discr_not_zero_of_basis
 
 /-- If `b` is a basis of a finite separable field extension `L/K`,