feat(tactic/lint): check that left-hand side of all simp lemmas is in…

… simp-normal form (#2017)

* feat(tactic/lint): check that lhs of simp lemmas are in simp nf

* fix(topology/metric_space/basic): remove @[simp] from lemmas with {x,y} on the lhs

* chore(topology/local_homeomorph): remove redundant lemmas from the simp set

* fix(topology/algebra/module): fix simp-nf lints

* chore(ring_theory/localization): mark fewer things as simp

* fix(set_theory/ordinal): put lhs into simp-normal form

* chore(algebra/big_operators): fix simp lemmas

* chore(data/set/lattice): remove redundant simp lemmas

* chore(data/set/basic): remove redundant simp lemma

* chore(data/zsqrtd/basic): make simp_nf lint happy

* fix(order/complete_lattice): remove lemmas from simp set

* chore(order/filter/filter_product): fix linting issues

* feat(data/mv_polynomial): add simp lemmas about neg

* fix(data/multiset): fix simp_nf linter issues

* chore(data/list/sigma): fix simp_nf linter issues

* fix(data/list/basic): remove redundant and unapplicable simp lemmas

* fix(measure_theory/set_integral): remove redundant simp lemma

* fix(measure_theory/l1_space): remove redundant simp lemmas

* fix(algebra/group_power): remove simp lemmas that are not in nf

* fix(algebra/field): remove redundant simp lemma

* chore(data/list/alist): remove simp lemmas

* fix(data/int/basic): simp-normal form for coercions...

* fix(data/finset): formulate simp-lemmas for simp-nf

* fix(data/int/parity): use simp-normal form

* fix(data/equiv/denumerable): remove redundant simp lemma

* fix(category_theory/**): fix simp-normal forms

* fix(set_theory/zfc): put simp lemmas in simp-normal form

* fix(tactlic/lint): ignore sub_eq_add_neg for simp_nf lint

* doc(tactic/lint): add simp_nf linter to module doc

* doc(docs/commands): add simp_nf linter

* fix(*): put lemmas in simp-normal form

docs/commands.md

@@ -116,6 +116,7 @@ The following linters are run by default:
 9.  `incorrect_type_class_argument` checks for arguments in [square brackets] that are not classes.
 10. `dangerous_instance` checks for instances that generate type-class problems with metavariables.
 11. `inhabited_nonempty` checks for `inhabited` instance arguments that should be changed to `nonempty`.
+12. `simp_nf` checks that arguments of the left-hand side of simp lemmas are in simp-normal form.
 
 Another linter, `doc_blame_thm`, checks for missing doc strings on lemmas and theorems.
 This is not run by default.

scripts/mk_all.sh

@@ -40,5 +40,5 @@ cat <<EOT >> lint_mathlib.lean
 open nat -- need to do something before running a command
 
 #lint_mathlib- only unused_arguments dup_namespace doc_blame ge_or_gt def_lemma instance_priority
-  impossible_instance incorrect_type_class_argument dangerous_instance inhabited_nonempty
+  impossible_instance incorrect_type_class_argument dangerous_instance inhabited_nonempty simp_nf
 EOT

src/algebra/big_operators.lean

@@ -626,20 +626,13 @@ lemma sum_mul : s.sum f * b = s.sum (λx, f x * b) :=
 lemma mul_sum : b * s.sum f = s.sum (λx, b * f x) :=
 (s.sum_hom _).symm
 
-@[simp] lemma sum_mul_boole [decidable_eq α] (s : finset α) (f : α → β) (a : α) :
+lemma sum_mul_boole [decidable_eq α] (s : finset α) (f : α → β) (a : α) :
   s.sum (λ x, (f x * ite (a = x) 1 0)) = ite (a ∈ s) (f a) 0 :=
-begin
-  convert sum_ite_eq s a f,
-  funext,
-  split_ifs with h; simp [h],
-end
-@[simp] lemma sum_boole_mul [decidable_eq α] (s : finset α) (f : α → β) (a : α) :
+by simp
+
+lemma sum_boole_mul [decidable_eq α] (s : finset α) (f : α → β) (a : α) :
   s.sum (λ x, (ite (a = x) 1 0) * f x) = ite (a ∈ s) (f a) 0 :=
-begin
-  convert sum_ite_eq s a f,
-  funext,
-  split_ifs with h; simp [h],
-end
+by simp
 
 end semiring
 
@@ -920,7 +913,7 @@ namespace with_top
 open finset
 variables [decidable_eq α]
 
-/-- sum of finte numbers is still finite -/
+/-- sum of finite numbers is still finite -/
 lemma sum_lt_top [ordered_comm_monoid β] {s : finset α} {f : α → with_top β} :
   (∀a∈s, f a < ⊤) → s.sum f < ⊤ :=
 finset.induction_on s (by { intro h, rw sum_empty, exact coe_lt_top _ })
@@ -931,7 +924,7 @@ finset.induction_on s (by { intro h, rw sum_empty, exact coe_lt_top _ })
     { apply ih, intros a ha, apply h, apply mem_insert_of_mem ha }
   end)
 
-/-- sum of finte numbers is still finite -/
+/-- sum of finite numbers is still finite -/
 lemma sum_lt_top_iff [canonically_ordered_monoid β] {s : finset α} {f : α → with_top β} :
   s.sum f < ⊤ ↔ (∀a∈s, f a < ⊤) :=
 iff.intro (λh a ha, lt_of_le_of_lt (single_le_sum (λa ha, zero_le _) ha) h) sum_lt_top

src/algebra/field.lean

@@ -46,8 +46,6 @@ def mk0 (a : α) (ha : a ≠ 0) : units α :=
 
 @[simp] theorem mk0_val (ha : a ≠ 0) : (mk0 a ha : α) = a := rfl
 
-@[simp] theorem mk0_inv (ha : a ≠ 0) : ((mk0 a ha)⁻¹ : α) = a⁻¹ := rfl
-
 @[simp] lemma mk0_coe (u : units α) (h : (u : α) ≠ 0) : mk0 (u : α) h = u :=
 units.ext rfl
 

src/algebra/group_power.lean

@@ -198,8 +198,8 @@ localized "infix ` •ℤ `:70 := gsmul" in smul
 @[simp] theorem gpow_coe_nat (a : G) (n : ℕ) : a ^ (n:ℤ) = a ^ n := rfl
 @[simp] theorem gsmul_coe_nat (a : A) (n : ℕ) : (n:ℤ) • a = n •ℕ a := rfl
 
-@[simp] theorem gpow_of_nat (a : G) (n : ℕ) : a ^ of_nat n = a ^ n := rfl
-@[simp] theorem gsmul_of_nat (a : A) (n : ℕ) : of_nat n • a = n •ℕ a := rfl
+theorem gpow_of_nat (a : G) (n : ℕ) : a ^ of_nat n = a ^ n := rfl
+theorem gsmul_of_nat (a : A) (n : ℕ) : of_nat n • a = n •ℕ a := rfl
 
 @[simp] theorem gpow_neg_succ (a : G) (n : ℕ) : a ^ -[1+n] = (a ^ n.succ)⁻¹ := rfl
 @[simp] theorem gsmul_neg_succ (a : A) (n : ℕ) : -[1+n] • a = - (n.succ •ℕ a) := rfl
@@ -231,11 +231,7 @@ theorem gpow_neg_one (x : G) : x ^ (-1:ℤ) = x⁻¹ := congr_arg has_inv.inv $
 theorem neg_one_gsmul (x : A) : (-1:ℤ) • x = -x := congr_arg has_neg.neg $ add_monoid.one_smul x
 
 theorem gsmul_one [has_one A] (n : ℤ) : n • (1 : A) = n :=
-begin
-cases n,
-  { rw [gsmul_of_nat, add_monoid.smul_one, int.cast_of_nat] },
-  { rw [gsmul_neg_succ, add_monoid.smul_one, int.cast_neg_succ_of_nat, nat.cast_succ] }
-end
+by cases n; simp
 
 theorem inv_gpow (a : G) : ∀n:ℤ, a⁻¹ ^ n = (a ^ n)⁻¹
 | (n : ℕ) := inv_pow a n
@@ -419,7 +415,7 @@ end
 @[field_simps] theorem pow_ne_zero [domain R] {a : R} (n : ℕ) (h : a ≠ 0) : a ^ n ≠ 0 :=
 mt pow_eq_zero h
 
-@[simp] theorem one_div_pow [division_ring R] {a : R} (ha : a ≠ 0) (n : ℕ) : (1 / a) ^ n = 1 / a ^ n :=
+theorem one_div_pow [division_ring R] {a : R} (ha : a ≠ 0) (n : ℕ) : (1 / a) ^ n = 1 / a ^ n :=
 by induction n with n ih; [exact (div_one _).symm,
   rw [pow_succ', ih, division_ring.one_div_mul_one_div (pow_ne_zero _ ha) ha]]; refl
 

src/algebra/ring.lean

@@ -60,6 +60,10 @@ theorem bit0_eq_two_mul (n : α) : bit0 n = 2 * n :=
   a * (if P then 1 else 0) = if P then a else 0 :=
 by split_ifs; simp
 
+@[simp] lemma ite_mul {α} [semiring α] (P : Prop) [decidable P] (a : α) :
+  (if P then 1 else 0) * a = if P then a else 0 :=
+by split_ifs; simp
+
 variable (α)
 
 /-- Either zero and one are nonequal in a semiring, or the semiring is the zero ring. -/

src/algebraic_geometry/prime_spectrum.lean

@@ -171,10 +171,14 @@ lemma subset_zero_locus_vanishing_ideal (t : set (prime_spectrum R)) :
   t ⊆ zero_locus (vanishing_ideal t) :=
 (gc R).l_u_le t
 
-@[simp] lemma zero_locus_bot :
+lemma zero_locus_bot :
   zero_locus ((⊥ : ideal R) : set R) = set.univ :=
 (gc R).l_bot
 
+@[simp] lemma zero_locus_singleton_zero :
+  zero_locus ({0} : set R) = set.univ :=
+zero_locus_bot
+
 @[simp] lemma zero_locus_empty :
   zero_locus (∅ : set R) = set.univ :=
 (gc_set R).l_bot

src/analysis/normed_space/multilinear.lean

@@ -841,10 +841,15 @@ variable {𝕜}
   (f : continuous_multilinear_map 𝕜 (λ (i : fin 0), G) E₂) :
   f.uncurry0 = f 0 := rfl
 
-@[simp] lemma continuous_multilinear_map.uncurry0_curry0
+@[simp] lemma continuous_multilinear_map.apply_zero_curry0
+  (f : continuous_multilinear_map 𝕜 (λ (i : fin 0), G) E₂) {x : fin 0 → G} :
+  continuous_multilinear_map.curry0 𝕜 G (f x) = f :=
+by { ext m, simp [(subsingleton.elim _ _ : x = m)] }
+
+lemma continuous_multilinear_map.uncurry0_curry0
   (f : continuous_multilinear_map 𝕜 (λ (i : fin 0), G) E₂) :
   continuous_multilinear_map.curry0 𝕜 G (f.uncurry0) = f :=
-by { ext m, have : m = 0 := zero_eq_dist.mp rfl, rw this, refl }
+by simp
 
 variables (𝕜 G)
 @[simp] lemma continuous_multilinear_map.curry0_uncurry0 (x : E₂) :
@@ -859,15 +864,21 @@ begin
 end
 
 variables {𝕜 G}
-@[simp] lemma continuous_multilinear_map.curry0_norm
-  (f : continuous_multilinear_map 𝕜 (λ (i : fin 0), G) E₂) : ∥f.uncurry0∥ = ∥f∥ :=
+@[simp] lemma continuous_multilinear_map.fin0_apply_norm
+  (f : continuous_multilinear_map 𝕜 (λ (i : fin 0), G) E₂) {x : fin 0 → G} :
+  ∥f x∥ = ∥f∥ :=
 begin
+  have : x = 0 := subsingleton.elim _ _, subst this,
   refine le_antisymm (by simpa using f.le_op_norm 0) _,
   have : ∥continuous_multilinear_map.curry0 𝕜 G (f.uncurry0)∥ ≤ ∥f.uncurry0∥ :=
     continuous_multilinear_map.op_norm_le_bound _ (norm_nonneg _) (λm, by simp),
-  simpa [-continuous_multilinear_map.uncurry0_apply]
+  simpa
 end
 
+lemma continuous_multilinear_map.curry0_norm
+  (f : continuous_multilinear_map 𝕜 (λ (i : fin 0), G) E₂) : ∥f.uncurry0∥ = ∥f∥ :=
+by simp
+
 variables (𝕜 G E₂)
 /-- The linear isomorphism between elements of a normed space, and continuous multilinear maps in
 `0` variables with values in this normed space. The continuous version is given in

src/category_theory/const.lean

@@ -62,17 +62,11 @@ include 𝒟
 /-- These are actually equal, of course, but not definitionally equal
   (the equality requires F.map (𝟙 _) = 𝟙 _). A natural isomorphism is
   more convenient than an equality between functors (compare id_to_iso). -/
-@[simp] def const_comp (X : C) (F : C ⥤ D) :
+@[simps] def const_comp (X : C) (F : C ⥤ D) :
   (const J).obj X ⋙ F ≅ (const J).obj (F.obj X) :=
 { hom := { app := λ _, 𝟙 _ },
   inv := { app := λ _, 𝟙 _ } }
 
-@[simp] lemma const_comp_hom_app (X : C) (F : C ⥤ D) (j : J) :
-  (const_comp J X F).hom.app j = 𝟙 _ := rfl
-
-@[simp] lemma const_comp_inv_app (X : C) (F : C ⥤ D) (j : J) :
-  (const_comp J X F).inv.app j = 𝟙 _ := rfl
-
 end
 
 end category_theory.functor

src/category_theory/equivalence.lean

@@ -49,12 +49,12 @@ lemma counit_def (e : C ≌ D) : e.counit_iso.hom = e.counit := rfl
 lemma unit_inv_def (e : C ≌ D) : e.unit_iso.inv = e.unit_inv := rfl
 lemma counit_inv_def (e : C ≌ D) : e.counit_iso.inv = e.counit_inv := rfl
 
-@[simp] lemma functor_unit_comp (e : C ≌ D) (X : C) : e.functor.map (e.unit.app X) ≫
-  e.counit.app (e.functor.obj X) = 𝟙 (e.functor.obj X) :=
+@[simp] lemma functor_unit_comp (e : C ≌ D) (X : C) : e.functor.map (e.unit_iso.hom.app X) ≫
+  e.counit_iso.hom.app (e.functor.obj X) = 𝟙 (e.functor.obj X) :=
 e.functor_unit_iso_comp X
 
 @[simp] lemma counit_inv_functor_comp (e : C ≌ D) (X : C) :
-  e.counit_inv.app (e.functor.obj X) ≫ e.functor.map (e.unit_inv.app X) = 𝟙 (e.functor.obj X) :=
+  e.counit_iso.inv.app (e.functor.obj X) ≫ e.functor.map (e.unit_iso.inv.app X) = 𝟙 (e.functor.obj X) :=
 begin
   erw [iso.inv_eq_inv
     (e.functor.map_iso (e.unit_iso.app X) ≪≫ e.counit_iso.app (e.functor.obj X)) (iso.refl _)],
@@ -72,7 +72,7 @@ by { erw [←iso.hom_comp_eq_id (e.functor.map_iso (e.unit_iso.app X)), functor_
 /-- The other triangle equality. The proof follows the following proof in Globular:
   http://globular.science/1905.001 -/
 @[simp] lemma unit_inverse_comp (e : C ≌ D) (Y : D) :
-  e.unit.app (e.inverse.obj Y) ≫ e.inverse.map (e.counit.app Y) = 𝟙 (e.inverse.obj Y) :=
+  e.unit_iso.hom.app (e.inverse.obj Y) ≫ e.inverse.map (e.counit_iso.hom.app Y) = 𝟙 (e.inverse.obj Y) :=
 begin
   rw [←id_comp _ (e.inverse.map _), ←map_id e.inverse, ←counit_inv_functor_comp, map_comp,
       ←iso.hom_inv_id_assoc (e.unit_iso.app _) (e.inverse.map (e.functor.map _)),
@@ -93,7 +93,7 @@ begin
 end
 
 @[simp] lemma inverse_counit_inv_comp (e : C ≌ D) (Y : D) :
-  e.inverse.map (e.counit_inv.app Y) ≫ e.unit_inv.app (e.inverse.obj Y) = 𝟙 (e.inverse.obj Y) :=
+  e.inverse.map (e.counit_iso.inv.app Y) ≫ e.unit_iso.inv.app (e.inverse.obj Y) = 𝟙 (e.inverse.obj Y) :=
 begin
   erw [iso.inv_eq_inv
     (e.unit_iso.app (e.inverse.obj Y) ≪≫ e.inverse.map_iso (e.counit_iso.app Y)) (iso.refl _)],

src/category_theory/functor.lean

@@ -41,7 +41,7 @@ infixr ` ⥤ `:26 := functor       -- type as \func --
 restate_axiom functor.map_id'
 attribute [simp] functor.map_id
 restate_axiom functor.map_comp'
-attribute [simp, reassoc] functor.map_comp
+attribute [reassoc, simp] functor.map_comp
 
 namespace functor
 

src/category_theory/functor_category.lean

@@ -14,6 +14,7 @@ open nat_trans category category_theory.functor
 variables (C : Type u₁) [𝒞 : category.{v₁} C] (D : Type u₂) [𝒟 : category.{v₂} D]
 include 𝒞 𝒟
 
+local attribute [simp] vcomp_app
 /--
 `functor.category C D` gives the category structure on functors and natural transformations
 between categories `C` and `D`.
@@ -35,6 +36,9 @@ namespace nat_trans
 
 @[simp] lemma vcomp_eq_comp (α : F ⟶ G) (β : G ⟶ H) : vcomp α β = α ≫ β := rfl
 
+@[simp] lemma vcomp_app' (α : F ⟶ G) (β : G ⟶ H) (X : C) :
+  (α ≫ β).app X = (α.app X) ≫ (β.app X) := rfl
+
 lemma congr_app {α β : F ⟶ G} (h : α = β) (X : C) : α.app X = β.app X := by rw h
 @[simp] lemma id_app (F : C ⥤ D) (X : C) : (𝟙 F : F ⟶ F).app X = 𝟙 (F.obj X) := rfl
 @[simp] lemma comp_app {F G H : C ⥤ D} (α : F ⟶ G) (β : G ⟶ H) (X : C) :

src/category_theory/isomorphism.lean

@@ -265,13 +265,13 @@ is_iso.of_iso $ F.map_iso (as_iso f)
   F.map (inv f) = inv (F.map f) :=
 rfl
 
-@[simp] lemma map_hom_inv (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) [is_iso f] :
+lemma map_hom_inv (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) [is_iso f] :
   F.map f ≫ F.map (inv f) = 𝟙 (F.obj X) :=
-by rw [map_inv, is_iso.hom_inv_id]
+by simp
 
-@[simp] lemma map_inv_hom (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) [is_iso f] :
+lemma map_inv_hom (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) [is_iso f] :
   F.map (inv f) ≫ F.map f = 𝟙 (F.obj Y) :=
-by rw [map_inv, is_iso.inv_hom_id]
+by simp
 
 end functor
 

src/category_theory/limits/limits.lean

@@ -462,9 +462,9 @@ def limit.cone_morphism {F : J ⥤ C} [has_limit F] (c : cone F) :
 
 @[simp] lemma limit.cone_morphism_hom {F : J ⥤ C} [has_limit F] (c : cone F) :
   (limit.cone_morphism c).hom = limit.lift F c := rfl
-@[simp] lemma limit.cone_morphism_π {F : J ⥤ C} [has_limit F] (c : cone F) (j : J) :
+lemma limit.cone_morphism_π {F : J ⥤ C} [has_limit F] (c : cone F) (j : J) :
   (limit.cone_morphism c).hom ≫ limit.π F j = c.π.app j :=
-by erw is_limit.fac
+by simp
 
 @[ext] lemma limit.hom_ext {F : J ⥤ C} [has_limit F] {X : C} {f f' : X ⟶ limit F}
   (w : ∀ j, f ≫ limit.π F j = f' ≫ limit.π F j) : f = f' :=
@@ -733,9 +733,9 @@ def colimit.cocone_morphism {F : J ⥤ C} [has_colimit F] (c : cocone F) :
 
 @[simp] lemma colimit.cocone_morphism_hom {F : J ⥤ C} [has_colimit F] (c : cocone F) :
   (colimit.cocone_morphism c).hom = colimit.desc F c := rfl
-@[simp] lemma colimit.ι_cocone_morphism {F : J ⥤ C} [has_colimit F] (c : cocone F) (j : J) :
+lemma colimit.ι_cocone_morphism {F : J ⥤ C} [has_colimit F] (c : cocone F) (j : J) :
   colimit.ι F j ≫ (colimit.cocone_morphism c).hom = c.ι.app j :=
-by erw is_colimit.fac
+by simp
 
 @[ext] lemma colimit.hom_ext {F : J ⥤ C} [has_colimit F] {X : C} {f f' : colimit F ⟶ X}
   (w : ∀ j, colimit.ι F j ≫ f = colimit.ι F j ≫ f') : f = f' :=

src/category_theory/limits/shapes/binary_products.lean

@@ -132,10 +132,14 @@ local attribute [tidy] tactic.case_bash
 { hom := prod.lift prod.snd prod.fst,
   inv := prod.lift prod.snd prod.fst }
 
+@[simp] lemma prod.symmetry' (P Q : C) :
+  prod.lift prod.snd prod.fst ≫ prod.lift prod.snd prod.fst = 𝟙 (P ⨯ Q) :=
+by tidy
+
 /-- The braiding isomorphism is symmetric. -/
-@[simp] lemma prod.symmetry (P Q : C) :
+lemma prod.symmetry (P Q : C) :
   (prod.braiding P Q).hom ≫ (prod.braiding Q P).hom = 𝟙 _ :=
-by tidy
+by simp
 
 /-- The associator isomorphism for binary products. -/
 @[simps] def prod.associator
@@ -191,10 +195,14 @@ local attribute [tidy] tactic.case_bash
 { hom := coprod.desc coprod.inr coprod.inl,
   inv := coprod.desc coprod.inr coprod.inl }
 
+@[simp] lemma coprod.symmetry' (P Q : C) :
+  coprod.desc coprod.inr coprod.inl ≫ coprod.desc coprod.inr coprod.inl = 𝟙 (P ⨿ Q) :=
+by tidy
+
 /-- The braiding isomorphism is symmetric. -/
-@[simp] lemma coprod.symmetry (P Q : C) :
+lemma coprod.symmetry (P Q : C) :
   (coprod.braiding P Q).hom ≫ (coprod.braiding Q P).hom = 𝟙 _ :=
-by tidy
+by simp
 
 /-- The associator isomorphism for binary coproducts. -/
 @[simps] def coprod.associator

src/category_theory/limits/shapes/pullbacks.lean

@@ -163,9 +163,9 @@ def span {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) : walking_span.{v} ⥤ C :=
 @[simp] lemma span_map_snd {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) :
   (span f g).map walking_span.hom.snd = g := rfl
 
-@[simp] lemma cospan_map_id {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (w : walking_cospan) :
+lemma cospan_map_id {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (w : walking_cospan) :
   (cospan f g).map (walking_cospan.hom.id w) = 𝟙 _ := rfl
-@[simp] lemma span_map_id {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (w : walking_span) :
+lemma span_map_id {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (w : walking_span) :
   (span f g).map (walking_span.hom.id w) = 𝟙 _ := rfl
 
 

src/category_theory/natural_isomorphism.lean

@@ -63,10 +63,10 @@ begin
 end
 
 variables {X Y : C}
-@[simp] lemma naturality_1 (α : F ≅ G) (f : X ⟶ Y) :
+lemma naturality_1 (α : F ≅ G) (f : X ⟶ Y) :
   (α.inv.app X) ≫ (F.map f) ≫ (α.hom.app Y) = G.map f :=
 begin erw [naturality, ←category.assoc, is_iso.hom_inv_id, category.id_comp] end
-@[simp] lemma naturality_2 (α : F ≅ G) (f : X ⟶ Y) :
+lemma naturality_2 (α : F ≅ G) (f : X ⟶ Y) :
   (α.hom.app X) ≫ (G.map f) ≫ (α.inv.app Y) = F.map f :=
 begin erw [naturality, ←category.assoc, is_iso.hom_inv_id, category.id_comp] end
 

src/category_theory/natural_transformation.lean

@@ -58,7 +58,9 @@ def vcomp (α : nat_trans F G) (β : nat_trans G H) : nat_trans F H :=
     intros, simp, rw [←assoc, naturality, assoc, ←naturality],
   end }
 
-@[simp] lemma vcomp_app (α : nat_trans F G) (β : nat_trans G H) (X : C) :
+-- functor_category will rewrite (vcomp α β) to (α ≫ β), so this is not a
+-- suitable simp lemma.  We will declare the variant vcomp_app' there.
+lemma vcomp_app (α : nat_trans F G) (β : nat_trans G H) (X : C) :
   (vcomp α β).app X = (α.app X) ≫ (β.app X) := rfl
 
 end

src/data/equiv/denumerable.lean

@@ -25,7 +25,7 @@ section
 variables {α : Type*} {β : Type*} [denumerable α] [denumerable β]
 open encodable
 
-@[simp] theorem decode_is_some (α) [denumerable α] (n : ℕ) :
+theorem decode_is_some (α) [denumerable α] (n : ℕ) :
   (decode α n).is_some :=
 option.is_some_iff_exists.2 $
 (decode_inv α n).imp $ λ a, Exists.fst

src/data/fin.lean

@@ -283,6 +283,10 @@ We can think of the type `Π(i : fin n), α i` as `n`-tuples of elements of poss
 operations, first about adding or removing elements at the beginning of a tuple.
 -/
 
+/-- There is exactly one tuple of size zero. -/
+instance tuple0_unique (α : fin 0 → Type u) : unique (Π i : fin 0, α i) :=
+{ default := fin_zero_elim', uniq := λ x, funext fin_zero_elim' }
+
 variables {α : fin (n+1) → Type u} (x : α 0) (q : Πi, α i) (p : Π(i : fin n), α (i.succ))
 (i : fin n) (y : α i.succ) (z : α 0)