feat(*): make more non-instances reducible (#8941)

* Also add some docstrings to `cau_seq_completion`.
* Related PR: #7835

src/algebra/algebra/basic.lean

@@ -301,7 +301,9 @@ variables [comm_ring R]
 
 variables (R)
 
-/-- A `semiring` that is an `algebra` over a commutative ring carries a natural `ring` structure. -/
+/-- A `semiring` that is an `algebra` over a commutative ring carries a natural `ring` structure.
+See note [reducible non-instances]. -/
+@[reducible]
 def semiring_to_ring [semiring A] [algebra R A] : ring A := {
   ..module.add_comm_monoid_to_add_comm_group R,
   ..(infer_instance : semiring A) }

src/algebra/direct_limit.lean

@@ -562,7 +562,9 @@ by rw [inv, dif_neg hp, classical.some_spec (direct_limit.exists_inv G f hp)]
 protected theorem inv_mul_cancel {p : ring.direct_limit G f} (hp : p ≠ 0) : inv G f p * p = 1 :=
 by rw [_root_.mul_comm, direct_limit.mul_inv_cancel G f hp]
 
-/-- Noncomputable field structure on the direct limit of fields. -/
+/-- Noncomputable field structure on the direct limit of fields.
+See note [reducible non-instances]. -/
+@[reducible]
 protected noncomputable def field [directed_system G (λ i j h, f' i j h)] :
   field (ring.direct_limit G (λ i j h, f' i j h)) :=
 { inv := inv G (λ i j h, f' i j h),

src/algebra/group/defs.lean

@@ -707,8 +707,8 @@ attribute [to_additive] group
 
 Useful because it corresponds to the fact that `Grp` is a subcategory of `Mon`.
 Not an instance since it duplicates `@div_inv_monoid.to_monoid _ (@group.to_div_inv_monoid _ _)`.
--/
-@[to_additive
+See note [reducible non-instances]. -/
+@[reducible, to_additive
 "Abbreviation for `@sub_neg_monoid.to_add_monoid _ (@add_group.to_sub_neg_monoid _ _)`.
 
 Useful because it corresponds to the fact that `AddGroup` is a subcategory of `AddMon`.

src/algebra/module/basic.lean

@@ -145,7 +145,9 @@ end add_comm_monoid
 variables (R)
 
 /-- An `add_comm_monoid` that is a `module` over a `ring` carries a natural `add_comm_group`
-structure. -/
+structure.
+See note [reducible non-instances]. -/
+@[reducible]
 def module.add_comm_monoid_to_add_comm_group [ring R] [add_comm_monoid M] [module R M] :
   add_comm_group M :=
 { neg          := λ a, (-1 : R) • a,

src/category_theory/monoidal/skeleton.lean

@@ -21,7 +21,9 @@ universes v u
 
 variables {C : Type u} [category.{v} C] [monoidal_category C]
 
-/-- If `C` is monoidal and skeletal, it is a monoid. -/
+/-- If `C` is monoidal and skeletal, it is a monoid.
+See note [reducible non-instances]. -/
+@[reducible]
 def monoid_of_skeletal_monoidal (hC : skeletal C) : monoid C :=
 { mul := λ X Y, (X ⊗ Y : C),
   one := (𝟙_ C : C),

src/data/real/cau_seq_completion.lean

@@ -19,14 +19,17 @@ section
 parameters {α : Type*} [linear_ordered_field α]
 parameters {β : Type*} [comm_ring β] {abv : β → α} [is_absolute_value abv]
 
+/-- The Cauchy completion of a commutative ring with absolute value. -/
 def Cauchy := @quotient (cau_seq _ abv) cau_seq.equiv
 
+/-- The map from Cauchy sequences into the Cauchy completion. -/
 def mk : cau_seq _ abv → Cauchy := quotient.mk
 
 @[simp] theorem mk_eq_mk (f) : @eq Cauchy ⟦f⟧ (mk f) := rfl
 
 theorem mk_eq {f g} : mk f = mk g ↔ f ≈ g := quotient.eq
 
+/-- The map from the original ring into the Cauchy completion. -/
 def of_rat (x : β) : Cauchy := mk (const abv x)
 
 instance : has_zero Cauchy := ⟨of_rat 0⟩
@@ -139,6 +142,9 @@ quotient.induction_on x $ λ f hf, begin
   exact quotient.sound (cau_seq.inv_mul_cancel hf)
 end
 
+/-- The Cauchy completion forms a field.
+See note [reducible non-instances]. -/
+@[reducible]
 noncomputable def field : field Cauchy :=
 { inv              := has_inv.inv,
   mul_inv_cancel   := λ x x0, by rw [mul_comm, cau_seq.completion.inv_mul_cancel x0],
@@ -163,6 +169,8 @@ section
 
 variables (β : Type*) [ring β] (abv : β → α) [is_absolute_value abv]
 
+/-- A class stating that a ring with an absolute value is complete, i.e. every Cauchy
+sequence has a limit. -/
 class is_complete :=
 (is_complete : ∀ s : cau_seq β abv, ∃ b : β, s ≈ const abv b)
 end
@@ -175,7 +183,9 @@ variable [is_complete β abv]
 lemma complete : ∀ s : cau_seq β abv, ∃ b : β, s ≈ const abv b :=
 is_complete.is_complete
 
-noncomputable def lim (s : cau_seq β abv) := classical.some (complete s)
+/-- The limit of a Cauchy sequence in a complete ring. Chosen non-computably. -/
+noncomputable def lim (s : cau_seq β abv) : β :=
+classical.some (complete s)
 
 lemma equiv_lim (s : cau_seq β abv) : s ≈ const abv (lim s) :=
 classical.some_spec (complete s)

src/ring_theory/ideal/basic.lean

@@ -544,7 +544,9 @@ begin
 end
 
 /-- quotient by maximal ideal is a field. def rather than instance, since users will have
-computable inverses in some applications -/
+computable inverses in some applications.
+See note [reducible non-instances]. -/
+@[reducible]
 protected noncomputable def field (I : ideal α) [hI : I.is_maximal] : field I.quotient :=
 { inv := λ a, if ha : a = 0 then 0 else classical.some (exists_inv ha),
   mul_inv_cancel := λ a (ha : a ≠ 0), show a * dite _ _ _ = _,

src/ring_theory/localization.lean

@@ -1235,7 +1235,9 @@ begin
 end
 
 /-- A `comm_ring` `S` which is the localization of an integral domain `R` at a subset of
-non-zero elements is an integral domain. -/
+non-zero elements is an integral domain.
+See note [reducible non-instances]. -/
+@[reducible]
 def integral_domain_of_le_non_zero_divisors [algebra A S] {M : submonoid A} [is_localization M S]
   (hM : M ≤ non_zero_divisors A) : integral_domain S :=
 { eq_zero_or_eq_zero_of_mul_eq_zero :=
@@ -1255,7 +1257,9 @@ def integral_domain_of_le_non_zero_divisors [algebra A S] {M : submonoid A} [is_
                      λ h, zero_ne_one (is_localization.injective S hM h)⟩,
   .. ‹comm_ring S› }
 
-/-- The localization at of an integral domain to a set of non-zero elements is an integral domain -/
+/-- The localization at of an integral domain to a set of non-zero elements is an integral domain.
+See note [reducible non-instances]. -/
+@[reducible]
 def integral_domain_localization {M : submonoid A} (hM : M ≤ non_zero_divisors A) :
   integral_domain (localization M) :=
 integral_domain_of_le_non_zero_divisors _ hM
@@ -1507,8 +1511,9 @@ show x * dite _ _ _ = 1, by rw [dif_neg hx,
     λ h0, hx $ eq_zero_of_fst_eq_zero (sec_spec (non_zero_divisors A) x) h0⟩),
   one_mul, mul_assoc, mk'_spec, ←eq_mk'_iff_mul_eq]; exact (mk'_sec _ x).symm
 
-/-- A `comm_ring` `K` which is the localization of an integral domain `R` at `R - {0}` is a
-field. -/
+/-- A `comm_ring` `K` which is the localization of an integral domain `R` at `R - {0}` is a field.
+See note [reducible non-instances]. -/
+@[reducible]
 noncomputable def to_field : field K :=
 { inv := is_fraction_ring.inv A,
   mul_inv_cancel := is_fraction_ring.mul_inv_cancel A,