Bump mathlib.

leanpkg.toml

@@ -5,5 +5,4 @@ lean_version = "3.4.1"
 path = "src"
 
 [dependencies]
-mathlib = {git = "https://github.com/leanprover/mathlib", rev = "0ff11df2f6d66151241797d592d19f32c2a747af"}
-lean-category-theory-pr = {git = "https://github.com/semorrison/lean-category-theory-pr", rev = "8eede03beaca5691e1694244e691d379f9f4a2c2"}
+mathlib = {git = "https://github.com/leanprover/mathlib", rev = "cbfe372d1d8e80c558ceb8645929d929bd0f07d7"}

src/category_theory/adjunctions.lean

@@ -1,5 +1,6 @@
 import category_theory.base
 import category_theory.functor_category
+import data.equiv.basic
 
 namespace category_theory
 open category

src/category_theory/assoc_pushouts.lean

@@ -38,8 +38,8 @@ begin
   refine {
     hom := po₁.induced (po₀.induced h₀' (h₁' ∘ g₂) _) (h₁' ∘ g₃) _,
     inv := po₃.induced (h₀ ∘ g₀) (po₂.induced (h₀ ∘ g₁) h₁ _) _,
-    hom_inv_id := _,
-    inv_hom_id := _,
+    hom_inv_id' := _,
+    inv_hom_id' := _,
   },
   { rw po₃.commutes, simp },
   -- TODO: Is_pushout.commutes_assoc

src/category_theory/base.lean

@@ -1,15 +1,13 @@
 --- Project-wide declarations related to category theory.
 
-import category_theory.category
-import tidy.tidy
+import category_theory.functor
+import tactic.tidy
 
 -- Set up `tidy` as the tactic to be invoked by `obviously`.
-@[obviously] meta def tidy_1 := tidy
-
--- `obviously` without trace
-meta def obviously_ := tidy { tactics := default_tidy_tactics ++ obviously_tactics, trace_result := ff, trace_steps := ff }
+@[obviously] meta def tidy_1 := tactic.interactive.tidy
 
 -- TODO: Notation for composition of functors, etc.?
 
 -- TODO: Transitional notation.
 notation F ` &> `:85 f:85 := F.map f
+infixr ` ↝ `:80 := category_theory.functor

src/category_theory/bundled.lean

@@ -30,8 +30,8 @@ instance Cat.category : category Cat :=
 { hom := Cat.functor,
   id := λ C, functor.id C,
   comp := λ _ _ _ F G, F.comp G,
-  id_comp := λ _ _ F, by cases F; refl,
-  comp_id := λ _ _ F, by cases F; refl }
+  id_comp' := λ _ _ F, by cases F; refl,
+  comp_id' := λ _ _ F, by cases F; refl }
 
 end «Cat»
 
@@ -55,8 +55,8 @@ instance Gpd.category : category Gpd :=
 { hom := Gpd.functor,
   id := λ C, functor.id C,
   comp := λ _ _ _ F G, F.comp G,
-  id_comp := λ _ _ F, by cases F; refl,
-  comp_id := λ _ _ F, by cases F; refl }
+  id_comp' := λ _ _ F, by cases F; refl,
+  comp_id' := λ _ _ F, by cases F; refl }
 
 def Gpd.mk_ob (α : Type u) [gpd : groupoid α] : Gpd := ⟨α, gpd⟩
 def Gpd.mk_hom {C D : Gpd} (f : C ↝ D) : C ⟶ D := f

src/category_theory/colimit_lemmas.lean

@@ -109,23 +109,23 @@ def isomorphic_coprod_of_Is_coproduct {a₀ a₁ b : C} {f₀ : a₀ ⟶ b} {f
   (h : Is_coproduct f₀ f₁) : iso (a₀ ⊔ a₁) b :=
 { hom := coprod.induced f₀ f₁,
   inv := h.induced i₀ i₁,
-  hom_inv_id := by apply coprod.uniqueness; { rw ←assoc, simp },
-  inv_hom_id := by apply h.uniqueness; { rw ←assoc, simp } }
+  hom_inv_id' := by apply coprod.uniqueness; { rw ←assoc, simp },
+  inv_hom_id' := by apply h.uniqueness; { rw ←assoc, simp } }
 
 def coprod_of_isomorphisms {a₀ a₁ b₀ b₁ : C} (j₀ : iso a₀ b₀) (j₁ : iso a₁ b₁) :
   iso (a₀ ⊔ a₁) (b₀ ⊔ b₁) :=
 { hom := coprod_of_maps j₀.hom j₁.hom,
   inv := coprod_of_maps j₀.inv j₁.inv,
-  hom_inv_id := by apply coprod.uniqueness; rw ←assoc; simp,
-  inv_hom_id := by apply coprod.uniqueness; rw ←assoc; simp }
+  hom_inv_id' := by apply coprod.uniqueness; rw ←assoc; simp,
+  inv_hom_id' := by apply coprod.uniqueness; rw ←assoc; simp }
 
 variables [has_initial_object.{u v} C]
 
 def coprod_initial_right (a : C) : a ≅ a ⊔ ∅ :=
 { hom := i₀,
   inv := coprod.induced (𝟙 a) (! a),
-  hom_inv_id := by simp,
-  inv_hom_id :=
+  hom_inv_id' := by simp,
+  inv_hom_id' :=
     by apply coprod.uniqueness; try { apply initial.uniqueness };
        rw ←assoc; simp }
 
@@ -136,8 +136,8 @@ rfl
 def coprod_initial_left (a : C) : a ≅ ∅ ⊔ a :=
 { hom := i₁,
   inv := coprod.induced (! a) (𝟙 a),
-  hom_inv_id := by simp,
-  inv_hom_id :=
+  hom_inv_id' := by simp,
+  inv_hom_id' :=
     by apply coprod.uniqueness; try { apply initial.uniqueness };
        rw ←assoc; simp }
 
@@ -216,8 +216,8 @@ parameters {a' : C} (init' : Is_initial_object.{u v} a')
 def initial_object.unique : iso a a' :=
 { hom := init.induced,
   inv := init'.induced,
-  hom_inv_id := init.uniqueness _ _,
-  inv_hom_id := init'.uniqueness _ _ }
+  hom_inv_id' := init.uniqueness _ _,
+  inv_hom_id' := init'.uniqueness _ _ }
 
 end uniqueness_of_initial_objects
 
@@ -235,8 +235,8 @@ parameters {g'₀ : b₀ ⟶ c'} {g'₁ : b₁ ⟶ c'} (po' : Is_pushout f₀ f
 def pushout.unique : iso c c' :=
 { hom := h,
   inv := h',
-  hom_inv_id := by apply po.uniqueness; {rw ←category.assoc, simp},
-  inv_hom_id := by apply po'.uniqueness; {rw ←category.assoc, simp} }
+  hom_inv_id' := by apply po.uniqueness; {rw ←category.assoc, simp},
+  inv_hom_id' := by apply po'.uniqueness; {rw ←category.assoc, simp} }
 
 @[simp] lemma pushout.unique_commutes₀ : ↑pushout.unique ∘ g₀ = g'₀ :=
 by apply po.induced_commutes₀
@@ -472,8 +472,8 @@ def Is_pushout.swap : c ⟶ c := po.induced g₁ g₀ po.commutes.symm
 def Is_pushout.swap_iso : c ≅ c :=
 { hom := po.swap,
   inv := po.swap,
-  hom_inv_id := by apply po.uniqueness; unfold Is_pushout.swap; rw ←assoc; simp,
-  inv_hom_id := by apply po.uniqueness; unfold Is_pushout.swap; rw ←assoc; simp }
+  hom_inv_id' := by apply po.uniqueness; unfold Is_pushout.swap; rw ←assoc; simp,
+  inv_hom_id' := by apply po.uniqueness; unfold Is_pushout.swap; rw ←assoc; simp }
 
 @[simp] def Is_pushout.induced_swap {x} {h₀ h₁ : b ⟶ x} {p p'} :
   po.induced h₀ h₁ p ∘ po.swap = po.induced h₁ h₀ p' :=

src/category_theory/congruence.lean

@@ -31,13 +31,17 @@ omit r
 instance Hom.setoid (a b : C) : setoid (a ⟶ b) :=
 { r := @r a b, iseqv := congruence.is_equiv r }
 
-instance : category (category_mod_congruence C r) :=
+instance category_mod_congruence.category : category (category_mod_congruence C r) :=
 { hom := λ a b, quotient (Hom.setoid C r a b),
   id := λ a, ⟦𝟙 a⟧,
   comp := λ a b c f₀ g₀, quotient.lift_on₂ f₀ g₀ (λ f g, ⟦g ∘ f⟧)
-    (λ f g f' g' rff' rgg', quotient.sound (congruence.congr C rff' rgg' : r _ _)) }
+    (λ f g f' g' rff' rgg', quotient.sound (congruence.congr C rff' rgg' : r _ _)),
+  id_comp' := begin rintros a b ⟨f⟩, change quot.mk _ _ = _, simp end,
+  comp_id' := begin rintros a b ⟨f⟩, change quot.mk _ _ = _, simp end,
+  assoc' := begin rintros a b c d ⟨f⟩ ⟨g⟩ ⟨h⟩, change quot.mk _ _ = quot.mk _ _, simp end
+ }
 
 def quotient_functor : C ↝ category_mod_congruence C r :=
-{ obj := λ a, a, map := λ a b f, ⟦f⟧ }
+{ obj := λ a, a, map' := λ a b f, ⟦f⟧ }
 
 end category_theory

src/category_theory/induced.lean

@@ -27,11 +27,11 @@ def induced_functor [catC : category.{u v} C] [catD : category.{w x} D] (F : C 
   (F' : C' → D') (e : ∀ a, F (k a) = l (F' a)) :
   @functor C' (induced_category k catC) D' (induced_category l catD) :=
 { obj := F',
-  map := λ X Y f,
+  map' := λ X Y f,
     show l (F' X) ⟶ l (F' Y), from
     id_of_eq (e Y) ∘ (F &> f) ∘ id_of_eq (e X).symm,
-  map_id := λ X, by dsimp [induced_category]; rw F.map_id; simp,
-  map_comp := λ X Y Z f g, by dsimp [induced_category]; rw F.map_comp; simp }
+  map_id' := λ X, by dsimp [induced_category]; rw F.map_id; simp,
+  map_comp' := λ X Y Z f g, by dsimp [induced_category]; rw F.map_comp; simp }
 
 def induced_functor_gpd [gpdC : groupoid.{u v} C] [gpdD : groupoid.{w x} D] (F : C ↝ D)
   (F' : C' → D') (e : ∀ a, F (k a) = l (F' a)) :

src/category_theory/iso_lemmas.lean

@@ -15,21 +15,18 @@ namespace iso
 
 -- These lemmas are quite common, to help us avoid having to muck around with associativity.
 -- If anyone has a suggestion for automating them away, I would be very appreciative.
-@[simp,ematch] lemma hom_inv_id_assoc_lemma (I : X ≅ Y) (f : X ⟶ Z) : I.hom ≫ I.inv ≫ f = f := 
+@[simp] lemma hom_inv_id_assoc_lemma (I : X ≅ Y) (f : X ⟶ Z) : (↑I : X ⟶ Y) ≫ (↑I.symm : Y ⟶ X) ≫ f = f :=
 begin
   -- `obviously'` says:
-  rw [←category.assoc_lemma, iso.hom_inv_id_lemma, category.id_comp_lemma]
+  rw [←category.assoc, iso.hom_inv_id, category.id_comp]
 end
 
-@[simp,ematch] lemma inv_hom_id_assoc_lemma (I : X ≅ Y) (f : Y ⟶ Z) : I.inv ≫ I.hom ≫ f = f := 
+@[simp] lemma inv_hom_id_assoc_lemma (I : X ≅ Y) (f : Y ⟶ Z) : (↑I.symm : Y ⟶ X) ≫ (↑I : X ⟶ Y) ≫ f = f :=
 begin
   -- `obviously'` says:
-  rw [←category.assoc_lemma, iso.inv_hom_id_lemma, category.id_comp_lemma]
+  rw [←category.assoc, iso.inv_hom_id, category.id_comp]
 end
 
 end iso
 
-instance of_iso_coe (f : X ≅ Y) : is_iso ↑f :=
-show is_iso f.hom, by apply_instance
-
 end category_theory

src/category_theory/replete.lean

@@ -1,5 +1,5 @@
 import category_theory.base
-import category_theory.isomorphism
+import category_theory.iso_lemmas
 
 open category_theory
 open category_theory.category
@@ -35,11 +35,11 @@ variables {D : Π ⦃a b : C⦄, (a ⟶ b) → Prop} [replete_wide_subcategory.{
 
 lemma mem_of_mem_comp_left {a b c : C} {f : a ⟶ b} (i : iso b c)
   (h : D (i.hom ∘ f)) : D f :=
-by convert mem_comp h (mem_iso i.symm); obviously_
+by convert mem_comp h (mem_iso i.symm); simp
 
 lemma mem_of_mem_comp_right {a b c : C} {f : b ⟶ c} (i : iso a b)
   (h : D (f ∘ i.hom)) : D f :=
-by convert mem_comp (mem_iso i.symm) h; obviously_
+by convert mem_comp (mem_iso i.symm) h; simp
 
 lemma mem_iff_mem_of_isomorphic {a b a' b' : C} {f : a ⟶ b} {f' : a' ⟶ b'}
   (i : iso a a') (j : iso b b')

src/category_theory/transport.lean

@@ -21,9 +21,9 @@ def transported_category : category.{u v'} C :=
 { hom := hom',
   id := λ a, e a a (id a),
   comp := λ a b c f g, e a c (comp ((e a b).symm f) ((e b c).symm g)),
-  id_comp := by intros; simp,
-  comp_id := by intros; simp,
-  assoc := by intros; simp }
+  id_comp' := by intros; simp,
+  comp_id' := by intros; simp,
+  assoc' := by intros; simp }
 
 end category
 
@@ -51,9 +51,9 @@ variables (F : C ↝ D)
 def transported_functor :
   @functor C (transported_category catC eC) D (transported_category catD eD) :=
 { obj := F.obj,
-  map := λ a b f, eD (F a) (F b) (F &> (eC a b).symm f),
-  map_id := by intros; dsimp [transported_category]; simp,
-  map_comp := by intros; dsimp [transported_category]; simp }
+  map' := λ a b f, eD (F a) (F b) (F &> (eC a b).symm f),
+  map_id' := by intros; dsimp [transported_category]; simp; refl,
+  map_comp' := by intros; dsimp [transported_category]; simp; refl }
 
 end functor
 

src/for_mathlib/analysis_topology_topological_space.lean

@@ -83,8 +83,8 @@ open filter
 variables {α : Type u} [topological_space α]
 
 lemma induced_nhds {s : set α} {x : α} (h : x ∈ s) :
-  nhds (⟨x,h⟩ : subtype s) = vmap subtype.val (nhds x) :=
-filter.ext.mpr $ assume r, by rw [mem_vmap_sets, nhds_sets, nhds_sets]; exact
+  nhds (⟨x,h⟩ : subtype s) = comap subtype.val (nhds x) :=
+filter.ext $ assume r, by rw [mem_comap_sets, nhds_sets, nhds_sets]; exact
   iff.intro
     (λ⟨t, tr, ⟨t', t'o, tt'⟩, xt⟩,
       ⟨t', ⟨t', subset.refl t', t'o, by subst tt'; exact xt⟩, tt' ▸ tr⟩)
@@ -99,12 +99,12 @@ begin
   intros f hf fs',
   let f' : filter α := map subtype.val f,
   have : f' ≤ principal s, begin
-    rw [map_le_iff_le_vmap, vmap_principal], convert fs',
+    rw [map_le_iff_le_comap, comap_principal], convert fs',
     apply ext, intro x, simpa using x.property,
   end,
   rcases s_cpt f' (ultrafilter_map hf) this with ⟨a, ha, h2⟩,
   refine ⟨⟨a, ha⟩, trivial, _⟩,
-  rwa [induced_nhds, ←map_le_iff_le_vmap]
+  rwa [induced_nhds, ←map_le_iff_le_comap]
 end
 
 end compact