diff --git a/library/algebra/binary.lean b/library/algebra/binary.lean
index be3d8f38c..5979e00b7 100644
--- a/library/algebra/binary.lean
+++ b/library/algebra/binary.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 import logic.core.eq
-open eq_ops
+open eq.ops
 
 namespace binary
   context
diff --git a/library/algebra/category.lean b/library/algebra/category.lean
index 255030653..8c383c9f4 100644
--- a/library/algebra/category.lean
+++ b/library/algebra/category.lean
@@ -8,7 +8,7 @@ import data.unit data.sigma data.prod
 import algebra.function
 import logic.axioms.funext
 
-open eq eq_ops
+open eq eq.ops
 
 inductive category [class] (ob : Type) : Type :=
 mk : Π (mor : ob → ob → Type) (comp : Π⦃A B C : ob⦄, mor B C → mor A B → mor A C)
@@ -476,7 +476,7 @@ namespace category
   end product
 
   section arrow
-  open sigma eq_ops
+  open sigma eq.ops
   -- theorem concat_commutative_squares {ob : Type} {C : category ob} {a1 a2 a3 b1 b2 b3 : ob}
   --     {f1 : a1 => b1} {f2 : a2 => b2} {f3 : a3 => b3} {g2 : a2 => a3} {g1 : a1 => a2}
   --     {h2 : b2 => b3} {h1 : b1 => b2} (H1 : f2 ∘ g1 = h1 ∘ f1) (H2 : f3 ∘ g2 = h2 ∘ f2)
diff --git a/library/data/bool.lean b/library/data/bool.lean
index 47efaea2d..f3176c36a 100644
--- a/library/data/bool.lean
+++ b/library/data/bool.lean
@@ -4,7 +4,7 @@
 import general_notation
 import logic.core.connectives logic.core.decidable logic.core.inhabited
 
-open eq_ops eq decidable
+open eq eq.ops decidable
 
 inductive bool : Type :=
   ff : bool,
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index 52e61d3d3..1ca173c13 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -14,7 +14,7 @@ import tools.fake_simplifier
 open nat
 open quotient subtype prod relation
 open decidable binary fake_simplifier
-open eq_ops
+open eq.ops
 
 namespace int
 -- ## The defining equivalence relation on ℕ × ℕ
diff --git a/library/data/int/order.lean b/library/data/int/order.lean
index 87b904c95..b6a9aa8fe 100644
--- a/library/data/int/order.lean
+++ b/library/data/int/order.lean
@@ -12,7 +12,7 @@ import .basic
 open nat (hiding case)
 open decidable
 open fake_simplifier
-open int eq_ops
+open int eq.ops
 
 namespace int
 
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index 6192a1eba..dda560970 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -15,7 +15,7 @@ import logic tools.helper_tactics
 import logic.core.identities
 
 open nat
-open eq_ops
+open eq.ops
 open helper_tactics
 
 inductive list (T : Type) : Type :=
diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index 0178e7cf6..b7be6ba6f 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -10,7 +10,7 @@
 import logic data.num tools.tactic algebra.binary tools.helper_tactics
 import logic.core.inhabited
 
-open tactic binary eq_ops
+open tactic binary eq.ops
 open decidable
 open relation -- for subst_iff
 open helper_tactics
diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index 78eb3a7b9..ef5970fbb 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -13,7 +13,7 @@ import tools.fake_simplifier
 
 open nat relation relation.iff_ops prod
 open fake_simplifier decidable
-open eq_ops
+open eq.ops
 
 namespace nat
 
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index 79bc63786..355fd3fbf 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -10,7 +10,7 @@
 import .basic logic.core.decidable
 import tools.fake_simplifier
 
-open nat eq_ops tactic
+open nat eq.ops tactic
 open fake_simplifier
 
 namespace nat
diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean
index b062d4e2b..c4504e3b0 100644
--- a/library/data/nat/sub.lean
+++ b/library/data/nat/sub.lean
@@ -10,7 +10,7 @@
 import data.nat.order
 import tools.fake_simplifier
 
-open nat eq_ops tactic
+open nat eq.ops tactic
 open helper_tactics
 open fake_simplifier
 
diff --git a/library/data/option.lean b/library/data/option.lean
index 387a49913..87314d7a7 100644
--- a/library/data/option.lean
+++ b/library/data/option.lean
@@ -3,7 +3,7 @@
 -- Author: Leonardo de Moura
 
 import logic.core.eq logic.core.inhabited logic.core.decidable
-open eq_ops decidable
+open eq.ops decidable
 
 inductive option (A : Type) : Type :=
   none {} : option A,
diff --git a/library/data/prod.lean b/library/data/prod.lean
index e12b3e4ae..e2d09e44b 100644
--- a/library/data/prod.lean
+++ b/library/data/prod.lean
@@ -37,7 +37,7 @@ section
   theorem prod_ext (p : prod A B) : pair (pr1 p) (pr2 p) = p :=
   destruct p (λx y, eq.refl (x, y))
 
-  open eq_ops
+  open eq.ops
 
   theorem pair_eq {a1 a2 : A} {b1 b2 : B} (H1 : a1 = a2) (H2 : b1 = b2) : (a1, b1) = (a2, b2) :=
   H1 ▸ H2 ▸ rfl
diff --git a/library/data/quotient/basic.lean b/library/data/quotient/basic.lean
index 97714578f..f29e56b7f 100644
--- a/library/data/quotient/basic.lean
+++ b/library/data/quotient/basic.lean
@@ -9,7 +9,7 @@ import logic tools.tactic ..subtype logic.core.cast algebra.relation data.prod
 import logic.core.instances
 import .util
 
-open relation prod inhabited nonempty tactic eq_ops
+open relation prod inhabited nonempty tactic eq.ops
 open subtype relation.iff_ops
 
 namespace quotient
@@ -225,7 +225,7 @@ theorem image_tag {A B : Type} {f : A → B} (u : image f) : ∃a H, tag (f a) H
 obtain a (H : fun_image f a = u), from fun_image_surj u,
 exists_intro a (exists_intro (exists_intro a rfl) H)
 
-open eq_ops
+open eq.ops
 
 theorem fun_image_eq {A B : Type} (f : A → B) (a a' : A)
   : (f a = f a') ↔ (fun_image f a = fun_image f a') :=
diff --git a/library/data/quotient/util.lean b/library/data/quotient/util.lean
index f3823a52f..ca109f903 100644
--- a/library/data/quotient/util.lean
+++ b/library/data/quotient/util.lean
@@ -5,7 +5,7 @@
 import logic ..prod algebra.relation
 import tools.fake_simplifier
 
-open prod eq_ops
+open prod eq.ops
 open fake_simplifier
 
 namespace quotient
diff --git a/library/data/set.lean b/library/data/set.lean
index a88363832..5d7aee4e2 100644
--- a/library/data/set.lean
+++ b/library/data/set.lean
@@ -4,7 +4,7 @@
 --- Author: Jeremy Avigad, Leonardo de Moura
 ----------------------------------------------------------------------------------------------------
 import data.bool
-open eq_ops bool
+open eq.ops bool
 
 namespace set
 definition set (T : Type) :=
diff --git a/library/data/sigma.lean b/library/data/sigma.lean
index 6a746d1e7..e346b7523 100644
--- a/library/data/sigma.lean
+++ b/library/data/sigma.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
 import logic.core.inhabited logic.core.eq
-open inhabited eq_ops
+open inhabited eq.ops
 
 inductive sigma {A : Type} (B : A → Type) : Type :=
 dpair : Πx : A, B x → sigma B
diff --git a/library/data/sum.lean b/library/data/sum.lean
index f517f66a8..8fba4a15e 100644
--- a/library/data/sum.lean
+++ b/library/data/sum.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad
 import logic.core.prop logic.core.inhabited logic.core.decidable
-open inhabited decidable eq_ops
+open inhabited decidable eq.ops
 -- data.sum
 -- ========
 -- The sum type, aka disjoint union.
diff --git a/library/data/vector.lean b/library/data/vector.lean
index c6f17b6dd..b9d2ffedc 100644
--- a/library/data/vector.lean
+++ b/library/data/vector.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Floris van Doorn
 import data.nat.basic data.empty
-open nat eq_ops
+open nat eq.ops
 
 inductive vector (T : Type) : ℕ → Type :=
   nil {} : vector T 0,
diff --git a/library/logic/axioms/classical.lean b/library/logic/axioms/classical.lean
index de437e6cd..f2a560e4a 100644
--- a/library/logic/axioms/classical.lean
+++ b/library/logic/axioms/classical.lean
@@ -7,7 +7,7 @@
 
 import logic.core.quantifiers logic.core.cast algebra.relation
 
-open eq_ops
+open eq.ops
 
 axiom prop_complete (a : Prop) : a = true ∨ a = false
 
diff --git a/library/logic/axioms/examples/diaconescu.lean b/library/logic/axioms/examples/diaconescu.lean
index 0ff9e0314..5c15c5162 100644
--- a/library/logic/axioms/examples/diaconescu.lean
+++ b/library/logic/axioms/examples/diaconescu.lean
@@ -3,7 +3,7 @@
 -- Author: Leonardo de Moura
 
 import logic.axioms.hilbert logic.axioms.funext
-open eq_ops nonempty inhabited
+open eq.ops nonempty inhabited
 
 -- Diaconescu’s theorem
 -- Show that Excluded middle follows from
diff --git a/library/logic/core/cast.lean b/library/logic/core/cast.lean
index 78bacc1f1..7c4be7b47 100644
--- a/library/logic/core/cast.lean
+++ b/library/logic/core/cast.lean
@@ -7,7 +7,7 @@
 
 import .eq .quantifiers
 
-open eq_ops
+open eq.ops
 
 definition cast {A B : Type} (H : A = B) (a : A) : B :=
 eq.rec a H
diff --git a/library/logic/core/connectives.lean b/library/logic/core/connectives.lean
index 9a3f06641..164321851 100644
--- a/library/logic/core/connectives.lean
+++ b/library/logic/core/connectives.lean
@@ -155,7 +155,7 @@ end iff
 calc_refl iff.refl
 calc_trans iff.trans
 
-open eq_ops
+open eq.ops
 
 theorem eq_to_iff {a b : Prop} (H : a = b) : a ↔ b :=
 iff.intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb)
diff --git a/library/logic/core/eq.lean b/library/logic/core/eq.lean
index 34a8cdd49..89c105425 100644
--- a/library/logic/core/eq.lean
+++ b/library/logic/core/eq.lean
@@ -36,18 +36,19 @@ namespace eq
 
   theorem symm {A : Type} {a b : A} (H : a = b) : b = a :=
   subst H (refl a)
+
+  namespace ops
+    postfix `⁻¹` := symm
+    infixr `⬝`   := trans
+    infixr `▸`   := subst
+  end ops
 end eq
 
 calc_subst eq.subst
 calc_refl  eq.refl
 calc_trans eq.trans
 
-namespace eq_ops
-  postfix `⁻¹` := eq.symm
-  infixr `⬝`   := eq.trans
-  infixr `▸`   := eq.subst
-end eq_ops
-open eq_ops
+open eq.ops
 
 namespace eq
   -- eq_rec with arguments swapped, for transporting an element of a dependent type
diff --git a/library/logic/core/examples/instances_test.lean b/library/logic/core/examples/instances_test.lean
index 6be183692..54fdc674d 100644
--- a/library/logic/core/examples/instances_test.lean
+++ b/library/logic/core/examples/instances_test.lean
@@ -7,7 +7,7 @@ import ..instances
 open relation
 open relation.general_operations
 open relation.iff_ops
-open eq_ops
+open eq.ops
 
 section
 
diff --git a/library/logic/core/if.lean b/library/logic/core/if.lean
index f29c37e39..aba58ebab 100644
--- a/library/logic/core/if.lean
+++ b/library/logic/core/if.lean
@@ -5,7 +5,7 @@
 ----------------------------------------------------------------------------------------------------
 
 import logic.core.decidable tools.tactic
-open decidable tactic eq_ops
+open decidable tactic eq.ops
 
 definition ite (c : Prop) {H : decidable c} {A : Type} (t e : A) : A :=
 decidable.rec_on H (assume Hc,  t) (assume Hnc, e)
diff --git a/tests/lean/have1.lean b/tests/lean/have1.lean
index 8a7f4c6b6..2fe4534b1 100644
--- a/tests/lean/have1.lean
+++ b/tests/lean/have1.lean
@@ -1,5 +1,5 @@
 import logic
-open bool eq_ops tactic eq
+open bool eq.ops tactic eq
 
 variables a b c : bool
 axiom H1 : a = b
diff --git a/tests/lean/run/div2.lean b/tests/lean/run/div2.lean
index 6c26d1943..90f2ac8fd 100644
--- a/tests/lean/run/div2.lean
+++ b/tests/lean/run/div2.lean
@@ -3,7 +3,7 @@ import tools.fake_simplifier
 
 open nat relation relation.iff_ops prod
 open fake_simplifier decidable
-open eq_ops
+open eq.ops
 
 namespace nat
 
diff --git a/tests/lean/run/list_elab1.lean b/tests/lean/run/list_elab1.lean
index 8a28ee97b..e0fa61f81 100644
--- a/tests/lean/run/list_elab1.lean
+++ b/tests/lean/run/list_elab1.lean
@@ -10,7 +10,7 @@
 -- Basic properties of lists.
 
 import data.nat
-open nat eq_ops
+open nat eq.ops
 inductive list (T : Type) : Type :=
 nil {} : list T,
 cons : T → list T → list T
diff --git a/tests/lean/run/nat_bug2.lean b/tests/lean/run/nat_bug2.lean
index 903f3252e..4aa31159d 100644
--- a/tests/lean/run/nat_bug2.lean
+++ b/tests/lean/run/nat_bug2.lean
@@ -1,5 +1,5 @@
 import logic
-open eq_ops
+open eq.ops
 
 inductive nat : Type :=
 zero : nat,
diff --git a/tests/lean/run/nat_bug3.lean b/tests/lean/run/nat_bug3.lean
index 31d17b016..5c7908885 100644
--- a/tests/lean/run/nat_bug3.lean
+++ b/tests/lean/run/nat_bug3.lean
@@ -1,5 +1,5 @@
 import logic
-open eq_ops
+open eq.ops
 
 inductive nat : Type :=
 zero : nat,
diff --git a/tests/lean/run/nat_bug4.lean b/tests/lean/run/nat_bug4.lean
index fd7de826c..03f7764d5 100644
--- a/tests/lean/run/nat_bug4.lean
+++ b/tests/lean/run/nat_bug4.lean
@@ -1,5 +1,5 @@
 import logic
-open eq_ops
+open eq.ops
 
 inductive nat : Type :=
 zero : nat,
diff --git a/tests/lean/run/nat_bug5.lean b/tests/lean/run/nat_bug5.lean
index 1b9e0aa14..b4859dd99 100644
--- a/tests/lean/run/nat_bug5.lean
+++ b/tests/lean/run/nat_bug5.lean
@@ -1,5 +1,5 @@
 import logic
-open eq_ops eq
+open eq.ops eq
 
 inductive nat : Type :=
 zero : nat,
diff --git a/tests/lean/run/nat_bug6.lean b/tests/lean/run/nat_bug6.lean
index 5e8bb28db..90ca8ac35 100644
--- a/tests/lean/run/nat_bug6.lean
+++ b/tests/lean/run/nat_bug6.lean
@@ -1,5 +1,5 @@
 import logic
-open eq_ops
+open eq.ops
 
 inductive nat : Type :=
 zero : nat,
diff --git a/tests/lean/show1.lean b/tests/lean/show1.lean
index 27479a3ed..6e56b9474 100644
--- a/tests/lean/show1.lean
+++ b/tests/lean/show1.lean
@@ -1,5 +1,5 @@
 import logic
-open bool eq_ops tactic
+open bool eq.ops tactic
 
 variables a b c : bool
 axiom H1 : a = b
diff --git a/tests/lean/slow/list_elab2.lean b/tests/lean/slow/list_elab2.lean
index 8752dce80..ceccc793b 100644
--- a/tests/lean/slow/list_elab2.lean
+++ b/tests/lean/slow/list_elab2.lean
@@ -14,7 +14,7 @@ import logic data.nat
 
 open nat
 -- open congr
-open eq_ops eq
+open eq.ops eq
 
 inductive list (T : Type) : Type :=
 nil {} : list T,
diff --git a/tests/lean/slow/nat_bug2.lean b/tests/lean/slow/nat_bug2.lean
index 561e36fbf..1a108911d 100644
--- a/tests/lean/slow/nat_bug2.lean
+++ b/tests/lean/slow/nat_bug2.lean
@@ -4,7 +4,7 @@
 -- Author: Floris van Doorn
 ----------------------------------------------------------------------------------------------------
 import logic algebra.binary
-open tactic binary eq_ops eq
+open tactic binary eq.ops eq
 open decidable
 
 definition refl := @eq.refl
diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean
index a63207e3e..f1b9cb5e6 100644
--- a/tests/lean/slow/nat_wo_hints.lean
+++ b/tests/lean/slow/nat_wo_hints.lean
@@ -4,7 +4,7 @@
 -- Author: Floris van Doorn
 ----------------------------------------------------------------------------------------------------
 import logic algebra.binary
-open tactic binary eq_ops eq
+open tactic binary eq.ops eq
 open decidable
 
 inductive nat : Type :=