chore(ring_theory/{subring,integral_closure}): simplify a proof, remove redundant instances (#6513)

Author: eric-wieser

src/field_theory/subfield.lean

@@ -196,7 +196,7 @@ instance to_field : field s :=
   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⟩,
-  ..subring.subring.domain s.to_subring }
+  ..s.to_subring.integral_domain }
 
 @[simp, norm_cast] lemma coe_add (x y : s) : (↑(x + y) : K) = ↑x + ↑y := rfl
 @[simp, norm_cast] lemma coe_neg (x : s) : (↑(-x) : K) = -↑x := rfl

src/ring_theory/integral_closure.lean

@@ -92,19 +92,14 @@ theorem is_integral_of_submodule_noetherian (S : subalgebra R A)
   (H : is_noetherian R (S : submodule R A)) (x : A) (hx : x ∈ S) :
   is_integral R x :=
 begin
-  letI : algebra R S := S.algebra,
-  letI : ring S := S.ring R A,
-  suffices : is_integral R (⟨x, hx⟩ : S),
+  suffices : is_integral R (show S, from ⟨x, hx⟩),
   { rcases this with ⟨p, hpm, hpx⟩,
-    replace hpx := congr_arg subtype.val hpx,
+    replace hpx := congr_arg S.val hpx,
     refine ⟨p, hpm, eq.trans _ hpx⟩,
     simp only [aeval_def, eval₂, finsupp.sum],
-    rw ← p.support.sum_hom subtype.val,
-    { refine finset.sum_congr rfl (λ n hn, _),
-      change _ = _ * _,
-      rw is_monoid_hom.map_pow coe, refl,
-      split; intros; refl },
-    refine { map_add := _, map_zero := _ }; intros; refl },
+    rw S.val.map_sum,
+    refine finset.sum_congr rfl (λ n hn, _),
+    rw [S.val.map_mul, S.val.map_pow, S.val.commutes, S.val_apply, subtype.coe_mk], },
   refine is_integral_of_noetherian H ⟨x, hx⟩
 end
 
@@ -562,10 +557,6 @@ section integral_domain
 variables {R S : Type*} [comm_ring R] [integral_domain S] [algebra R S]
 
 instance : integral_domain (integral_closure R S) :=
-{ exists_pair_ne := ⟨0, 1, mt subtype.ext_iff_val.mp zero_ne_one⟩,
-  eq_zero_or_eq_zero_of_mul_eq_zero := λ ⟨a, ha⟩ ⟨b, hb⟩ h,
-    or.imp subtype.ext_iff_val.mpr subtype.ext_iff_val.mpr
-    (eq_zero_or_eq_zero_of_mul_eq_zero (subtype.ext_iff_val.mp h)),
-  ..(integral_closure R S).comm_ring R S }
+infer_instance
 
 end integral_domain

src/ring_theory/subring.lean

@@ -242,6 +242,18 @@ instance to_ring : ring s :=
 instance to_comm_ring {R} [comm_ring R] (s : subring R) : comm_ring s :=
 { mul_comm := λ _ _, subtype.eq $ mul_comm _ _, ..subring.to_ring s}
 
+/-- A subring of a non-trivial ring is non-trivial. -/
+instance {R} [ring R] [nontrivial R] (s : subring R) : nontrivial s :=
+s.to_subsemiring.nontrivial
+
+/-- A subring of a ring with no zero divisors has no zero divisors. -/
+instance {R} [ring R] [no_zero_divisors R] (s : subring R) : no_zero_divisors s :=
+s.to_subsemiring.no_zero_divisors
+
+/-- A subring of an integral domain is an integral domain. -/
+instance {R} [integral_domain R] (s : subring R) : integral_domain s :=
+{ .. s.nontrivial, .. s.no_zero_divisors, .. s.to_comm_ring }
+
 /-- The natural ring hom from a subring of ring `R` to `R`. -/
 def subtype (s : subring R) : s →+* R :=
 { to_fun := coe,
@@ -363,24 +375,6 @@ end ring_hom
 
 namespace subring
 
-variables {cR : Type u} [comm_ring cR]
-
-/-- A subring of a commutative ring is a commutative ring. -/
-def subset_comm_ring (S : subring cR) : comm_ring S :=
-{mul_comm := λ _ _, subtype.eq $ mul_comm _ _, ..subring.to_ring S}
-
-/-- A subring of a non-trivial ring is non-trivial. -/
-instance {D : Type*} [ring D] [nontrivial D] (S : subring D) : nontrivial S :=
-S.to_subsemiring.nontrivial
-
-/-- A subring of a ring with no zero divisors has no zero divisors. -/
-instance {D : Type*} [ring D] [no_zero_divisors D] (S : subring D) : no_zero_divisors S :=
-S.to_subsemiring.no_zero_divisors
-
-/-- A subring of an integral domain is an integral domain. -/
-instance subring.domain {D : Type*} [integral_domain D] (S : subring D) : integral_domain S :=
-{ .. S.nontrivial, .. S.no_zero_divisors, .. S.subset_comm_ring }
-
 /-! # bot -/
 
 instance : has_bot (subring R) := ⟨(int.cast_ring_hom R).range⟩