refactor(category_theory/limits): use auto_param (#6696)

Add an `auto_param`, making it slightly more convenient when build limits of particular shapes first, then all limits.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/limits/constructions/over/default.lean

@@ -37,8 +37,7 @@ begin
   { apply @has_equalizers_of_pullbacks_and_binary_products _ _ _ _,
     { haveI : has_pullbacks C := ⟨by apply_instance⟩,
       exact construct_products.over_binary_product_of_pullback },
-    { split,
-      apply_instance} }
+    { apply_instance, } }
 end
 
 instance has_limits {B : C} [has_wide_pullbacks C] : has_limits (over B) :=
@@ -48,8 +47,7 @@ begin
   { apply @has_equalizers_of_pullbacks_and_binary_products _ _ _ _,
     { haveI : has_pullbacks C := ⟨by apply_instance⟩,
       exact construct_products.over_binary_product_of_pullback },
-    { split,
-      apply_instance } }
+    { apply_instance, } }
 end
 
 end category_theory.over

src/category_theory/limits/functor_category.lean

@@ -138,11 +138,9 @@ instance functor_category_has_colimits_of_shape
   { cocone := combine_cocones _ (λ k, get_colimit_cocone _),
     is_colimit := combined_is_colimit _ _ } }
 
-instance functor_category_has_limits [has_limits C] : has_limits (K ⥤ C) :=
-{ has_limits_of_shape := λ J 𝒥, by resetI; apply_instance }
+instance functor_category_has_limits [has_limits C] : has_limits (K ⥤ C) := {}
 
-instance functor_category_has_colimits [has_colimits C] : has_colimits (K ⥤ C) :=
-{ has_colimits_of_shape := λ J 𝒥, by resetI; apply_instance }
+instance functor_category_has_colimits [has_colimits C] : has_colimits (K ⥤ C) := {}
 
 instance evaluation_preserves_limits_of_shape [has_limits_of_shape J C] (k : K) :
   preserves_limits_of_shape J ((evaluation K C).obj k) :=

src/category_theory/limits/limits.lean

@@ -922,11 +922,12 @@ variables (J C)
 
 /-- `C` has limits of shape `J` if there exists a limit for every functor `F : J ⥤ C`. -/
 class has_limits_of_shape : Prop :=
-(has_limit : Π F : J ⥤ C, has_limit F)
+(has_limit : Π F : J ⥤ C, has_limit F . tactic.apply_instance)
 
 /-- `C` has all (small) limits if it has limits of every shape. -/
 class has_limits : Prop :=
-(has_limits_of_shape : Π (J : Type v) [𝒥 : small_category J], has_limits_of_shape J C)
+(has_limits_of_shape :
+  Π (J : Type v) [𝒥 : small_category J], has_limits_of_shape J C . tactic.apply_instance)
 
 variables {J C}
 
@@ -1327,11 +1328,12 @@ variables (J C)
 
 /-- `C` has colimits of shape `J` if there exists a colimit for every functor `F : J ⥤ C`. -/
 class has_colimits_of_shape : Prop :=
-(has_colimit : Π F : J ⥤ C, has_colimit F)
+(has_colimit : Π F : J ⥤ C, has_colimit F . tactic.apply_instance)
 
 /-- `C` has all (small) colimits if it has colimits of every shape. -/
 class has_colimits : Prop :=
-(has_colimits_of_shape : Π (J : Type v) [𝒥 : small_category J], has_colimits_of_shape J C)
+(has_colimits_of_shape :
+  Π (J : Type v) [𝒥 : small_category J], has_colimits_of_shape J C . tactic.apply_instance)
 
 variables {J C}
 

src/category_theory/limits/opposites.lean

@@ -59,8 +59,7 @@ local attribute [instance] has_limits_of_shape_op_of_has_colimits_of_shape
 /--
 If `C` has colimits, we can construct limits for `Cᵒᵖ`.
 -/
-lemma has_limits_op_of_has_colimits [has_colimits C] : has_limits Cᵒᵖ :=
-{ has_limits_of_shape := λ J 𝒥, by { resetI, apply_instance } }
+lemma has_limits_op_of_has_colimits [has_colimits C] : has_limits Cᵒᵖ := {}
 
 /--
 If `F.left_op : Jᵒᵖ ⥤ C` has a limit, we can construct a colimit for `F : J ⥤ Cᵒᵖ`.
@@ -98,8 +97,7 @@ local attribute [instance] has_colimits_of_shape_op_of_has_limits_of_shape
 /--
 If `C` has limits, we can construct colimits for `Cᵒᵖ`.
 -/
-lemma has_colimits_op_of_has_limits [has_limits C] : has_colimits Cᵒᵖ :=
-{ has_colimits_of_shape := λ J 𝒥, by { resetI, apply_instance } }
+lemma has_colimits_op_of_has_limits [has_limits C] : has_colimits Cᵒᵖ := {}
 
 variables (X : Type v)
 /--

src/category_theory/limits/over.lean

@@ -78,10 +78,9 @@ has_colimit_of_created _ (forget X)
 
 instance has_colimits_of_shape [has_colimits_of_shape J C] :
   has_colimits_of_shape J (over X) :=
-{ has_colimit := λ F, by apply_instance }
+{}
 
-instance has_colimits [has_colimits C] : has_colimits (over X) :=
-{ has_colimits_of_shape := λ J 𝒥, by apply_instance }
+instance has_colimits [has_colimits C] : has_colimits (over X) := {}
 
 -- We can automatically infer that the forgetful functor preserves colimits
 example [has_colimits C] : preserves_colimits (forget X) := infer_instance
@@ -174,10 +173,9 @@ has_limit_of_created F (forget X)
 
 instance has_limits_of_shape [has_limits_of_shape J C] :
   has_limits_of_shape J (under X) :=
-{ has_limit := λ F, by apply_instance }
+{}
 
-instance has_limits [has_limits C] : has_limits (under X) :=
-{ has_limits_of_shape := λ J 𝒥, by resetI; apply_instance }
+instance has_limits [has_limits C] : has_limits (under X) := {}
 
 -- We can automatically infer that the forgetful functor preserves limits
 example [has_limits C] : preserves_limits (forget X) := infer_instance

src/category_theory/limits/shapes/kernels.lean

@@ -653,20 +653,20 @@ variables [has_zero_morphisms C]
 
 /-- `has_kernels` represents the existence of kernels for every morphism. -/
 class has_kernels : Prop :=
-(has_limit : Π {X Y : C} (f : X ⟶ Y), has_kernel f)
+(has_limit : Π {X Y : C} (f : X ⟶ Y), has_kernel f . tactic.apply_instance)
 
 /-- `has_cokernels` represents the existence of cokernels for every morphism. -/
 class has_cokernels : Prop :=
-(has_colimit : Π {X Y : C} (f : X ⟶ Y), has_cokernel f)
+(has_colimit : Π {X Y : C} (f : X ⟶ Y), has_cokernel f . tactic.apply_instance)
 
 attribute [instance, priority 100] has_kernels.has_limit has_cokernels.has_colimit
 
 @[priority 100]
 instance has_kernels_of_has_equalizers [has_equalizers C] : has_kernels C :=
-{ has_limit := by apply_instance }
+{}
 
 @[priority 100]
 instance has_cokernels_of_has_coequalizers [has_coequalizers C] : has_cokernels C :=
-{ has_colimit := by apply_instance }
+{}
 
 end category_theory.limits