chore: adjust Module.Finite instance priority (leanprover-community#37522)

Make instances that are rarely going to be helpful lower priority.
Increase the priority of `FiniteDimensional.complexToReal`, because it's more likely correct than the other priority 100 `Module.Finite` instances.

Co-authored-by: Matthew Jasper <mjjasper1@gmail.com>

Author: matthewjasper

Mathlib/LinearAlgebra/Complex/FiniteDimensional.lean

@@ -44,7 +44,7 @@ theorem finrank_real_complex_fact : Fact (finrank ℝ ℂ = 2) :=
 
 end Complex
 
-instance (priority := 100) FiniteDimensional.complexToReal (E : Type*) [AddCommGroup E]
+instance (priority := 500) FiniteDimensional.complexToReal (E : Type*) [AddCommGroup E]
     [Module ℂ E] [FiniteDimensional ℂ E] : FiniteDimensional ℝ E :=
   FiniteDimensional.trans ℝ ℂ E
 

Mathlib/LinearAlgebra/Dimension/Free.lean

@@ -366,8 +366,8 @@ end StrongRankCondition
 
 namespace Algebra
 
-instance (R S : Type*) [CommSemiring R] [StrongRankCondition R] [Semiring S] [Algebra R S]
-    [IsQuadraticExtension R S] :
+instance (priority := 100) (R S : Type*) [CommSemiring R] [StrongRankCondition R] [Semiring S]
+    [Algebra R S] [IsQuadraticExtension R S] :
     Module.Finite R S := finite_of_finrank_eq_succ <| IsQuadraticExtension.finrank_eq_two R S
 
 end Algebra

Mathlib/LinearAlgebra/Dual/Lemmas.lean

@@ -283,7 +283,9 @@ instance _root_.Prod.instModuleIsReflexive [IsReflexive R N] :
 instance _root_.ULift.instModuleIsReflexive.{w} : IsReflexive R (ULift.{w} M) :=
   equiv ULift.moduleEquiv.symm
 
-instance instFiniteDimensionalOfIsReflexive (K V : Type*)
+-- Very low priority because instance resolution will often end up using the instances above
+-- to prove `IsReflexive`, which require proving `Finite` again.
+instance (priority := 90) instFiniteDimensionalOfIsReflexive (K V : Type*)
     [Field K] [AddCommGroup V] [Module K V] [IsReflexive K V] :
     FiniteDimensional K V := by
   rw [FiniteDimensional, ← rank_lt_aleph0_iff]