chore(algebraic_topology/cech_nerve): An attempt to speed up the proo…

…fs... (#10521)

Let's hope this works!

See [zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.2310312.20timeouts.20in.20cech_nerve/near/262587999)

src/algebraic_topology/cech_nerve.lean

@@ -44,14 +44,38 @@ def cech_nerve : simplicial_object C :=
 { obj := λ n, wide_pullback f.right
     (λ i : ulift (fin (n.unop.len + 1)), f.left) (λ i, f.hom),
   map := λ m n g, wide_pullback.lift (wide_pullback.base _)
-    (λ i, wide_pullback.π (λ i, f.hom) $ ulift.up $ g.unop.to_preorder_hom i.down) (by tidy) }
+    (λ i, wide_pullback.π (λ i, f.hom) $ ulift.up $ g.unop.to_preorder_hom i.down) $ λ j, by simp,
+  map_id' := λ x, by { ext ⟨⟩, { simpa }, { simp } },
+  map_comp' := λ x y z f g, by { ext ⟨⟩, { simpa }, { simp } } }
+
+/-- The morphism between Čech nerves associated to a morphism of arrows. -/
+@[simps]
+def map_cech_nerve {f g : arrow C}
+  [∀ n : ℕ, has_wide_pullback f.right (λ i : ulift (fin (n+1)), f.left) (λ i, f.hom)]
+  [∀ n : ℕ, has_wide_pullback g.right (λ i : ulift (fin (n+1)), g.left) (λ i, g.hom)]
+  (F : f ⟶ g) : f.cech_nerve ⟶ g.cech_nerve :=
+{ app := λ n, wide_pullback.lift (wide_pullback.base _ ≫ F.right)
+    (λ i, wide_pullback.π _ i ≫ F.left) $ λ j, by simp,
+  naturality' := λ x y f, by { ext ⟨⟩, { simp }, { simp } } }
 
 /-- The augmented Čech nerve associated to an arrow. -/
 @[simps]
 def augmented_cech_nerve : simplicial_object.augmented C :=
 { left := f.cech_nerve,
   right := f.right,
-  hom := { app := λ i, wide_pullback.base _ } }
+  hom :=
+  { app := λ i, wide_pullback.base _,
+    naturality' := λ x y f, by { dsimp, simp } } }
+
+/-- The morphism between augmented Čech nerve associated to a morphism of arrows. -/
+@[simps]
+def map_augmented_cech_nerve {f g : arrow C}
+  [∀ n : ℕ, has_wide_pullback f.right (λ i : ulift (fin (n+1)), f.left) (λ i, f.hom)]
+  [∀ n : ℕ, has_wide_pullback g.right (λ i : ulift (fin (n+1)), g.left) (λ i, g.hom)]
+  (F : f ⟶ g) : f.augmented_cech_nerve ⟶ g.augmented_cech_nerve :=
+{ left := map_cech_nerve F,
+  right := F.right,
+  w' := by { ext, simp } }
 
 end category_theory.arrow
 
@@ -65,28 +89,17 @@ variables [∀ (n : ℕ) (f : arrow C),
 @[simps]
 def cech_nerve : arrow C ⥤ simplicial_object C :=
 { obj := λ f, f.cech_nerve,
-  map := λ f g F,
-  { app := λ n, wide_pullback.lift (wide_pullback.base _ ≫ F.right)
-      (λ i, wide_pullback.π _ i ≫ F.left) (λ i, by simp [← category.assoc]) },
-  -- tidy needs a bit of help here...
-  map_id' := by { intros i, ext, tidy },
-  map_comp' := begin
-    intros f g h F G,
-    ext,
-    all_goals
-    { dsimp,
-      simp only [category.assoc, limits.wide_pullback.lift_base,
-        limits.wide_pullback.lift_π, limits.limit.lift_π_assoc],
-      simpa only [← category.assoc] },
-  end }
+  map := λ f g F, arrow.map_cech_nerve F,
+  map_id' := λ i, by { ext, { simp }, { simp } },
+  map_comp' := λ x y z f g, by { ext, { simp }, { simp } } }
 
 /-- The augmented Čech nerve construction, as a functor from `arrow C`. -/
 @[simps]
 def augmented_cech_nerve : arrow C ⥤ simplicial_object.augmented C :=
 { obj := λ f, f.augmented_cech_nerve,
-  map := λ f g F,
-  { left := cech_nerve.map F,
-    right := F.right } }
+  map := λ f g F, arrow.map_augmented_cech_nerve F,
+  map_id' := λ x, by { ext, { simp }, { simp }, { refl } },
+  map_comp' := λ x y z f g, by { ext, { simp }, { simp }, { refl } } }
 
 /-- A helper function used in defining the Čech adjunction. -/
 @[simps]
@@ -97,7 +110,7 @@ def equivalence_right_to_left (X : simplicial_object.augmented C) (F : arrow C)
   w' := begin
     have := G.w,
     apply_fun (λ e, e.app (opposite.op $ simplex_category.mk 0)) at this,
-    tidy,
+    simpa using this,
   end }
 
 /-- A helper function used in defining the Čech adjunction. -/
@@ -106,7 +119,10 @@ def equivalence_left_to_right (X : simplicial_object.augmented C) (F : arrow C)
   (G : augmented.to_arrow.obj X ⟶ F) : X ⟶ F.augmented_cech_nerve :=
 { left :=
   { app := λ x, limits.wide_pullback.lift (X.hom.app _ ≫ G.right)
-      (λ i, X.left.map (simplex_category.const x.unop i.down).op ≫ G.left) (by tidy),
+      (λ i, X.left.map (simplex_category.const x.unop i.down).op ≫ G.left)
+      (λ i, by { dsimp, erw [category.assoc, arrow.w,
+        augmented.to_arrow_obj_hom, nat_trans.naturality_assoc,
+        functor.const.obj_map, category.id_comp] } ),
     naturality' := begin
       intros x y f,
       ext,
@@ -119,7 +135,8 @@ def equivalence_left_to_right (X : simplicial_object.augmented C) (F : arrow C)
           wide_pullback.lift_base, category.assoc],
         erw category.id_comp }
     end },
-  right := G.right }
+  right := G.right,
+  w' := by { ext, dsimp, simp } }
 
 /-- A helper function used in defining the Čech adjunction. -/
 @[simps]
@@ -146,14 +163,12 @@ def cech_nerve_equiv (X : simplicial_object.augmented C) (F : arrow C) :
   end,
   right_inv := begin
     intro A,
-    dsimp,
     ext _ ⟨j⟩,
     { dsimp,
       simp only [arrow.cech_nerve_map, wide_pullback.lift_π, nat_trans.naturality_assoc],
       erw wide_pullback.lift_π,
       refl },
-    { dsimp,
-      erw wide_pullback.lift_base,
+    { erw wide_pullback.lift_base,
       have := A.w,
       apply_fun (λ e, e.app x) at this,
       rw nat_trans.comp_app at this,
@@ -165,7 +180,10 @@ def cech_nerve_equiv (X : simplicial_object.augmented C) (F : arrow C) :
 /-- The augmented Čech nerve construction is right adjoint to the `to_arrow` functor. -/
 abbreviation cech_nerve_adjunction :
   (augmented.to_arrow : _ ⥤ arrow C) ⊣ augmented_cech_nerve :=
-adjunction.mk_of_hom_equiv { hom_equiv := cech_nerve_equiv }
+adjunction.mk_of_hom_equiv
+{ hom_equiv := cech_nerve_equiv,
+  hom_equiv_naturality_left_symm' := λ x y f g h, by { ext, { simp }, { simp } },
+  hom_equiv_naturality_right' := λ x y f g h, by { ext, { simp }, { simp }, { refl } } }
 
 end simplicial_object
 
@@ -182,19 +200,40 @@ def cech_conerve : cosimplicial_object C :=
 { obj := λ n, wide_pushout f.left
     (λ i : ulift (fin (n.len + 1)), f.right) (λ i, f.hom),
   map := λ m n g, wide_pushout.desc (wide_pushout.head _)
-    (λ i, wide_pushout.ι (λ i, f.hom) $ ulift.up $ g.to_preorder_hom i.down)
-    begin
-      rintros ⟨⟨j⟩⟩,
-      dsimp,
-      rw [wide_pushout.arrow_ι (λ i, f.hom)],
-    end }
+    (λ i, wide_pushout.ι (λ i, f.hom) $ ulift.up $ g.to_preorder_hom i.down) $
+    λ i, by { rw [wide_pushout.arrow_ι (λ i, f.hom)] },
+  map_id' := λ x, by { ext ⟨⟩, { simpa }, { simp } },
+  map_comp' := λ x y z f g, by { ext ⟨⟩, { simpa }, { simp } } }
+
+/-- The morphism between Čech conerves associated to a morphism of arrows. -/
+@[simps]
+def map_cech_conerve {f g : arrow C}
+  [∀ n : ℕ, has_wide_pushout f.left (λ i : ulift (fin (n+1)), f.right) (λ i, f.hom)]
+  [∀ n : ℕ, has_wide_pushout g.left (λ i : ulift (fin (n+1)), g.right) (λ i, g.hom)]
+  (F : f ⟶ g) : f.cech_conerve ⟶ g.cech_conerve :=
+{ app := λ n, wide_pushout.desc (F.left ≫ wide_pushout.head _)
+      (λ i, F.right ≫ wide_pushout.ι _ i) $
+      λ i, by { rw [← arrow.w_assoc F, wide_pushout.arrow_ι (λ i, g.hom)] },
+  naturality' := λ x y f, by { ext, { simp }, { simp } } }
 
 /-- The augmented Čech conerve associated to an arrow. -/
 @[simps]
 def augmented_cech_conerve : cosimplicial_object.augmented C :=
 { left := f.left,
   right := f.cech_conerve,
-  hom := { app := λ i, wide_pushout.head _ } }
+  hom :=
+  { app := λ i, wide_pushout.head _,
+    naturality' := λ x y f, by { dsimp, simp } } }
+
+/-- The morphism between augmented Čech conerves associated to a morphism of arrows. -/
+@[simps]
+def map_augmented_cech_conerve {f g : arrow C}
+  [∀ n : ℕ, has_wide_pushout f.left (λ i : ulift (fin (n+1)), f.right) (λ i, f.hom)]
+  [∀ n : ℕ, has_wide_pushout g.left (λ i : ulift (fin (n+1)), g.right) (λ i, g.hom)]
+  (F : f ⟶ g) : f.augmented_cech_conerve ⟶ g.augmented_cech_conerve :=
+{ left := F.left,
+  right := map_cech_conerve F,
+  w' := by { ext, simp } }
 
 end category_theory.arrow
 
@@ -208,29 +247,17 @@ variables [∀ (n : ℕ) (f : arrow C),
 @[simps]
 def cech_conerve : arrow C ⥤ cosimplicial_object C :=
 { obj := λ f, f.cech_conerve,
-  map := λ f g F,
-  { app := λ n, wide_pushout.desc (F.left ≫ wide_pushout.head _)
-      (λ i, F.right ≫ wide_pushout.ι _ i)
-      (λ i, by { rw [←arrow.w_assoc F, wide_pushout.arrow_ι (λ i, g.hom)], }) },
-  -- tidy needs a bit of help here...
-  map_id' := by { intros i, ext, tidy },
-  map_comp' := begin
-    intros f g h F G,
-    ext,
-    all_goals
-    { dsimp,
-      simp only [category.assoc, limits.wide_pushout.head_desc_assoc,
-        limits.wide_pushout.ι_desc_assoc, limits.colimit.ι_desc],
-      simpa only [← category.assoc], },
-  end }
+  map := λ f g F, arrow.map_cech_conerve F,
+  map_id' := λ i, by { ext, { dsimp, simp }, { dsimp, simp } },
+  map_comp' := λ f g h F G, by { ext, { simp }, { simp } } }
 
 /-- The augmented Čech conerve construction, as a functor from `arrow C`. -/
 @[simps]
 def augmented_cech_conerve : arrow C ⥤ cosimplicial_object.augmented C :=
 { obj := λ f, f.augmented_cech_conerve,
-  map := λ f g F,
-  { left := F.left,
-    right := cech_conerve.map F, } }
+  map := λ f g F, arrow.map_augmented_cech_conerve F,
+  map_id' := λ f, by { ext, { refl }, { dsimp, simp }, { dsimp, simp } },
+  map_comp' := λ f g h F G, by { ext, { refl }, { simp }, { simp } } }
 
 /-- A helper function used in defining the Čech conerve adjunction. -/
 @[simps]
@@ -242,7 +269,6 @@ def equivalence_left_to_right (F : arrow C) (X : cosimplicial_object.augmented C
   w' := begin
     have := G.w,
     apply_fun (λ e, e.app (simplex_category.mk 0)) at this,
-    dsimp at this,
     simpa only [category_theory.functor.id_map, augmented.to_arrow_obj_hom,
       wide_pushout.arrow_ι_assoc (λ i, F.hom)],
   end }
@@ -256,11 +282,11 @@ def equivalence_right_to_left (F : arrow C) (X : cosimplicial_object.augmented C
       (λ i, G.right ≫ X.right.map (simplex_category.const x i.down))
       begin
         rintros ⟨j⟩,
-        rw ←arrow.w_assoc G,
-        dsimp,
+        rw ← arrow.w_assoc G,
         have t := X.hom.naturality (x.const j),
-        dsimp at t, simp only [category.id_comp] at t,
-        rw ←t,
+        dsimp at t ⊢,
+        simp only [category.id_comp] at t,
+        rw ← t,
       end,
     naturality' := begin
       intros x y f,
@@ -273,7 +299,8 @@ def equivalence_right_to_left (F : arrow C) (X : cosimplicial_object.augmented C
         simp only [functor.const.obj_map, ←nat_trans.naturality,
           wide_pushout.head_desc_assoc, wide_pushout.head_desc, category.assoc],
         erw category.id_comp }
-    end }, }
+    end },
+  w' := by { ext, simp } }
 
 /-- A helper function used in defining the Čech conerve adjunction. -/
 @[simps]
@@ -284,15 +311,12 @@ def cech_conerve_equiv (F : arrow C) (X : cosimplicial_object.augmented C) :
   left_inv := begin
     intro A,
     dsimp,
-    ext,
-    { refl, },
-    { cases j,
-      dsimp,
+    ext _, { refl }, ext _ ⟨⟩,  -- A bug in the `ext` tactic?
+    { dsimp,
       simp only [arrow.cech_conerve_map, wide_pushout.ι_desc, category.assoc,
-        ←nat_trans.naturality, wide_pushout.ι_desc_assoc],
+        ← nat_trans.naturality, wide_pushout.ι_desc_assoc],
       refl },
-    { dsimp,
-      erw wide_pushout.head_desc,
+    { erw wide_pushout.head_desc,
       have := A.w,
       apply_fun (λ e, e.app x) at this,
       rw nat_trans.comp_app at this,
@@ -301,7 +325,6 @@ def cech_conerve_equiv (F : arrow C) (X : cosimplicial_object.augmented C) :
   end,
   right_inv := begin
     intro A,
-    dsimp,
     ext,
     { refl, },
     { dsimp,
@@ -318,7 +341,10 @@ def cech_conerve_equiv (F : arrow C) (X : cosimplicial_object.augmented C) :
 /-- The augmented Čech conerve construction is left adjoint to the `to_arrow` functor. -/
 abbreviation cech_conerve_adjunction :
   augmented_cech_conerve ⊣ (augmented.to_arrow : _ ⥤ arrow C) :=
-adjunction.mk_of_hom_equiv { hom_equiv := cech_conerve_equiv }
+adjunction.mk_of_hom_equiv
+{ hom_equiv := cech_conerve_equiv,
+  hom_equiv_naturality_left_symm' := λ x y f g h, by { ext, { refl }, { simp }, { simp } },
+  hom_equiv_naturality_right' := λ x y f g h, by { ext, { simp }, { simp } } }
 
 end cosimplicial_object