chore(linear_algebra/finite_dimensional): generalize from Type to Sort (

#18723)

The replacement of `fintype` with `finite` means there's no longer a need to handle these cases (added in #12877) separately.

I verified that `{ι : Sort*}` is not being inferred as `{ι : Sort (u + 1)}`.

src/linear_algebra/finite_dimensional.lean

@@ -688,27 +688,15 @@ begin
 end
 
 /-- The submodule generated by a supremum of finite dimensional submodules, indexed by a finite
-type is finite-dimensional. -/
-instance finite_dimensional_supr {ι : Type*} [_root_.finite ι] (S : ι → submodule K V)
+sort is finite-dimensional. -/
+instance finite_dimensional_supr {ι : Sort*} [_root_.finite ι] (S : ι → submodule K V)
   [Π i, finite_dimensional K (S i)] : finite_dimensional K ↥(⨆ i, S i) :=
 begin
-  casesI nonempty_fintype ι,
-  rw ←finset.sup_univ_eq_supr,
+  casesI nonempty_fintype (plift ι),
+  rw [←supr_plift_down, ← finset.sup_univ_eq_supr],
   exact submodule.finite_dimensional_finset_sup _ _,
 end
 
-/-- The submodule generated by a supremum indexed by a proposition is finite-dimensional if
-the submodule is. -/
-instance finite_dimensional_supr_prop {P : Prop} (S : P → submodule K V)
-  [Π h, finite_dimensional K (S h)] : finite_dimensional K ↥(⨆ h, S h) :=
-begin
-  by_cases hp : P,
-  { rw supr_pos hp,
-    apply_instance },
-  { rw supr_neg hp,
-    apply_instance },
-end
-
 /-- The dimension of a submodule is bounded by the dimension of the ambient space. -/
 lemma finrank_le [finite_dimensional K V] (s : submodule K V) : finrank K s ≤ finrank K V :=
 by simpa only [cardinal.nat_cast_le, ←finrank_eq_dim] using