diff --git a/src/algebraic_geometry/presheafed_space.lean b/src/algebraic_geometry/presheafed_space.lean
index a68d0803a1ca7..949c5569397b9 100644
--- a/src/algebraic_geometry/presheafed_space.lean
+++ b/src/algebraic_geometry/presheafed_space.lean
@@ -9,10 +9,13 @@ open category_theory
 open category_theory.instances
 open category_theory.instances.Top
 open topological_space
+open opposite
 
 variables (C : Type u) [𝒞 : category.{v+1} C]
 include 𝒞
 
+local attribute [tidy] tactic.op_induction'
+
 namespace algebraic_geometry
 
 structure PresheafedSpace :=
@@ -23,13 +26,17 @@ variables {C}
 
 namespace PresheafedSpace
 
-instance : has_coe_to_sort (PresheafedSpace.{v} C) :=
-{ S := Type v, coe := λ F, F.to_Top.α }
+instance coe_to_Top : has_coe (PresheafedSpace.{v} C) Top :=
+{ coe := λ X, X.to_Top }
+
+@[simp] lemma as_coe (X : PresheafedSpace.{v} C) : X.to_Top = (X : Top.{v}) := rfl
+@[simp] lemma mk_coe (to_Top) (𝒪) : (({ to_Top := to_Top, 𝒪 := 𝒪 } :
+  PresheafedSpace.{v} C) : Top.{v}) = to_Top := rfl
 
 instance (X : PresheafedSpace.{v} C) : topological_space X := X.to_Top.str
 
 structure hom (X Y : PresheafedSpace.{v} C) :=
-(f : X.to_Top ⟶ Y.to_Top)
+(f : (X : Top.{v}) ⟶ (Y : Top.{v}))
 (c : Y.𝒪 ⟶ f _* X.𝒪)
 
 @[extensionality] lemma ext {X Y : PresheafedSpace.{v} C} (α β : hom X Y)
@@ -43,7 +50,7 @@ end
 .
 
 def id (X : PresheafedSpace.{v} C) : hom X X :=
-{ f := 𝟙 X.to_Top,
+{ f := 𝟙 (X : Top.{v}),
   c := ((functor.left_unitor _).inv) ≫ (whisker_right (nat_trans.op (opens.map_id _).hom) _) }
 
 def comp (X Y Z : PresheafedSpace.{v} C) (α : hom X Y) (β : hom Y Z) : hom X Z :=
@@ -58,43 +65,7 @@ local attribute [simp] id comp presheaf.pushforward
 instance category_of_PresheafedSpaces : category (PresheafedSpace.{v} C) :=
 { hom  := hom,
   id   := id,
-  comp := comp,
-  -- I'm still grumpy about these proofs.
-  -- The obstacle here is the mysterious need to use `erw` for some `simp` lemmas.
-  -- If we could avoid that, locally adding `op_induction` to `tidy` would discharge these.
-  comp_id' := λ X Y f,
-  begin
-    ext U,
-    { op_induction U,
-      cases U,
-      dsimp,
-      simp, },
-    { dsimp, simp }
-  end,
-  id_comp' := λ X Y f,
-  begin
-    ext U,
-    { op_induction U,
-      cases U,
-      dsimp,
-      simp only [category.assoc],
-      -- This should be done by `simp`, but unfortunately isn't.
-      erw [category_theory.functor.map_id],
-      simp, },
-    { simp }
-  end,
-  assoc' := λ W X Y Z f g h,
-  begin
-    ext U,
-    { op_induction U,
-      cases U,
-      dsimp,
-      simp only [category.assoc],
-      -- This should be done by `simp`, but unfortunately isn't.
-      erw [category_theory.functor.map_id],
-      simp, },
-    { refl }
-  end }
+  comp := comp }
 end
 .
 
@@ -103,25 +74,28 @@ variables {C}
 instance {X Y : PresheafedSpace.{v} C} : has_coe (X ⟶ Y) (X.to_Top ⟶ Y.to_Top) :=
 { coe := λ α, α.f }
 
-@[simp] lemma id_f (X : PresheafedSpace.{v} C) : ((𝟙 X) : X ⟶ X).f = 𝟙 X.to_Top := rfl
-@[simp] lemma comp_f {X Y Z : PresheafedSpace.{v} C} (α : X ⟶ Y) (β : Y ⟶ Z) :
-  (α ≫ β).f = α.f ≫ β.f :=
-rfl
+@[simp] lemma hom_mk_coe {X Y : PresheafedSpace.{v} C} (f) (c) :
+  (({ f := f, c := c } : X ⟶ Y) : (X : Top.{v}) ⟶ (Y : Top.{v})) = f := rfl
+@[simp] lemma f_as_coe {X Y : PresheafedSpace.{v} C} (α : X ⟶ Y) :
+  α.f = (α : (X : Top.{v}) ⟶ (Y : Top.{v})) := rfl
+@[simp] lemma id_coe (X : PresheafedSpace.{v} C) :
+  (((𝟙 X) : X ⟶ X) : (X : Top.{v}) ⟶ X) = 𝟙 (X : Top.{v}) := rfl
 @[simp] lemma comp_coe {X Y Z : PresheafedSpace.{v} C} (α : X ⟶ Y) (β : Y ⟶ Z) :
-  ((α ≫ β : X ⟶ Z) : X.to_Top ⟶ Z.to_Top) = (α : X.to_Top ⟶ Y.to_Top) ≫ (β : Y.to_Top ⟶ Z.to_Top) :=
-rfl
+  ((α ≫ β : X ⟶ Z) : (X : Top.{v}) ⟶ Z) = (α : (X : Top.{v}) ⟶ Y) ≫ (β : Y ⟶ Z) := rfl
 
--- We don't mark these as simp lemmas, because the innards are pretty unsightly.
 lemma id_c (X : PresheafedSpace.{v} C) :
   ((𝟙 X) : X ⟶ X).c =
-  (((functor.left_unitor _).inv) ≫ (whisker_right (nat_trans.op (opens.map_id _).hom) _)) :=
-rfl
+  (((functor.left_unitor _).inv) ≫ (whisker_right (nat_trans.op (opens.map_id _).hom) _)) := rfl
 lemma comp_c {X Y Z : PresheafedSpace.{v} C} (α : X ⟶ Y) (β : Y ⟶ Z) :
-  (α ≫ β).c = (β.c ≫ (whisker_left (opens.map β.f).op α.c)) :=
-rfl
+  (α ≫ β).c = (β.c ≫ (whisker_left (opens.map β.f).op α.c)) := rfl
+@[simp] lemma id_c_app (X : PresheafedSpace.{v} C) (U) :
+  ((𝟙 X) : X ⟶ X).c.app U = eq_to_hom (by tidy) :=
+by { simp only [id_c], tidy }
+@[simp] lemma comp_c_app {X Y Z : PresheafedSpace.{v} C} (α : X ⟶ Y) (β : Y ⟶ Z) (U) :
+  (α ≫ β).c.app U = (β.c).app U ≫ (α.c).app (op ((opens.map (β.f)).obj (unop U))) := rfl
 
 def forget : PresheafedSpace.{v} C ⥤ Top :=
-{ obj := λ X, X.to_Top,
+{ obj := λ X, (X : Top.{v}),
   map := λ X Y f, f }
 
 end PresheafedSpace
@@ -145,11 +119,11 @@ def map_presheaf (F : C ⥤ D) : PresheafedSpace.{v} C ⥤ PresheafedSpace.{v} D
   map := λ X Y f, { f := f.f, c := whisker_right f.c F } }.
 
 @[simp] lemma map_presheaf_obj_X (F : C ⥤ D) (X : PresheafedSpace.{v} C) :
-  (F.map_presheaf.obj X).to_Top = X.to_Top := rfl
+  ((F.map_presheaf.obj X) : Top.{v}) = (X : Top.{v}) := rfl
 @[simp] lemma map_presheaf_obj_𝒪 (F : C ⥤ D) (X : PresheafedSpace.{v} C) :
   (F.map_presheaf.obj X).𝒪 = X.𝒪 ⋙ F := rfl
 @[simp] lemma map_presheaf_map_f (F : C ⥤ D) {X Y : PresheafedSpace.{v} C} (f : X ⟶ Y) :
-  (F.map_presheaf.map f).f = f := rfl
+  ((F.map_presheaf.map f) : (X : Top.{v}) ⟶ (Y : Top.{v})) = f := rfl
 @[simp] lemma map_presheaf_map_c (F : C ⥤ D) {X Y : PresheafedSpace.{v} C} (f : X ⟶ Y) :
   (F.map_presheaf.map f).c = whisker_right f.c F := rfl
 
@@ -161,21 +135,7 @@ def on_presheaf {F G : C ⥤ D} (α : F ⟶ G) : G.map_presheaf ⟶ F.map_preshe
 { app := λ X,
   { f := 𝟙 _,
     c := whisker_left X.𝒪 α ≫ ((functor.left_unitor _).inv) ≫
-           (whisker_right (nat_trans.op (opens.map_id _).hom) _) },
-  naturality' := λ X Y f,
-  begin
-    ext U,
-    { op_induction U,
-      cases U,
-      dsimp,
-      simp only [functor.map_id, category.id_comp, category.comp_id, category.assoc],
-      -- This should be done by `simp`, but unfortunately isn't.
-      erw category_theory.functor.map_id,
-      erw category_theory.functor.map_id,
-      simp only [category.comp_id],
-      exact (α.naturality _).symm, },
-    { refl, }
-  end }.
+           (whisker_right (nat_trans.op (opens.map_id _).hom) _) } }.
 
 end nat_trans
 
diff --git a/src/algebraic_geometry/stalks.lean b/src/algebraic_geometry/stalks.lean
new file mode 100644
index 0000000000000..5817a9b02506c
--- /dev/null
+++ b/src/algebraic_geometry/stalks.lean
@@ -0,0 +1,61 @@
+-- Copyright (c) 2019 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Scott Morrison
+import algebraic_geometry.presheafed_space
+import category_theory.instances.Top.stalks
+
+universes v u v' u'
+
+open category_theory
+open category_theory.instances
+open category_theory.limits
+open algebraic_geometry
+open topological_space
+
+variables {C : Type u} [𝒞 : category.{v+1} C] [has_colimits.{v} C]
+include 𝒞
+
+local attribute [tidy] tactic.op_induction'
+
+open category_theory.instances.Top.presheaf
+
+namespace algebraic_geometry.PresheafedSpace
+
+def stalk (X : PresheafedSpace.{v} C) (x : X) : C := X.𝒪.stalk x
+
+def stalk_map {X Y : PresheafedSpace.{v} C} (α : X ⟶ Y) (x : X) : Y.stalk (α x) ⟶ X.stalk x :=
+(stalk_functor C (α x)).map (α.c) ≫ X.𝒪.stalk_pushforward C α x
+
+namespace stalk_map
+
+@[simp] lemma id (X : PresheafedSpace.{v} C) (x : X) : stalk_map (𝟙 X) x = 𝟙 (X.stalk x) :=
+begin
+  dsimp [stalk_map],
+  simp only [stalk_pushforward.id],
+  rw [←category_theory.functor.map_comp],
+  convert (stalk_functor C x).map_id X.𝒪,
+  tidy,
+end
+.
+
+@[simp] lemma comp {X Y Z : PresheafedSpace.{v} C} (α : X ⟶ Y) (β : Y ⟶ Z) (x : X) :
+  stalk_map (α ≫ β) x =
+    (stalk_map β (α x) : Z.stalk (β (α x)) ⟶ Y.stalk (α x)) ≫
+    (stalk_map α x : Y.stalk (α x) ⟶ X.stalk x) :=
+begin
+  dsimp [stalk, stalk_map, stalk_functor, stalk_pushforward, comp_c],
+  ext U,
+  op_induction U,
+  cases U,
+  cases U_val,
+  simp only [colim.ι_map_assoc, colimit.ι_pre_assoc, colimit.ι_pre,
+    whisker_left.app, whisker_right.app,
+    functor.map_comp, category.assoc, category_theory.functor.map_id, category.id_comp],
+  dsimp,
+  simp only [category_theory.functor.map_id],
+  -- FIXME Why doesn't simp do this:
+  erw [category.id_comp, category.id_comp],
+end
+end stalk_map
+
+end algebraic_geometry.PresheafedSpace
diff --git a/src/category_theory/functor_category.lean b/src/category_theory/functor_category.lean
index 9ada0840f1264..b15a32b6c8b1c 100644
--- a/src/category_theory/functor_category.lean
+++ b/src/category_theory/functor_category.lean
@@ -81,11 +81,13 @@ protected def flip (F : C ⥤ (D ⥤ E)) : D ⥤ (C ⥤ E) :=
     map_id' := λ X, begin rw category_theory.functor.map_id, refl end,
     map_comp' := λ X Y Z f g, by rw [map_comp, ←comp_app] },
   map := λ c c' f,
-  { app := λ j, (F.obj j).map f,
-    naturality' := λ X Y g, by dsimp; rw ←naturality } }.
+  { app := λ j, (F.obj j).map f } }.
 
+@[simp] lemma flip_obj_obj (F : C ⥤ (D ⥤ E)) (c) (d) : (F.flip.obj d).obj c = (F.obj c).obj d := rfl
 @[simp] lemma flip_obj_map (F : C ⥤ (D ⥤ E)) {c c' : C} (f : c ⟶ c') (d : D) :
-  ((F.flip).obj d).map f = (F.map f).app d := rfl
+  (F.flip.obj d).map f = (F.map f).app d := rfl
+@[simp] lemma flip_map_app (F : C ⥤ (D ⥤ E)) {d d' : D} (f : d ⟶ d') (c : C) :
+  (F.flip.map f).app c = (F.obj c).map f := rfl
 
 end functor
 
diff --git a/src/category_theory/instances/Top/basic.lean b/src/category_theory/instances/Top/basic.lean
index 8d692f0b0f775..1fc12364c306b 100644
--- a/src/category_theory/instances/Top/basic.lean
+++ b/src/category_theory/instances/Top/basic.lean
@@ -21,6 +21,8 @@ instance topological_space_unbundled (x : Top) : topological_space x := x.str
 namespace Top
 instance concrete_category_continuous : concrete_category @continuous := ⟨@continuous_id, @continuous.comp⟩
 
+abbreviation forget : Top ⥤ Type u := category_theory.forget
+
 def of (X : Type u) [topological_space X] : Top := ⟨X, by apply_instance⟩
 
 def discrete : Type u ⥤ Top.{u} :=
diff --git a/src/category_theory/instances/Top/open_nhds.lean b/src/category_theory/instances/Top/open_nhds.lean
index ddd92a8a659c6..5dd584af849dc 100644
--- a/src/category_theory/instances/Top/open_nhds.lean
+++ b/src/category_theory/instances/Top/open_nhds.lean
@@ -27,6 +27,8 @@ def map (x : X) : open_nhds (f x) ⥤ open_nhds x :=
 { obj := λ U, ⟨(opens.map f).obj U.1, by tidy⟩,
   map := λ U V i, (opens.map f).map i }
 
+@[simp] lemma map_obj (x : X) (U) (q) : (map f x).obj ⟨U, q⟩ = ⟨(opens.map f).obj U, by tidy⟩ :=
+rfl
 @[simp] lemma map_id_obj' (x : X) (U) (p) (q) : (map (𝟙 X) x).obj ⟨⟨U, p⟩, q⟩ = ⟨⟨U, p⟩, q⟩ :=
 rfl
 @[simp] lemma map_id_obj (x : X) (U) : (map (𝟙 X) x).obj U = U :=
diff --git a/src/category_theory/instances/Top/opens.lean b/src/category_theory/instances/Top/opens.lean
index f5904eeb57836..e9af3c1348d02 100644
--- a/src/category_theory/instances/Top/opens.lean
+++ b/src/category_theory/instances/Top/opens.lean
@@ -36,6 +36,9 @@ def map (f : X ⟶ Y) : opens Y ⥤ opens X :=
 { obj := λ U, ⟨ f.val ⁻¹' U.val, f.property _ U.property ⟩,
   map := λ U V i, ⟨ ⟨ λ a b, i.down.down b ⟩ ⟩ }.
 
+@[simp] lemma map_obj (f : X ⟶ Y) (U) (p) : (map f).obj ⟨U, p⟩ = ⟨ f.val ⁻¹' U, f.property _ p ⟩ :=
+rfl
+
 @[simp] lemma map_id_obj' (U) (p) : (map (𝟙 X)).obj ⟨U, p⟩ = ⟨U, p⟩ :=
 rfl
 
diff --git a/src/category_theory/instances/Top/presheaf.lean b/src/category_theory/instances/Top/presheaf.lean
index 32e559cdb467e..63823087c32b0 100644
--- a/src/category_theory/instances/Top/presheaf.lean
+++ b/src/category_theory/instances/Top/presheaf.lean
@@ -28,7 +28,7 @@ variables {C}
 def pushforward {X Y : Top.{v}} (f : X ⟶ Y) (ℱ : X.presheaf C) : Y.presheaf C :=
 (opens.map f).op ⋙ ℱ
 
-infix `_*`: 80 := pushforward
+infix ` _* `: 80 := pushforward
 
 def pushforward_eq {X Y : Top.{v}} {f g : X ⟶ Y} (h : f = g) (ℱ : X.presheaf C) :
   f _* ℱ ≅ g _* ℱ :=
@@ -47,14 +47,10 @@ def id : (𝟙 X) _* ℱ ≅ ℱ :=
   (id ℱ).hom.app (op ⟨U, p⟩) = ℱ.map (𝟙 (op ⟨U, p⟩)) :=
 by { dsimp [id], simp, }
 
+local attribute [tidy] tactic.op_induction'
+
 @[simp] lemma id_hom_app (U) :
-  (id ℱ).hom.app U = ℱ.map (eq_to_hom (opens.op_map_id_obj U)) :=
-begin
-  op_induction U,
-  cases U,
-  simp,
-  apply category_theory.functor.map_id,
-end
+  (id ℱ).hom.app U = ℱ.map (eq_to_hom (opens.op_map_id_obj U)) := by tidy
 
 @[simp] lemma id_inv_app' (U) (p) : (id ℱ).inv.app (op ⟨U, p⟩) = ℱ.map (𝟙 (op ⟨U, p⟩)) :=
 by { dsimp [id], simp, }
@@ -65,13 +61,13 @@ iso_whisker_right (nat_iso.op (opens.map_comp f g).symm) ℱ
 @[simp] lemma comp_hom_app {Y Z : Top.{v}} (f : X ⟶ Y) (g : Y ⟶ Z) (U) : (comp ℱ f g).hom.app U = 𝟙 _ :=
 begin
   dsimp [pushforward, comp],
-  erw category_theory.functor.map_id, -- FIXME simp should do this
+  tidy,
 end
 
 @[simp] lemma comp_inv_app {Y Z : Top.{v}} (f : X ⟶ Y) (g : Y ⟶ Z) (U) : (comp ℱ f g).inv.app U = 𝟙 _ :=
 begin
   dsimp [pushforward, comp],
-  erw category_theory.functor.map_id,
+  tidy,
 end
 
 end pushforward
diff --git a/src/category_theory/instances/Top/presheaf_of_functions.lean b/src/category_theory/instances/Top/presheaf_of_functions.lean
index 326c058c6ba14..c8567d58672e4 100644
--- a/src/category_theory/instances/Top/presheaf_of_functions.lean
+++ b/src/category_theory/instances/Top/presheaf_of_functions.lean
@@ -1,3 +1,6 @@
+-- Copyright (c) 2019 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Scott Morrison
 import category_theory.instances.Top.presheaf
 import category_theory.instances.TopCommRing.basic
 import category_theory.yoneda
@@ -63,9 +66,6 @@ def presheaf_to_TopCommRing (T : TopCommRing.{v}) :
   X.presheaf CommRing.{v} :=
 (opens.to_Top X).op ⋙ (CommRing_yoneda.obj T)
 
-noncomputable def presheaf_ℚ (Y : Top) : Y.presheaf CommRing :=
-presheaf_to_TopCommRing Y (TopCommRing.of ℚ)
-
 noncomputable def presheaf_ℝ (Y : Top) : Y.presheaf CommRing :=
 presheaf_to_TopCommRing Y (TopCommRing.of ℝ)
 
diff --git a/src/category_theory/instances/Top/stalks.lean b/src/category_theory/instances/Top/stalks.lean
new file mode 100644
index 0000000000000..51481c58e02b1
--- /dev/null
+++ b/src/category_theory/instances/Top/stalks.lean
@@ -0,0 +1,97 @@
+-- Copyright (c) 2019 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Scott Morrison
+
+import category_theory.instances.Top.open_nhds
+import category_theory.instances.Top.presheaf
+import category_theory.limits.limits
+
+universes v u v' u'
+
+open category_theory
+open category_theory.instances
+open category_theory.instances.Top
+open category_theory.limits
+open topological_space
+
+variables {C : Type u} [𝒞 : category.{v+1} C]
+include 𝒞
+
+variables [has_colimits.{v} C]
+
+variables {X Y Z : Top.{v}}
+
+namespace category_theory.instances.Top.presheaf
+
+variables (C)
+/-- Stalks are functorial with respect to morphisms of presheaves over a fixed `X`. -/
+def stalk_functor (x : X) : X.presheaf C ⥤ C :=
+((whiskering_left _ _ C).obj (open_nhds.inclusion x).op) ⋙ colim
+
+variables {C}
+
+/--
+The stalk of a presheaf `F` at a point `x` is calculated as the colimit of the functor
+nbhds x ⥤ opens F.X ⥤ C
+-/
+def stalk (ℱ : X.presheaf C) (x : X) : C :=
+(stalk_functor C x).obj ℱ -- -- colimit (nbhds_inclusion x ⋙ ℱ)
+
+@[simp] lemma stalk_functor_obj (ℱ : X.presheaf C) (x : X) : (stalk_functor C x).obj ℱ = ℱ.stalk x := rfl
+
+variables (C)
+
+def stalk_pushforward (f : X ⟶ Y) (ℱ : X.presheaf C) (x : X) : (f _* ℱ).stalk (f x) ⟶ ℱ.stalk x :=
+begin
+  -- This is a hack; Lean doesn't like to elaborate the term written directly.
+  transitivity,
+  swap,
+  exact colimit.pre _ (open_nhds.map f x).op,
+  exact colim.map (whisker_right (nat_trans.op (open_nhds.inclusion_map_iso f x).inv) ℱ),
+end
+
+-- Here are two other potential solutions, suggested by @fpvandoorn at
+-- https://github.com/leanprover-community/mathlib/pull/1018#discussion_r283978240
+-- However, I can't get the subsequent two proofs to work with either one.
+
+-- def stalk_pushforward (f : X ⟶ Y) (ℱ : X.presheaf C) (x : X) : (f _* ℱ).stalk (f x) ⟶ ℱ.stalk x :=
+-- colim.map ((functor.associator _ _ _).inv ≫
+--   whisker_right (nat_trans.op (open_nhds.inclusion_map_iso f x).inv) ℱ) ≫
+-- colimit.pre ((open_nhds.inclusion x).op ⋙ ℱ) (open_nhds.map f x).op
+
+-- def stalk_pushforward (f : X ⟶ Y) (ℱ : X.presheaf C) (x : X) : (f _* ℱ).stalk (f x) ⟶ ℱ.stalk x :=
+-- (colim.map (whisker_right (nat_trans.op (open_nhds.inclusion_map_iso f x).inv) ℱ) :
+--   colim.obj ((open_nhds.inclusion (f x) ⋙ opens.map f).op ⋙ ℱ) ⟶ _) ≫
+-- colimit.pre ((open_nhds.inclusion x).op ⋙ ℱ) (open_nhds.map f x).op
+
+namespace stalk_pushforward
+local attribute [tidy] tactic.op_induction'
+
+@[simp] lemma id (ℱ : X.presheaf C) (x : X) :
+  ℱ.stalk_pushforward C (𝟙 X) x = (stalk_functor C x).map ((pushforward.id ℱ).hom) :=
+begin
+  dsimp [stalk_pushforward, stalk_functor],
+  tidy,
+end
+
+@[simp] lemma comp (ℱ : X.presheaf C) (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
+  ℱ.stalk_pushforward C (f ≫ g) x =
+  ((f _* ℱ).stalk_pushforward C g (f x)) ≫ (ℱ.stalk_pushforward C f x) :=
+begin
+  dsimp [stalk_pushforward, stalk_functor, pushforward],
+  ext U,
+  op_induction U,
+  cases U,
+  cases U_val,
+  simp only [colim.ι_map_assoc, colimit.ι_pre_assoc, colimit.ι_pre,
+             whisker_right.app, category.assoc],
+  dsimp,
+  simp only [category.id_comp, category_theory.functor.map_id],
+  -- FIXME A simp lemma which unfortunately doesn't fire:
+  rw [category_theory.functor.map_id],
+  dsimp,
+  simp,
+end
+
+end stalk_pushforward
+end category_theory.instances.Top.presheaf
diff --git a/src/category_theory/instances/TopCommRing/basic.lean b/src/category_theory/instances/TopCommRing/basic.lean
index 8c89b62fdf3fe..40e3206dd7647 100644
--- a/src/category_theory/instances/TopCommRing/basic.lean
+++ b/src/category_theory/instances/TopCommRing/basic.lean
@@ -75,8 +75,8 @@ R.is_comm_ring
 instance forget_topological_ring (R : TopCommRing) : topological_ring (forget.obj R) :=
 R.is_topological_ring
 
-def forget_to_Type_via_Top : forget_to_Top ⋙ category_theory.forget ≅ forget := iso.refl _
-def forget_to_Type_via_CommRing : forget_to_Top ⋙ category_theory.forget ≅ forget := iso.refl _
+def forget_to_Type_via_Top : forget_to_Top ⋙ Top.forget ≅ forget := iso.refl _
+def forget_to_Type_via_CommRing : forget_to_CommRing ⋙ CommRing.forget ≅ forget := iso.refl _
 
 end TopCommRing
 
diff --git a/src/category_theory/limits/functor_category.lean b/src/category_theory/limits/functor_category.lean
index 201eb2edd1312..23ba821368bfe 100644
--- a/src/category_theory/limits/functor_category.lean
+++ b/src/category_theory/limits/functor_category.lean
@@ -57,9 +57,7 @@ cocones.ext (iso.refl _) (by tidy)
 def functor_category_is_limit_cone [has_limits_of_shape J C] (F : J ⥤ K ⥤ C) :
   is_limit (functor_category_limit_cone F) :=
 { lift := λ s,
-  { app := λ k, limit.lift (F.flip.obj k) (((evaluation K C).obj k).map_cone s),
-    naturality' := λ k k' f,
-      by ext; dsimp; simpa using (s.π.app j).naturality f },
+  { app := λ k, limit.lift (F.flip.obj k) (((evaluation K C).obj k).map_cone s) },
   uniq' := λ s m w,
   begin
     ext1 k,
@@ -70,14 +68,7 @@ def functor_category_is_limit_cone [has_limits_of_shape J C] (F : J ⥤ K ⥤ C)
 def functor_category_is_colimit_cocone [has_colimits_of_shape.{v} J C] (F : J ⥤ K ⥤ C) :
   is_colimit (functor_category_colimit_cocone F) :=
 { desc := λ s,
-  { app := λ k, colimit.desc (F.flip.obj k) (((evaluation K C).obj k).map_cocone s),
-    naturality' := λ k k' f,
-    begin
-      ext,
-      rw [←assoc, ←assoc],
-      dsimp [functor.flip],
-      simpa using (s.ι.app j).naturality f
-    end },
+  { app := λ k, colimit.desc (F.flip.obj k) (((evaluation K C).obj k).map_cocone s) },
   uniq' := λ s m w,
   begin
     ext1 k,
diff --git a/src/category_theory/natural_isomorphism.lean b/src/category_theory/natural_isomorphism.lean
index 1cba3f4dd6cdc..fdf5cb95e7d92 100644
--- a/src/category_theory/natural_isomorphism.lean
+++ b/src/category_theory/natural_isomorphism.lean
@@ -73,7 +73,11 @@ def is_iso_of_is_iso_app (α : F ⟶ G) [∀ X : C, is_iso (α.app X)] : is_iso
 { inv :=
   { app := λ X, inv (α.app X),
     naturality' := λ X Y f,
-    by simpa using congr_arg (λ f, inv (α.app X) ≫ (f ≫ inv (α.app Y))) (α.naturality f).symm } }
+     begin
+       have h := congr_arg (λ f, inv (α.app X) ≫ (f ≫ inv (α.app Y))) (α.naturality f).symm,
+       simp only [is_iso.inv_hom_id_assoc, is_iso.hom_inv_id, assoc, comp_id, cancel_mono] at h,
+       exact h
+     end } }
 
 instance is_iso_of_is_iso_app' (α : F ⟶ G) [H : ∀ X : C, is_iso (nat_trans.app α X)] : is_iso α :=
 @nat_iso.is_iso_of_is_iso_app _ _ _ _ _ _ α H
diff --git a/src/category_theory/natural_transformation.lean b/src/category_theory/natural_transformation.lean
index c1a6802a8794e..448277bc09e64 100644
--- a/src/category_theory/natural_transformation.lean
+++ b/src/category_theory/natural_transformation.lean
@@ -35,6 +35,8 @@ structure nat_trans (F G : C ⥤ D) : Sort (max u₁ v₂ 1) :=
 (naturality' : ∀ {{X Y : C}} (f : X ⟶ Y), (F.map f) ≫ (app Y) = (app X) ≫ (G.map f) . obviously)
 
 restate_axiom nat_trans.naturality'
+attribute [simp] nat_trans.naturality
+
 namespace nat_trans
 
 /-- `nat_trans.id F` is the identity natural transformation on a functor `F`. -/
diff --git a/src/category_theory/whiskering.lean b/src/category_theory/whiskering.lean
index e97466c9748ad..955421241a0db 100644
--- a/src/category_theory/whiskering.lean
+++ b/src/category_theory/whiskering.lean
@@ -1,9 +1,7 @@
 -- Copyright (c) 2018 Scott Morrison. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Scott Morrison
-
-import category_theory.isomorphism
-import category_theory.functor_category
+import category_theory.natural_isomorphism
 
 namespace category_theory
 
diff --git a/src/data/opposite.lean b/src/data/opposite.lean
index 4f2b9664c28f6..b3e148b9494bc 100644
--- a/src/data/opposite.lean
+++ b/src/data/opposite.lean
@@ -5,6 +5,7 @@ Authors: Scott Morrison, Reid Barton, Simon Hudon, Kenny Lau
 
 Opposites.
 -/
+import data.list.defs
 
 namespace opposite
 universes v u -- declare the `v` first; see `category_theory.category` for an explanation
@@ -55,15 +56,45 @@ def op_induction {F : Π (X : αᵒᵖ), Sort v} (h : Π X, F (op X)) : Π X, F
 λ X, h (unop X)
 end opposite
 
-namespace tactic.interactive
+namespace tactic
 
+open opposite
 open interactive interactive.types lean.parser tactic
+local postfix `?`:9001 := optional
 
-meta def op_induction (h : parse ident) : tactic unit :=
-do h' ← tactic.get_local h,
+namespace op_induction
+
+meta def is_opposite (e : expr) : tactic bool :=
+do t ← infer_type e,
+   `(opposite _) ← whnf t | return ff,
+   return tt
+
+meta def find_opposite_hyp : tactic name :=
+do lc ← local_context,
+   h :: _ ← lc.mfilter $ is_opposite | fail "No hypotheses of the form Xᵒᵖ",
+   return h.local_pp_name
+
+end op_induction
+
+open op_induction
+
+meta def op_induction (h : option name) : tactic unit :=
+do h ← match h with
+   | (some h) := pure h
+   | none     := find_opposite_hyp
+   end,
+   h' ← tactic.get_local h,
    revert_lst [h'],
    applyc `opposite.op_induction,
    tactic.intro h,
    skip
 
-end tactic.interactive
+-- For use with `local attribute [tidy] op_induction`
+meta def op_induction' := op_induction none
+
+namespace interactive
+meta def op_induction (h : parse ident?) : tactic unit :=
+tactic.op_induction h
+end interactive
+
+end tactic