chore (Algebra.Field.Defs): remove unused structure instances (#6686)

In both `Division.toDivisionSemiring` and `Field.toSemiField`, an extra unused `Semiring` instance is provided to construct the instance. This removes them.

Mathlib/Algebra/Field/Defs.lean

@@ -106,7 +106,7 @@ class DivisionRing (K : Type u) extends Ring K, DivInvMonoid K, Nontrivial K, Ra
 
 -- see Note [lower instance priority]
 instance (priority := 100) DivisionRing.toDivisionSemiring [DivisionRing α] : DivisionSemiring α :=
-  { ‹DivisionRing α›, (inferInstance : Semiring α) with }
+  { ‹DivisionRing α› with }
 #align division_ring.to_division_semiring DivisionRing.toDivisionSemiring
 
 /-- A `Semifield` is a `CommSemiring` with multiplicative inverses for nonzero elements. -/
@@ -170,7 +170,7 @@ variable [Field K]
 
 -- see Note [lower instance priority]
 instance (priority := 100) Field.toSemifield : Semifield K :=
-  { ‹Field K›, (inferInstance : Semiring K) with }
+  { ‹Field K› with }
 #align field.to_semifield Field.toSemifield
 
 end Field