chore(*/sub*): tidy up inherited algebraic structures from parent obj…

…ects (#6509)

This changes `subfield.to_field` to ensure that division is defeq.

It also removes `subring.subset_comm_ring` which was identical to `subring.to_comm_ring`, renames some `subalgebra` instances to match those of `subring`s, and cleans up a few related proofs that relied on the old names.

These are cleanups split from #6489, which failed CI but was otherwise approved

src/algebra/algebra/subalgebra.lean

@@ -148,14 +148,25 @@ instance {R : Type u} {A : Type v} [comm_ring R] [ring A] [algebra R A] (S : sub
 { neg_mem := λ _, S.neg_mem }
 
 instance : inhabited S := ⟨0⟩
-instance (R : Type u) (A : Type v) [comm_semiring R] [semiring A]
-  [algebra R A] (S : subalgebra R A) : semiring S := subsemiring.to_semiring S
-instance (R : Type u) (A : Type v) [comm_semiring R] [comm_semiring A]
-  [algebra R A] (S : subalgebra R A) : comm_semiring S := subsemiring.to_comm_semiring S
-instance (R : Type u) (A : Type v) [comm_ring R] [ring A]
-  [algebra R A] (S : subalgebra R A) : ring S := @@subtype.ring _ S.is_subring
-instance (R : Type u) (A : Type v) [comm_ring R] [comm_ring A]
-  [algebra R A] (S : subalgebra R A) : comm_ring S := @@subtype.comm_ring _ S.is_subring
+
+section
+
+/-! `subalgebra`s inherit structure from their `subsemiring` / `semiring` coercions. -/
+
+instance to_semiring {R A}
+  [comm_semiring R] [semiring A] [algebra R A] (S : subalgebra R A) :
+  semiring S := S.to_subsemiring.to_semiring
+instance to_comm_semiring {R A}
+  [comm_semiring R] [comm_semiring A] [algebra R A] (S : subalgebra R A) :
+  comm_semiring S := S.to_subsemiring.to_comm_semiring
+instance to_ring {R A}
+  [comm_ring R] [ring A] [algebra R A] (S : subalgebra R A) :
+  ring S := S.to_subring.to_ring
+instance to_comm_ring {R A}
+  [comm_ring R] [comm_ring A] [algebra R A] (S : subalgebra R A) :
+  comm_ring S := S.to_subring.to_comm_ring
+
+end
 
 instance algebra : algebra R S :=
 { smul := λ (c:R) x, ⟨c • x.1, S.smul_mem x.2 c⟩,

src/field_theory/subfield.lean

@@ -190,17 +190,20 @@ lemma gsmul_mem {x : K} (hx : x ∈ s) (n : ℤ) :
 lemma coe_int_mem (n : ℤ) : (n : K) ∈ s :=
 by simp only [← gsmul_one, gsmul_mem, one_mem]
 
+instance : ring s := s.to_subring.to_ring
+instance : has_div s := ⟨λ x y, ⟨x / y, s.div_mem x.2 y.2⟩⟩
+instance : has_inv s := ⟨λ x, ⟨x⁻¹, s.inv_mem x.2⟩⟩
+
 /-- A subfield inherits a field structure -/
 instance to_field : field s :=
-{ inv := λ x, ⟨x⁻¹, s.inv_mem x.2⟩,
-  inv_zero := subtype.ext inv_zero,
-  mul_inv_cancel := λ x hx, subtype.ext (mul_inv_cancel (mt s.to_subring.coe_eq_zero_iff.mp hx)),
-  exists_pair_ne := ⟨⟨0, s.zero_mem⟩, ⟨1, s.one_mem⟩, mt subtype.mk_eq_mk.mp zero_ne_one⟩,
-  ..s.to_subring.integral_domain }
+subtype.coe_injective.field coe
+  rfl rfl (λ _ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl)
 
 @[simp, norm_cast] lemma coe_add (x y : s) : (↑(x + y) : K) = ↑x + ↑y := rfl
+@[simp, norm_cast] lemma coe_sub (x y : s) : (↑(x - y) : K) = ↑x - ↑y := rfl
 @[simp, norm_cast] lemma coe_neg (x : s) : (↑(-x) : K) = -↑x := rfl
 @[simp, norm_cast] lemma coe_mul (x y : s) : (↑(x * y) : K) = ↑x * ↑y := rfl
+@[simp, norm_cast] lemma coe_div (x y : s) : (↑(x / y) : K) = ↑x / ↑y := rfl
 @[simp, norm_cast] lemma coe_inv (x : s) : (↑(x⁻¹) : K) = (↑x)⁻¹ := rfl
 @[simp, norm_cast] lemma coe_zero : ((0 : s) : K) = 0 := rfl
 @[simp, norm_cast] lemma coe_one : ((1 : s) : K) = 1 := rfl

src/group_theory/subgroup.lean

@@ -299,16 +299,12 @@ attribute [norm_cast] add_subgroup.coe_add add_subgroup.coe_zero
 /-- A subgroup of a group inherits a group structure. -/
 @[to_additive "An `add_subgroup` of an `add_group` inherits an `add_group` structure."]
 instance to_group {G : Type*} [group G] (H : subgroup G) : group H :=
-{ inv := has_inv.inv,
-  div := (/),
-  div_eq_mul_inv := λ x y, subtype.eq $ div_eq_mul_inv x y,
-  mul_left_inv := λ x, subtype.eq $ mul_left_inv x,
-  .. H.to_submonoid.to_monoid }
+subtype.coe_injective.group_div _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl)
 
 /-- A subgroup of a `comm_group` is a `comm_group`. -/
 @[to_additive "An `add_subgroup` of an `add_comm_group` is an `add_comm_group`."]
 instance to_comm_group {G : Type*} [comm_group G] (H : subgroup G) : comm_group H :=
-{ mul_comm := λ _ _, subtype.eq $ mul_comm _ _, .. H.to_group}
+subtype.coe_injective.comm_group_div _ rfl (λ _ _, rfl) (λ _, rfl) (λ _ _, rfl)
 
 /-- The natural group hom from a subgroup of group `G` to `G`. -/
 @[to_additive "The natural group hom from an `add_subgroup` of `add_group` `G` to `G`."]