fix: tidy def of fieldOfFiniteDimensional (#5288)

As suggested by Sebastian Gouezel [here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.235256.20RingTheory.2ETrace/near/367812247). Makes the term `fieldOfFiniteDimensional` a bit tidier (it removes `  let src_1 := inst_1;`).

Author: kbuzzard

Mathlib/LinearAlgebra/FiniteDimensional.lean

@@ -1079,27 +1079,32 @@ end LinearMap
 
 section
 
+lemma FiniteDimensional.exists_mul_eq_one (F : Type _) {K : Type _} [Field F] [Ring K] [IsDomain K]
+    [Algebra F K] [FiniteDimensional F K] {x : K} (H : x ≠ 0) : ∃ y, x * y = 1 := by
+  have : Function.Surjective (LinearMap.mulLeft F x) :=
+    LinearMap.injective_iff_surjective.1 fun y z => ((mul_right_inj' H).1 : x * y = x * z → y = z)
+  exact this 1
+
 /-- A domain that is module-finite as an algebra over a field is a division ring. -/
-noncomputable def divisionRingOfFiniteDimensional (F K : Type _) [Field F] [Ring K] [IsDomain K]
+noncomputable def divisionRingOfFiniteDimensional (F K : Type _) [Field F] [h : Ring K] [IsDomain K]
     [Algebra F K] [FiniteDimensional F K] : DivisionRing K :=
-  -- porting note: extracted from the fields below to a `haveI`
-  haveI : ∀ x : K, x ≠ 0 → Function.Surjective (LinearMap.mulLeft F x) := fun x H =>
-    LinearMap.injective_iff_surjective.1 fun y z => ((mul_right_inj' H).1 : x * y = x * z → y = z)
-  { ‹IsDomain K›, ‹Ring K› with
-    inv := fun x => if H : x = 0 then 0 else Classical.choose <| (this _ H) 1
+  { ‹IsDomain K› with
+    toRing := h
+    inv := fun x => if H : x = 0 then 0 else Classical.choose <|
+      FiniteDimensional.exists_mul_eq_one F H
     mul_inv_cancel := fun x hx =>
       show x * dite _ _ _ = _ by
         rw [dif_neg hx]
-        exact (Classical.choose_spec (this _ hx 1) :)
+        exact (Classical.choose_spec (FiniteDimensional.exists_mul_eq_one F hx) :)
     inv_zero := dif_pos rfl }
 #align division_ring_of_finite_dimensional divisionRingOfFiniteDimensional
 
 /-- An integral domain that is module-finite as an algebra over a field is a field. -/
-noncomputable def fieldOfFiniteDimensional (F K : Type _) [Field F] [CommRing K] [IsDomain K]
+noncomputable def fieldOfFiniteDimensional (F K : Type _) [Field F] [h : CommRing K] [IsDomain K]
     [Algebra F K] [FiniteDimensional F K] : Field K :=
-  { divisionRingOfFiniteDimensional F K, ‹CommRing K› with }
+  { divisionRingOfFiniteDimensional F K with
+    toCommRing := h }
 #align field_of_finite_dimensional fieldOfFiniteDimensional
-
 end
 
 namespace Submodule