[Merged by Bors] - chore(Field/InjSurj): Tidy

Mathlib/Algebra/DirectSum/Ring.lean

@@ -432,7 +432,7 @@ theorem of_zero_mul (a b : A 0) : of _ 0 (a * b) = of _ 0 a * of _ 0 b :=
 
 instance GradeZero.nonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring (A 0) :=
   Function.Injective.nonUnitalNonAssocSemiring (of A 0) DFinsupp.single_injective (of A 0).map_zero
-    (of A 0).map_add (of_zero_mul A) fun x n => DFinsupp.single_smul n x
+    (of A 0).map_add (of_zero_mul A) (map_nsmul _)
 #align direct_sum.grade_zero.non_unital_non_assoc_semiring DirectSum.GradeZero.nonUnitalNonAssocSemiring
 
 instance GradeZero.smulWithZero (i : ι) : SMulWithZero (A 0) (A i) := by
@@ -473,8 +473,8 @@ theorem of_zero_ofNat (n : ℕ) [n.AtLeastTwo] : of A 0 (no_index (OfNat.ofNat n
 /-- The `Semiring` structure derived from `GSemiring A`. -/
 instance GradeZero.semiring : Semiring (A 0) :=
   Function.Injective.semiring (of A 0) DFinsupp.single_injective (of A 0).map_zero (of_zero_one A)
-    (of A 0).map_add (of_zero_mul A) (of A 0).map_nsmul (fun _ _ => of_zero_pow _ _ _)
-    (of_natCast A)
+    (of A 0).map_add (of_zero_mul A) (fun _ _ ↦ (of A 0).map_nsmul _ _)
+    (fun _ _ => of_zero_pow _ _ _) (of_natCast A)
 #align direct_sum.grade_zero.semiring DirectSum.GradeZero.semiring
 
 /-- `of A 0` is a `RingHom`, using the `DirectSum.GradeZero.semiring` structure. -/
@@ -501,7 +501,7 @@ variable [∀ i, AddCommMonoid (A i)] [AddCommMonoid ι] [GCommSemiring A]
 /-- The `CommSemiring` structure derived from `GCommSemiring A`. -/
 instance GradeZero.commSemiring : CommSemiring (A 0) :=
   Function.Injective.commSemiring (of A 0) DFinsupp.single_injective (of A 0).map_zero
-    (of_zero_one A) (of A 0).map_add (of_zero_mul A) (fun x n => DFinsupp.single_smul n x)
+    (of_zero_one A) (of A 0).map_add (of_zero_mul A) (fun _ _ ↦ map_nsmul _ _ _)
     (fun _ _ => of_zero_pow _ _ _) (of_natCast A)
 #align direct_sum.grade_zero.comm_semiring DirectSum.GradeZero.commSemiring
 
@@ -514,13 +514,8 @@ variable [∀ i, AddCommGroup (A i)] [AddZeroClass ι] [GNonUnitalNonAssocSemiri
 /-- The `NonUnitalNonAssocRing` derived from `GNonUnitalNonAssocSemiring A`. -/
 instance GradeZero.nonUnitalNonAssocRing : NonUnitalNonAssocRing (A 0) :=
   Function.Injective.nonUnitalNonAssocRing (of A 0) DFinsupp.single_injective (of A 0).map_zero
-    (of A 0).map_add (of_zero_mul A) (of A 0).map_neg (of A 0).map_sub
-    (fun x n =>
-      letI : ∀ i, DistribMulAction ℕ (A i) := fun _ => inferInstance
-      DFinsupp.single_smul n x)
-    fun x n =>
-    letI : ∀ i, DistribMulAction ℤ (A i) := fun _ => inferInstance
-    DFinsupp.single_smul n x
+    (of A 0).map_add (of_zero_mul A) (of A 0).map_neg (of A 0).map_sub (fun _ _ ↦ map_nsmul _ _ _)
+    (fun _ _ ↦ map_zsmul _ _ _)
 #align direct_sum.grade_zero.non_unital_non_assoc_ring DirectSum.GradeZero.nonUnitalNonAssocRing
 
 end Ring
@@ -540,14 +535,8 @@ theorem of_intCast (n : ℤ) : of A 0 n = n := by
 /-- The `Ring` derived from `GSemiring A`. -/
 instance GradeZero.ring : Ring (A 0) :=
   Function.Injective.ring (of A 0) DFinsupp.single_injective (of A 0).map_zero (of_zero_one A)
-    (of A 0).map_add (of_zero_mul A) (of A 0).map_neg (of A 0).map_sub
-    (fun x n =>
-      letI : ∀ i, DistribMulAction ℕ (A i) := fun _ => inferInstance
-      DFinsupp.single_smul n x)
-    (fun x n =>
-      letI : ∀ i, DistribMulAction ℤ (A i) := fun _ => inferInstance
-      DFinsupp.single_smul n x)
-    (fun _ _ => of_zero_pow _ _ _) (of_natCast A) (of_intCast A)
+    (of A 0).map_add (of_zero_mul A) (of A 0).map_neg (of A 0).map_sub (fun _ _ ↦ map_nsmul _ _ _)
+    (fun _ _ ↦ map_zsmul _ _ _) (fun _ _ => of_zero_pow _ _ _) (of_natCast A) (of_intCast A)
 #align direct_sum.grade_zero.ring DirectSum.GradeZero.ring
 
 end Ring
@@ -559,14 +548,8 @@ variable [∀ i, AddCommGroup (A i)] [AddCommMonoid ι] [GCommRing A]
 /-- The `CommRing` derived from `GCommSemiring A`. -/
 instance GradeZero.commRing : CommRing (A 0) :=
   Function.Injective.commRing (of A 0) DFinsupp.single_injective (of A 0).map_zero (of_zero_one A)
-    (of A 0).map_add (of_zero_mul A) (of A 0).map_neg (of A 0).map_sub
-    (fun x n =>
-      letI : ∀ i, DistribMulAction ℕ (A i) := fun _ => inferInstance
-      DFinsupp.single_smul n x)
-    (fun x n =>
-      letI : ∀ i, DistribMulAction ℤ (A i) := fun _ => inferInstance
-      DFinsupp.single_smul n x)
-    (fun _ _ => of_zero_pow _ _ _) (of_natCast A) (of_intCast A)
+    (of A 0).map_add (of_zero_mul A) (of A 0).map_neg (of A 0).map_sub (fun _ _ ↦ map_nsmul _ _ _)
+    (fun _ _ ↦ map_zsmul _ _ _) (fun _ _ => of_zero_pow _ _ _) (of_natCast A) (of_intCast A)
 #align direct_sum.grade_zero.comm_ring DirectSum.GradeZero.commRing
 
 end CommRing

Mathlib/Algebra/Field/Basic.lean

@@ -6,7 +6,6 @@ Authors: Robert Lewis, Leonardo de Moura, Johannes Hölzl, Mario Carneiro
 import Mathlib.Algebra.Field.Defs
 import Mathlib.Algebra.GroupWithZero.Units.Lemmas
 import Mathlib.Algebra.Ring.Commute
-import Mathlib.Algebra.Ring.Hom.Defs
 
 #align_import algebra.field.basic from "leanprover-community/mathlib"@"05101c3df9d9cfe9430edc205860c79b6d660102"
 
@@ -15,7 +14,6 @@ import Mathlib.Algebra.Ring.Hom.Defs
 
 -/
 
-
 open Function OrderDual Set
 
 universe u
@@ -265,149 +263,129 @@ section NoncomputableDefs
 variable {R : Type*} [Nontrivial R]
 
 /-- Constructs a `DivisionRing` structure on a `Ring` consisting only of units and 0. -/
-noncomputable def divisionRingOfIsUnitOrEqZero [hR : Ring R] (h : ∀ a : R, IsUnit a ∨ a = 0) :
-    DivisionRing R :=
-  { groupWithZeroOfIsUnitOrEqZero h, hR with qsmul := qsmulRec _}
-#align division_ring_of_is_unit_or_eq_zero divisionRingOfIsUnitOrEqZero
-
-/-- Constructs a `Field` structure on a `CommRing` consisting only of units and 0.
-See note [reducible non-instances]. -/
-@[reducible]
-noncomputable def fieldOfIsUnitOrEqZero [hR : CommRing R] (h : ∀ a : R, IsUnit a ∨ a = 0) :
-    Field R :=
-  { divisionRingOfIsUnitOrEqZero h, hR with }
-#align field_of_is_unit_or_eq_zero fieldOfIsUnitOrEqZero
+@[reducible] -- See note [reducible non-instances]
+noncomputable def DivisionRing.ofIsUnitOrEqZero [Ring R] (h : ∀ a : R, IsUnit a ∨ a = 0) :
+    DivisionRing R where
+  toRing := ‹Ring R›
+  __ := groupWithZeroOfIsUnitOrEqZero h
+  qsmul := _
+#align division_ring_of_is_unit_or_eq_zero DivisionRing.ofIsUnitOrEqZero
+
+/-- Constructs a `Field` structure on a `CommRing` consisting only of units and 0. -/
+@[reducible] -- See note [reducible non-instances]
+noncomputable def Field.ofIsUnitOrEqZero [CommRing R] (h : ∀ a : R, IsUnit a ∨ a = 0) :
+    Field R where
+  toCommRing := ‹CommRing R›
+  __ := DivisionRing.ofIsUnitOrEqZero h
+#align field_of_is_unit_or_eq_zero Field.ofIsUnitOrEqZero
 
 end NoncomputableDefs
 
--- See note [reducible non-instances]
+namespace Function.Injective
+variable [Zero α] [Add α] [Neg α] [Sub α] [One α] [Mul α] [Inv α] [Div α] [SMul ℕ α]
+  [SMul ℤ α] [SMul ℚ α] [Pow α ℕ] [Pow α ℤ] [NatCast α] [IntCast α] [RatCast α]
+  (f : α → β) (hf : Injective f)
+
 /-- Pullback a `DivisionSemiring` along an injective function. -/
-@[reducible]
-protected def Function.Injective.divisionSemiring [DivisionSemiring β] [Zero α] [Mul α] [Add α]
-    [One α] [Inv α] [Div α] [SMul ℕ α] [Pow α ℕ] [Pow α ℤ] [NatCast α] (f : α → β)
-    (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y)
-    (mul : ∀ x y, f (x * y) = f x * f y) (inv : ∀ x, f x⁻¹ = (f x)⁻¹)
-    (div : ∀ x y, f (x / y) = f x / f y) (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x)
+@[reducible] -- See note [reducible non-instances]
+protected def divisionSemiring [DivisionSemiring β] (zero : f 0 = 0) (one : f 1 = 1)
+    (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
+    (inv : ∀ x, f x⁻¹ = (f x)⁻¹) (div : ∀ x y, f (x / y) = f x / f y)
+    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
     (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n)
-    (nat_cast : ∀ n : ℕ, f n = n) : DivisionSemiring α :=
-  { hf.groupWithZero f zero one mul inv div npow zpow,
-    hf.semiring f zero one add mul nsmul npow nat_cast with }
+    (natCast : ∀ n : ℕ, f n = n) : DivisionSemiring α where
+  toSemiring := hf.semiring f zero one add mul nsmul npow natCast
+  __ := hf.groupWithZero f zero one mul inv div npow zpow
 #align function.injective.division_semiring Function.Injective.divisionSemiring
 
-/-- Pullback a `DivisionSemiring` along an injective function.
-See note [reducible non-instances]. -/
-@[reducible]
-protected def Function.Injective.divisionRing [DivisionRing K] {K'} [Zero K'] [One K'] [Add K']
-    [Mul K'] [Neg K'] [Sub K'] [Inv K'] [Div K'] [SMul ℕ K'] [SMul ℤ K'] [SMul ℚ K']
-    [Pow K' ℕ] [Pow K' ℤ] [NatCast K'] [IntCast K'] [RatCast K'] (f : K' → K) (hf : Injective f)
-    (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y)
-    (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x)
-    (sub : ∀ x y, f (x - y) = f x - f y) (inv : ∀ x, f x⁻¹ = (f x)⁻¹)
-    (div : ∀ x y, f (x / y) = f x / f y) (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x)
-    (zsmul : ∀ (x) (n : ℤ), f (n • x) = n • f x) (qsmul : ∀ (x) (n : ℚ), f (n • x) = n • f x)
+/-- Pullback a `DivisionSemiring` along an injective function. -/
+@[reducible] -- See note [reducible non-instances]
+protected def divisionRing [DivisionRing β] (zero : f 0 = 0) (one : f 1 = 1)
+    (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
+    (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) (inv : ∀ x, f x⁻¹ = (f x)⁻¹)
+    (div : ∀ x y, f (x / y) = f x / f y)
+    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
+    (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (qsmul : ∀ (q : ℚ) (x), f (q • x) = q • f x)
     (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n)
-    (nat_cast : ∀ n : ℕ, f n = n) (int_cast : ∀ n : ℤ, f n = n) (rat_cast : ∀ n : ℚ, f n = n) :
-    DivisionRing K' :=
-  { hf.groupWithZero f zero one mul inv div npow zpow,
-    hf.ring f zero one add mul neg sub nsmul zsmul npow nat_cast int_cast with
-    ratCast := Rat.cast,
-    ratCast_mk := fun a b h1 h2 ↦
-      hf
-        (by
-          erw [rat_cast, mul, inv, int_cast, nat_cast]
-          exact DivisionRing.ratCast_mk a b h1 h2),
-    qsmul := (· • ·), qsmul_eq_mul' := fun a x ↦ hf (by erw [qsmul, mul, Rat.smul_def, rat_cast]) }
+    (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n)
+    (ratCast : ∀ q : ℚ, f q = q) : DivisionRing α where
+  toRing := hf.ring f zero one add mul neg sub nsmul zsmul npow natCast intCast
+  __ := hf.groupWithZero f zero one mul inv div npow zpow
+  __ := hf.divisionSemiring f zero one add mul inv div nsmul npow zpow natCast
+  ratCast_mk a b h1 h2 := hf $ by
+    erw [ratCast, mul, inv, intCast, natCast, Rat.cast_def, div_eq_mul_inv]
+  qsmul := (· • ·)
+  qsmul_eq_mul' q a := hf $ by erw [qsmul, mul, Rat.smul_def, ratCast]
 #align function.injective.division_ring Function.Injective.divisionRing
 
--- See note [reducible non-instances]
 /-- Pullback a `Field` along an injective function. -/
-@[reducible]
-protected def Function.Injective.semifield [Semifield β] [Zero α] [Mul α] [Add α] [One α] [Inv α]
-    [Div α] [SMul ℕ α] [Pow α ℕ] [Pow α ℤ] [NatCast α] (f : α → β) (hf : Injective f)
-    (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y)
-    (mul : ∀ x y, f (x * y) = f x * f y) (inv : ∀ x, f x⁻¹ = (f x)⁻¹)
-    (div : ∀ x y, f (x / y) = f x / f y) (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x)
+@[reducible] -- See note [reducible non-instances]
+protected def semifield [Semifield β] (zero : f 0 = 0) (one : f 1 = 1)
+    (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
+    (inv : ∀ x, f x⁻¹ = (f x)⁻¹) (div : ∀ x y, f (x / y) = f x / f y)
+    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
     (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n)
-    (nat_cast : ∀ n : ℕ, f n = n) : Semifield α :=
-  { hf.commGroupWithZero f zero one mul inv div npow zpow,
-    hf.commSemiring f zero one add mul nsmul npow nat_cast with }
+    (natCast : ∀ n : ℕ, f n = n) : Semifield α where
+  toCommSemiring := hf.commSemiring f zero one add mul nsmul npow natCast
+  __ := hf.commGroupWithZero f zero one mul inv div npow zpow
+  __ := hf.divisionSemiring f zero one add mul inv div nsmul npow zpow natCast
 #align function.injective.semifield Function.Injective.semifield
 
-/-- Pullback a `Field` along an injective function.
-See note [reducible non-instances]. -/
-@[reducible]
-protected def Function.Injective.field [Field K] {K'} [Zero K'] [Mul K'] [Add K'] [Neg K'] [Sub K']
-    [One K'] [Inv K'] [Div K'] [SMul ℕ K'] [SMul ℤ K'] [SMul ℚ K'] [Pow K' ℕ] [Pow K' ℤ]
-    [NatCast K'] [IntCast K'] [RatCast K'] (f : K' → K) (hf : Injective f) (zero : f 0 = 0)
-    (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
+/-- Pullback a `Field` along an injective function. -/
+@[reducible] -- See note [reducible non-instances]
+protected def field [Field β] (zero : f 0 = 0) (one : f 1 = 1)
+    (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
     (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y) (inv : ∀ x, f x⁻¹ = (f x)⁻¹)
-    (div : ∀ x y, f (x / y) = f x / f y) (nsmul : ∀ (x) (n : ℕ), f (n • x) = n • f x)
-    (zsmul : ∀ (x) (n : ℤ), f (n • x) = n • f x) (qsmul : ∀ (x) (n : ℚ), f (n • x) = n • f x)
+    (div : ∀ x y, f (x / y) = f x / f y)
+    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
+    (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x) (qsmul : ∀ (q : ℚ) (x), f (q • x) = q • f x)
     (npow : ∀ (x) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x) (n : ℤ), f (x ^ n) = f x ^ n)
-    (nat_cast : ∀ n : ℕ, f n = n) (int_cast : ∀ n : ℤ, f n = n) (rat_cast : ∀ n : ℚ, f n = n) :
-    Field K' :=
-  { hf.commGroupWithZero f zero one mul inv div npow zpow,
-    hf.commRing f zero one add mul neg sub nsmul zsmul npow nat_cast int_cast with
-    ratCast := Rat.cast,
-    ratCast_mk := fun a b h1 h2 ↦
-      hf
-        (by
-          erw [rat_cast, mul, inv, int_cast, nat_cast]
-          exact DivisionRing.ratCast_mk a b h1 h2),
-    qsmul := (· • ·), qsmul_eq_mul' := fun a x ↦ hf (by erw [qsmul, mul, Rat.smul_def, rat_cast]) }
+    (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n)
+    (ratCast : ∀ q : ℚ, f q = q) :
+    Field α where
+  toCommRing := hf.commRing f zero one add mul neg sub nsmul zsmul npow natCast intCast
+  __ := hf.commGroupWithZero f zero one mul inv div npow zpow
+  __ := hf.divisionSemiring f zero one add mul inv div nsmul npow zpow natCast
+  ratCast_mk a b h1 h2 := hf $ by
+    erw [ratCast, mul, inv, intCast, natCast, Rat.cast_def, div_eq_mul_inv]
+  qsmul := (· • ·)
+  qsmul_eq_mul' q a := hf $ by erw [qsmul, mul, Rat.smul_def, ratCast]
 #align function.injective.field Function.Injective.field
 
-/-! ### Order dual -/
-
-
-instance [h : RatCast α] : RatCast αᵒᵈ :=
-  h
+end Function.Injective
 
-instance [h : DivisionSemiring α] : DivisionSemiring αᵒᵈ :=
-  h
+/-! ### Order dual -/
 
-instance [h : DivisionRing α] : DivisionRing αᵒᵈ :=
-  h
+namespace OrderDual
 
-instance [h : Semifield α] : Semifield αᵒᵈ :=
-  h
+instance instRatCast [RatCast α] : RatCast αᵒᵈ := ‹_›
+instance instDivisionSemiring [DivisionSemiring α] : DivisionSemiring αᵒᵈ := ‹_›
+instance instDivisionRing [DivisionRing α] : DivisionRing αᵒᵈ := ‹_›
+instance instSemifield [Semifield α] : Semifield αᵒᵈ := ‹_›
+instance instField [Field α] : Field αᵒᵈ := ‹_›
 
-instance [h : Field α] : Field αᵒᵈ :=
-  h
+end OrderDual
 
-@[simp]
-theorem toDual_rat_cast [RatCast α] (n : ℚ) : toDual (n : α) = n :=
-  rfl
-#align to_dual_rat_cast toDual_rat_cast
+@[simp] lemma toDual_ratCast [RatCast α] (n : ℚ) : toDual (n : α) = n := rfl
+#align to_dual_rat_cast toDual_ratCast
 
-@[simp]
-theorem ofDual_rat_cast [RatCast α] (n : ℚ) : (ofDual n : α) = n :=
-  rfl
-#align of_dual_rat_cast ofDual_rat_cast
+@[simp] lemma ofDual_ratCast [RatCast α] (n : ℚ) : (ofDual n : α) = n := rfl
+#align of_dual_rat_cast ofDual_ratCast
 
 /-! ### Lexicographic order -/
 
-instance [h : RatCast α] : RatCast (Lex α) :=
-  h
-
-instance [h : DivisionSemiring α] : DivisionSemiring (Lex α) :=
-  h
+namespace Lex
 
-instance [h : DivisionRing α] : DivisionRing (Lex α) :=
-  h
+instance instRatCast [RatCast α] : RatCast (Lex α) := ‹_›
+instance instDivisionSemiring [DivisionSemiring α] : DivisionSemiring (Lex α) := ‹_›
+instance instDivisionRing [DivisionRing α] : DivisionRing (Lex α) := ‹_›
+instance instSemifield [Semifield α] : Semifield (Lex α) := ‹_›
+instance instField [Field α] : Field (Lex α) := ‹_›
 
-instance [h : Semifield α] : Semifield (Lex α) :=
-  h
+end Lex
 
-instance [h : Field α] : Field (Lex α) :=
-  h
+@[simp] lemma toLex_ratCast [RatCast α] (n : ℚ) : toLex (n : α) = n := rfl
+#align to_lex_rat_cast toLex_ratCast
 
-@[simp]
-theorem toLex_rat_cast [RatCast α] (n : ℚ) : toLex (n : α) = n :=
-  rfl
-#align to_lex_rat_cast toLex_rat_cast
-
-@[simp]
-theorem ofLex_rat_cast [RatCast α] (n : ℚ) : (ofLex n : α) = n :=
-  rfl
-#align of_lex_rat_cast ofLex_rat_cast
+@[simp] lemma ofLex_ratCast [RatCast α] (n : ℚ) : (ofLex n : α) = n := rfl
+#align of_lex_rat_cast ofLex_ratCast