feat(algebra/category/*): get rid of the local reducible hack (#3354)

I thought I did this back in April, but apparently never made the PR.

We currently use a strange hack when setting up concrete categories, making them locally reducible. There's a library note about this, which ends:

```
TODO: Probably @[derive] should be able to create instances of the	
required form (without `id`), and then we could use that instead of	
this obscure `local attribute [reducible]` method.
```

This PR makes the small change required to `delta_instance` to make this happen, and then stops using the hack in setting up concrete categories (and deletes the library note explaining this hack).



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>

Author: kim-em

src/algebra/category/CommRing/basic.lean

@@ -15,11 +15,6 @@ We introduce the bundled categories:
 * `CommSemiRing`
 * `CommRing`
 along with the relevant forgetful functors between them.
-
-## Implementation notes
-
-See the note [locally reducible category instances].
-
 -/
 
 universes u v
@@ -31,23 +26,18 @@ def SemiRing : Type (u+1) := bundled semiring
 
 namespace SemiRing
 
+instance bundled_hom : bundled_hom @ring_hom :=
+⟨@ring_hom.to_fun, @ring_hom.id, @ring_hom.comp, @ring_hom.coe_inj⟩
+
+attribute [derive [has_coe_to_sort, large_category, concrete_category]] SemiRing
+
 /-- Construct a bundled SemiRing from the underlying type and typeclass. -/
 def of (R : Type u) [semiring R] : SemiRing := bundled.of R
 
 instance : inhabited SemiRing := ⟨of punit⟩
 
-local attribute [reducible] SemiRing
-
-instance : has_coe_to_sort SemiRing := infer_instance -- short-circuit type class inference
-
 instance (R : SemiRing) : semiring R := R.str
 
-instance bundled_hom : bundled_hom @ring_hom :=
-⟨@ring_hom.to_fun, @ring_hom.id, @ring_hom.comp, @ring_hom.coe_inj⟩
-
-instance : category SemiRing := infer_instance -- short-circuit type class inference
-instance : concrete_category SemiRing := infer_instance -- short-circuit type class inference
-
 instance has_forget_to_Mon : has_forget₂ SemiRing Mon :=
 bundled_hom.mk_has_forget₂
   (λ R hR, @monoid_with_zero.to_monoid R (@semiring.to_monoid_with_zero R hR))
@@ -68,20 +58,15 @@ namespace Ring
 
 instance : bundled_hom.parent_projection @ring.to_semiring := ⟨⟩
 
+attribute [derive [has_coe_to_sort, large_category, concrete_category]] Ring
+
 /-- Construct a bundled Ring from the underlying type and typeclass. -/
 def of (R : Type u) [ring R] : Ring := bundled.of R
 
 instance : inhabited Ring := ⟨of punit⟩
 
-local attribute [reducible] Ring
-
-instance : has_coe_to_sort Ring := by apply_instance -- short-circuit type class inference
-
 instance (R : Ring) : ring R := R.str
 
-instance : category Ring := infer_instance -- short-circuit type class inference
-instance : concrete_category Ring := infer_instance -- short-circuit type class inference
-
 instance has_forget_to_SemiRing : has_forget₂ Ring SemiRing := bundled_hom.forget₂ _ _
 instance has_forget_to_AddCommGroup : has_forget₂ Ring AddCommGroup :=
 -- can't use bundled_hom.mk_has_forget₂, since AddCommGroup is an induced category
@@ -98,20 +83,15 @@ namespace CommSemiRing
 
 instance : bundled_hom.parent_projection @comm_semiring.to_semiring := ⟨⟩
 
+attribute [derive [has_coe_to_sort, large_category, concrete_category]] CommSemiRing
+
 /-- Construct a bundled CommSemiRing from the underlying type and typeclass. -/
 def of (R : Type u) [comm_semiring R] : CommSemiRing := bundled.of R
 
 instance : inhabited CommSemiRing := ⟨of punit⟩
 
-local attribute [reducible] CommSemiRing
-
-instance : has_coe_to_sort CommSemiRing := infer_instance -- short-circuit type class inference
-
 instance (R : CommSemiRing) : comm_semiring R := R.str
 
-instance : category CommSemiRing := infer_instance -- short-circuit type class inference
-instance : concrete_category CommSemiRing := infer_instance -- short-circuit type class inference
-
 instance has_forget_to_SemiRing : has_forget₂ CommSemiRing SemiRing := bundled_hom.forget₂ _ _
 
 /-- The forgetful functor from commutative rings to (multiplicative) commutative monoids. -/
@@ -129,20 +109,15 @@ namespace CommRing
 
 instance : bundled_hom.parent_projection @comm_ring.to_ring := ⟨⟩
 
+attribute [derive [has_coe_to_sort, large_category, concrete_category]] CommRing
+
 /-- Construct a bundled CommRing from the underlying type and typeclass. -/
 def of (R : Type u) [comm_ring R] : CommRing := bundled.of R
 
 instance : inhabited CommRing := ⟨of punit⟩
 
-local attribute [reducible] CommRing
-
-instance : has_coe_to_sort CommRing := infer_instance -- short-circuit type class inference
-
 instance (R : CommRing) : comm_ring R := R.str
 
-instance : category CommRing := infer_instance -- short-circuit type class inference
-instance : concrete_category CommRing := infer_instance -- short-circuit type class inference
-
 instance has_forget_to_Ring : has_forget₂ CommRing Ring := bundled_hom.forget₂ _ _
 
 /-- The forgetful functor from commutative rings to (multiplicative) commutative monoids. -/

src/algebra/category/Group/basic.lean

@@ -15,10 +15,6 @@ We introduce the bundled categories:
 * `CommGroup`
 * `AddCommGroup`
 along with the relevant forgetful functors between them, and to the bundled monoid categories.
-
-## Implementation notes
-
-See the note [locally reducible category instances].
 -/
 
 universes u v
@@ -37,17 +33,14 @@ namespace Group
 @[to_additive]
 instance : bundled_hom.parent_projection group.to_monoid := ⟨⟩
 
+attribute [derive [has_coe_to_sort, large_category, concrete_category]] Group AddGroup
+
 /-- Construct a bundled `Group` from the underlying type and typeclass. -/
 @[to_additive] def of (X : Type u) [group X] : Group := bundled.of X
 
 /-- Construct a bundled `AddGroup` from the underlying type and typeclass. -/
 add_decl_doc AddGroup.of
 
-local attribute [reducible] Group
-
-@[to_additive]
-instance : has_coe_to_sort Group := infer_instance -- short-circuit type class inference
-
 @[to_additive add_group]
 instance (G : Group) : group G := G.str
 
@@ -65,13 +58,7 @@ instance : unique (1 : Group) :=
 @[simp, to_additive]
 lemma one_apply (G H : Group) (g : G) : (1 : G ⟶ H) g = 1 := rfl
 
-@[to_additive]
-instance : category Group := infer_instance -- short-circuit type class inference
-
-@[to_additive]
-instance : concrete_category Group := infer_instance -- short-circuit type class inference
-
-@[to_additive,ext]
+@[to_additive, ext]
 lemma ext (G H : Group) (f₁ f₂ : G ⟶ H) (w : ∀ x, f₁ x = f₂ x) : f₁ = f₂ :=
 by { ext1, apply w }
 
@@ -97,17 +84,14 @@ namespace CommGroup
 @[to_additive]
 instance : bundled_hom.parent_projection comm_group.to_group := ⟨⟩
 
+attribute [derive [has_coe_to_sort, large_category, concrete_category]] CommGroup AddCommGroup
+
 /-- Construct a bundled `CommGroup` from the underlying type and typeclass. -/
 @[to_additive] def of (G : Type u) [comm_group G] : CommGroup := bundled.of G
 
 /-- Construct a bundled `AddCommGroup` from the underlying type and typeclass. -/
 add_decl_doc AddCommGroup.of
 
-local attribute [reducible] CommGroup
-
-@[to_additive]
-instance : has_coe_to_sort CommGroup := infer_instance -- short-circuit type class inference
-
 @[to_additive add_comm_group_instance]
 instance comm_group_instance (G : CommGroup) : comm_group G := G.str
 
@@ -123,12 +107,6 @@ instance : unique (1 : CommGroup) :=
 @[simp, to_additive]
 lemma one_apply (G H : CommGroup) (g : G) : (1 : G ⟶ H) g = 1 := rfl
 
-@[to_additive]
-instance : category CommGroup := infer_instance -- short-circuit type class inference
-
-@[to_additive]
-instance : concrete_category CommGroup := infer_instance -- short-circuit type class inference
-
 @[to_additive,ext]
 lemma ext (G H : CommGroup) (f₁ f₂ : G ⟶ H) (w : ∀ x, f₁ x = f₂ x) : f₁ = f₂ :=
 by { ext1, apply w }

src/algebra/category/Mon/basic.lean

@@ -15,34 +15,7 @@ We introduce the bundled categories:
 * `CommMon`
 * `AddCommMon`
 along with the relevant forgetful functors between them.
-
-## Implementation notes
-
-See the note [locally reducible category instances].
--/
-
-/--
-We make SemiRing (and the other categories) locally reducible in order
-to define its instances. This is because writing, for example,
-
-```
-instance : concrete_category SemiRing := by { delta SemiRing, apply_instance }
-```
-
-results in an instance of the form `id (bundled_hom.concrete_category _)`
-and this `id`, not being [reducible], prevents a later instance search
-(once SemiRing is no longer reducible) from seeing that the morphisms of
-SemiRing are really semiring morphisms (`→+*`), and therefore have a coercion
-to functions, for example. It's especially important that the `has_coe_to_sort`
-instance not contain an extra `id` as we want the `semiring ↥R` instance to
-also apply to `semiring R.α` (it seems to be impractical to guarantee that
-we always access `R.α` through the coercion rather than directly).
-
-TODO: Probably @[derive] should be able to create instances of the
-required form (without `id`), and then we could use that instead of
-this obscure `local attribute [reducible]` method.
 -/
-library_note "locally reducible category instances"
 
 universes u v
 
@@ -57,11 +30,17 @@ add_decl_doc AddMon
 
 namespace Mon
 
+@[to_additive]
+instance bundled_hom : bundled_hom @monoid_hom :=
+⟨@monoid_hom.to_fun, @monoid_hom.id, @monoid_hom.comp, @monoid_hom.coe_inj⟩
+
+attribute [derive [has_coe_to_sort, large_category, concrete_category]] Mon AddMon
+
 /-- Construct a bundled `Mon` from the underlying type and typeclass. -/
 @[to_additive]
 def of (M : Type u) [monoid M] : Mon := bundled.of M
 
-/-- Construct a bundled Mon from the underlying type and typeclass. -/
+/-- Construct a bundled `Mon` from the underlying type and typeclass. -/
 add_decl_doc AddMon.of
 
 @[to_additive]
@@ -70,24 +49,9 @@ instance : inhabited Mon :=
 -- which breaks to_additive.
 ⟨@of punit $ @group.to_monoid _ $ @comm_group.to_group _ punit.comm_group⟩
 
-local attribute [reducible] Mon
-
-@[to_additive]
-instance : has_coe_to_sort Mon := infer_instance -- short-circuit type class inference
-
 @[to_additive add_monoid]
 instance (M : Mon) : monoid M := M.str
 
-@[to_additive]
-instance bundled_hom : bundled_hom @monoid_hom :=
-⟨@monoid_hom.to_fun, @monoid_hom.id, @monoid_hom.comp, @monoid_hom.coe_inj⟩
-
-@[to_additive]
-instance : category Mon := infer_instance -- short-circuit type class inference
-
-@[to_additive]
-instance : concrete_category Mon := infer_instance -- short-circuit type class inference
-
 end Mon
 
 /-- The category of commutative monoids and monoid morphisms. -/
@@ -102,6 +66,8 @@ namespace CommMon
 @[to_additive]
 instance : bundled_hom.parent_projection comm_monoid.to_monoid := ⟨⟩
 
+attribute [derive [has_coe_to_sort, large_category, concrete_category]] CommMon AddCommMon
+
 /-- Construct a bundled `CommMon` from the underlying type and typeclass. -/
 @[to_additive]
 def of (M : Type u) [comm_monoid M] : CommMon := bundled.of M
@@ -115,20 +81,9 @@ instance : inhabited CommMon :=
 -- which breaks to_additive.
 ⟨@of punit $ @comm_group.to_comm_monoid _ punit.comm_group⟩
 
-local attribute [reducible] CommMon
-
-@[to_additive]
-instance : has_coe_to_sort CommMon := infer_instance -- short-circuit type class inference
-
 @[to_additive add_comm_monoid]
 instance (M : CommMon) : comm_monoid M := M.str
 
-@[to_additive]
-instance : category CommMon := infer_instance -- short-circuit type class inference
-
-@[to_additive]
-instance : concrete_category CommMon := infer_instance -- short-circuit type class inference
-
 @[to_additive has_forget_to_AddMon]
 instance has_forget_to_Mon : has_forget₂ CommMon Mon := bundled_hom.forget₂ _ _
 

src/computability/halting.lean

@@ -181,7 +181,7 @@ begin
   simp at e,
   by_cases eval c ∈ C,
   { simp [h] at e, rwa ← e },
-  { simp at h, simp [h] at e,
+  { simp [h] at e,
     rw e at h, contradiction }
 end
 

src/linear_algebra/finsupp.lean

@@ -181,13 +181,9 @@ begin
   rintro l ⟨⟩,
   apply finsupp.induction l, {exact zero_mem _},
   refine λ x a l hl a0, add_mem _ _,
-  haveI := classical.dec_pred (λ x, ∃ i, x ∈ s i),
   by_cases (∃ i, x ∈ s i); simp [h],
   { cases h with i hi,
-    exact le_supr (λ i, supported M R (s i)) i (single_mem_supported R _ hi) },
-  { rw filter_single_of_neg,
-    { simp },
-    { exact h } }
+    exact le_supr (λ i, supported M R (s i)) i (single_mem_supported R _ hi) }
 end
 
 theorem supported_union (s t : set α) :

src/measure_theory/category/Meas.lean

@@ -28,7 +28,8 @@ noncomputable theory
 open category_theory measure_theory
 universes u v
 
-@[reducible] def Meas : Type (u+1) := bundled measurable_space
+@[derive has_coe_to_sort]
+def Meas : Type (u+1) := bundled measurable_space
 
 namespace Meas
 
@@ -39,6 +40,10 @@ def of (α : Type u) [measurable_space α] : Meas := ⟨α⟩
 
 instance unbundled_hom : unbundled_hom @measurable := ⟨@measurable_id, @measurable.comp⟩
 
+attribute [derive [large_category, concrete_category]] Meas
+
+instance : inhabited Meas := ⟨Meas.of empty⟩
+
 /-- `Measure X` is the measurable space of measures over the measurable space `X`. It is the
 weakest measurable space, s.t. λμ, μ s is measurable for all measurable sets `s` in `X`. An
 important purpose is to assign a monadic structure on it, the Giry monad. In the Giry monad,

src/tactic/basic.lean

@@ -1,6 +1,7 @@
 import tactic.alias
 import tactic.clear
 import tactic.converter.apply_congr
+import tactic.delta_instance
 import tactic.elide
 import tactic.explode
 import tactic.find