feat(linear_algebra/finite_dimensional): make finite_dimensional_bot …

…an instance (#9053)

This was previously made into a local instance in several places, but there appears to be no reason it can't be a global instance.

cf discussion at #8884.

src/analysis/normed_space/inner_product.lean

@@ -2211,8 +2211,6 @@ end
 @[simp] lemma orthogonal_projection_mem_subspace_eq_self (v : K) : orthogonal_projection K v = v :=
 by { ext, apply eq_orthogonal_projection_of_mem_of_inner_eq_zero; simp }
 
-local attribute [instance] finite_dimensional_bot
-
 /-- The orthogonal projection onto the trivial submodule is the zero map. -/
 @[simp] lemma orthogonal_projection_bot : orthogonal_projection (⊥ : submodule 𝕜 E) = 0 :=
 by ext

src/linear_algebra/finite_dimensional.lean

@@ -608,12 +608,11 @@ finrank_eq_zero_of_basis_imp_false (λ s b, h ⟨s, ⟨b⟩⟩)
 
 variables (K V)
 
-lemma finite_dimensional_bot : finite_dimensional K (⊥ : submodule K V) :=
+instance finite_dimensional_bot : finite_dimensional K (⊥ : submodule K V) :=
 finite_dimensional_of_dim_eq_zero $ by simp
 
 @[simp] lemma finrank_bot : finrank K (⊥ : submodule K V) = 0 :=
 begin
-  haveI := finite_dimensional_bot K V,
   convert finrank_eq_dim K (⊥ : submodule K V),
   rw dim_bot, norm_cast
 end
@@ -1426,13 +1425,12 @@ by { rw ← algebra.top_to_submodule, refl }
 lemma subalgebra.dim_top : module.rank F (⊤ : subalgebra F E) = module.rank F E :=
 by { rw subalgebra_top_dim_eq_submodule_top_dim, exact dim_top F E }
 
-lemma subalgebra.finite_dimensional_bot : finite_dimensional F (⊥ : subalgebra F E) :=
+instance subalgebra.finite_dimensional_bot : finite_dimensional F (⊥ : subalgebra F E) :=
 finite_dimensional_of_dim_eq_one subalgebra.dim_bot
 
 @[simp]
 lemma subalgebra.finrank_bot : finrank F (⊥ : subalgebra F E) = 1 :=
 begin
-  haveI : finite_dimensional F (⊥ : subalgebra F E) := subalgebra.finite_dimensional_bot,
   have : module.rank F (⊥ : subalgebra F E) = 1 := subalgebra.dim_bot,
   rw ← finrank_eq_dim at this,
   norm_cast at *,