chore(category_theory): T50000 challenge (#2840)

A lame effort at making something compile with `-T50000`. No actual speed improvement, just split up a definition into pieces.

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

src/category_theory/limits/over.lean

@@ -94,16 +94,27 @@ namespace construct_products
 def wide_pullback_diagram_of_diagram_over (B : C) {J : Type v} (F : discrete J ⥤ over B) : wide_pullback_shape J ⥤ C :=
 wide_pullback_shape.wide_cospan B (λ j, (F.obj j).left) (λ j, (F.obj j).hom)
 
-local attribute [tidy] tactic.case_bash
+/-- (Impl) A preliminary definition to avoid timeouts. -/
+@[simps]
+def cones_equiv_inverse_obj (B : C) {J : Type v} (F : discrete J ⥤ over B) (c : cone F) :
+  cone (wide_pullback_diagram_of_diagram_over B F) :=
+{ X := c.X.left,
+  π :=
+  { app := λ X, option.cases_on X c.X.hom (λ (j : J), (c.π.app j).left),
+  -- `tidy` can do this using `case_bash`, but let's try to be a good `-T50000` citizen:
+    naturality' := λ X Y f,
+    begin
+      dsimp, cases X; cases Y; cases f,
+      { rw [category.id_comp, category.comp_id], },
+      { rw [over.w, category.id_comp], },
+      { rw [category.id_comp, category.comp_id], },
+    end } }
 
--- FIXME deterministic timeout with `-T50000`
-/-- (Impl) Pull these out to avoid timeouts. -/
+/-- (Impl) A preliminary definition to avoid timeouts. -/
 @[simps]
 def cones_equiv_inverse (B : C) {J : Type v} (F : discrete J ⥤ over B) :
   cone F ⥤ cone (wide_pullback_diagram_of_diagram_over B F) :=
-{ obj := λ c,
-  { X := c.X.left,
-    π := { app := λ X, option.cases_on X c.X.hom (λ (j : J), (c.π.app j).left) } },
+{ obj := cones_equiv_inverse_obj B F,
   map := λ c₁ c₂ f,
   { hom := f.hom.left,
     w' := λ j,
@@ -115,7 +126,7 @@ def cones_equiv_inverse (B : C) {J : Type v} (F : discrete J ⥤ over B) :
         refl }
     end } }
 
-/-- (Impl) Pull these out to avoid timeouts. -/
+/-- (Impl) A preliminary definition to avoid timeouts. -/
 @[simps]
 def cones_equiv_functor (B : C) {J : Type v} (F : discrete J ⥤ over B) :
   cone (wide_pullback_diagram_of_diagram_over B F) ⥤ cone F :=
@@ -125,15 +136,31 @@ def cones_equiv_functor (B : C) {J : Type v} (F : discrete J ⥤ over B) :
   map := λ c₁ c₂ f,
   { hom := over.hom_mk f.hom } }
 
+local attribute [tidy] tactic.case_bash
+
+/-- (Impl) A preliminary definition to avoid timeouts. -/
+@[simp]
+def cones_equiv_unit_iso (B : C) {J : Type v} (F : discrete J ⥤ over B) :
+  𝟭 (cone (wide_pullback_diagram_of_diagram_over B F)) ≅
+    cones_equiv_functor B F ⋙ cones_equiv_inverse B F :=
+nat_iso.of_components (λ _, cones.ext {hom := 𝟙 _, inv := 𝟙 _} (by tidy)) (by tidy)
+
+/-- (Impl) A preliminary definition to avoid timeouts. -/
+@[simp]
+def cones_equiv_counit_iso (B : C) {J : Type v} (F : discrete J ⥤ over B) :
+  cones_equiv_inverse B F ⋙ cones_equiv_functor B F ≅ 𝟭 (cone F) :=
+nat_iso.of_components
+  (λ _, cones.ext {hom := over.hom_mk (𝟙 _), inv := over.hom_mk (𝟙 _)} (by tidy)) (by tidy)
+
 -- TODO: Can we add `. obviously` to the second arguments of `nat_iso.of_components` and `cones.ext`?
 /-- (Impl) Establish an equivalence between the category of cones for `F` and for the "grown" `F`. -/
 @[simps]
 def cones_equiv (B : C) {J : Type v} (F : discrete J ⥤ over B) :
   cone (wide_pullback_diagram_of_diagram_over B F) ≌ cone F :=
 { functor := cones_equiv_functor B F,
   inverse := cones_equiv_inverse B F,
-  unit_iso := nat_iso.of_components (λ _, cones.ext {hom := 𝟙 _, inv := 𝟙 _} (by tidy)) (by tidy),
-  counit_iso := nat_iso.of_components (λ _, cones.ext {hom := over.hom_mk (𝟙 _), inv := over.hom_mk (𝟙 _)} (by tidy)) (by tidy) }
+  unit_iso := cones_equiv_unit_iso B F,
+  counit_iso := cones_equiv_counit_iso B F, }
 
 /-- Use the above equivalence to prove we have a limit. -/
 def has_over_limit_discrete_of_wide_pullback_limit {B : C} {J : Type v} (F : discrete J ⥤ over B)

src/category_theory/limits/shapes/binary_products.lean

@@ -362,8 +362,6 @@ section
 variables {C} [has_binary_products.{v} C]
 variables {D : Type u₂} [category.{v} D] [has_binary_products.{v} D]
 
-local attribute [tidy] tactic.case_bash
-
 -- FIXME deterministic timeout with `-T50000`
 /-- The binary product functor. -/
 @[simps]
@@ -411,7 +409,7 @@ nat_iso.of_components (prod.associator _ _) (by tidy)
 lemma prod.pentagon (W X Y Z : C) :
   prod.map ((prod.associator W X Y).hom) (𝟙 Z) ≫
       (prod.associator W (X ⨯ Y) Z).hom ≫ prod.map (𝟙 W) ((prod.associator X Y Z).hom) =
-    (prod.associator (W ⨯ X) Y Z).hom ≫ (prod.associator W X (Y⨯Z)).hom :=
+    (prod.associator (W ⨯ X) Y Z).hom ≫ (prod.associator W X (Y ⨯ Z)).hom :=
 by tidy
 
 @[reassoc]
@@ -482,8 +480,6 @@ end
 section
 variables {C} [has_binary_coproducts.{v} C]
 
-local attribute [tidy] tactic.case_bash
-
 /-- The braiding isomorphism which swaps a binary coproduct. -/
 @[simps] def coprod.braiding (P Q : C) : P ⨿ Q ≅ Q ⨿ P :=
 { hom := coprod.desc coprod.inr coprod.inl,
@@ -512,8 +508,8 @@ by simp
 
 lemma coprod.pentagon (W X Y Z : C) :
   coprod.map ((coprod.associator W X Y).hom) (𝟙 Z) ≫
-      (coprod.associator W (X⨿Y) Z).hom ≫ coprod.map (𝟙 W) ((coprod.associator X Y Z).hom) =
-    (coprod.associator (W⨿X) Y Z).hom ≫ (coprod.associator W X (Y⨿Z)).hom :=
+      (coprod.associator W (X ⨿ Y) Z).hom ≫ coprod.map (𝟙 W) ((coprod.associator X Y Z).hom) =
+    (coprod.associator (W ⨿ X) Y Z).hom ≫ (coprod.associator W X (Y ⨿ Z)).hom :=
 by tidy
 
 lemma coprod.associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) :