diff --git a/library/data/sigma/thms.lean b/library/data/sigma/thms.lean
index 0bc91aa30..6309da403 100644
--- a/library/data/sigma/thms.lean
+++ b/library/data/sigma/thms.lean
@@ -12,27 +12,27 @@ namespace sigma
   destruct u (λx y H, H) H
 
   theorem dpair_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) :
-    dpair a₁ b₁ = dpair a₂ b₂ :=
+    ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩ :=
   dcongr_arg2 dpair H₁ H₂
 
   theorem dpair_heq {a : A} {a' : A'} {b : B a} {b' : B' a'}
-      (HB : B == B') (Ha : a == a') (Hb : b == b') : dpair a b == dpair a' b' :=
+      (HB : B == B') (Ha : a == a') (Hb : b == b') : ⟨a, b⟩ == ⟨a', b'⟩ :=
   hcongr_arg4 @dpair (heq.type_eq Ha) HB Ha Hb
 
   protected theorem equal {p₁ p₂ : Σa : A, B a} :
-    ∀(H₁ : dpr1 p₁ = dpr1 p₂) (H₂ : eq.rec_on H₁ (dpr2 p₁) = dpr2 p₂), p₁ = p₂ :=
+    ∀(H₁ : p₁.1 = p₂.1) (H₂ : eq.rec_on H₁ p₁.2 = p₂.2), p₁ = p₂ :=
   destruct p₁ (take a₁ b₁, destruct p₂ (take a₂ b₂ H₁ H₂, dpair_eq H₁ H₂))
 
   protected theorem hequal {p : Σa : A, B a} {p' : Σa' : A', B' a'} (HB : B == B') :
-    ∀(H₁ : dpr1 p == dpr1 p') (H₂ : dpr2 p == dpr2 p'), p == p' :=
+    ∀(H₁ : p.1 == p'.1) (H₂ : p.2 == p'.2), p == p' :=
   destruct p (take a₁ b₁, destruct p' (take a₂ b₂ H₁ H₂, dpair_heq HB H₁ H₂))
 
   protected definition is_inhabited [instance] (H₁ : inhabited A) (H₂ : inhabited (B (default A))) :
     inhabited (sigma B) :=
-  inhabited.destruct H₁ (λa, inhabited.destruct H₂ (λb, inhabited.mk (dpair (default A) b)))
+  inhabited.destruct H₁ (λa, inhabited.destruct H₂ (λb, inhabited.mk ⟨default A, b⟩))
 
   theorem eq_rec_dpair_commute {C : Πa, B a → Type} {a a' : A} (H : a = a') (b : B a) (c : C a b) :
-      eq.rec_on H (dpair b c) = dpair (eq.rec_on H b) (eq.rec_on (dcongr_arg2 C H rfl) c) :=
+      eq.rec_on H ⟨b, c⟩ = ⟨eq.rec_on H b, eq.rec_on (dcongr_arg2 C H rfl) c⟩ :=
   eq.drec_on H (dpair_eq rfl (!eq.rec_on_id⁻¹))
 
   variables {C : Πa, B a → Type} {D : Πa b, C a b → Type}
diff --git a/library/init/sigma.lean b/library/init/sigma.lean
index 2ec84d5a5..113a77334 100644
--- a/library/init/sigma.lean
+++ b/library/init/sigma.lean
@@ -10,17 +10,16 @@ dpair :: (dpr1 : A) (dpr2 : B dpr1)
 notation `Σ` binders `,` r:(scoped P, sigma P) := r
 
 namespace sigma
-
-  notation `dpr₁` := dpr1
-  notation `dpr₂` := dpr2
+  notation `dpr₁`  := dpr1
+  notation `dpr₂`  := dpr2
 
   namespace ops
   postfix `.1`:(max+1) := dpr1
   postfix `.2`:(max+1) := dpr2
-  notation `⟨` t:(foldr `,` (e r, sigma.dpair e r)) `⟩`:0 := t --input ⟨ ⟩ as \< \>
+  notation `⟨`:max t:(foldr `,` (e r, dpair e r)) `⟩`:0 := t --input ⟨ ⟩ as \< \>
   end ops
 
-  open well_founded
+  open ops well_founded
 
   section
   variables {A : Type} {B : A → Type}
@@ -29,8 +28,8 @@ namespace sigma
 
   -- Lexicographical order based on Ra and Rb
   inductive lex : sigma B → sigma B → Prop :=
-  left  : ∀{a₁ b₁} a₂ b₂, Ra a₁ a₂   → lex (dpair a₁ b₁) (dpair a₂ b₂),
-  right : ∀a {b₁ b₂},     Rb a b₁ b₂ → lex (dpair a b₁)  (dpair a b₂)
+  left  : ∀{a₁ b₁} a₂ b₂, Ra a₁ a₂   → lex ⟨a₁, b₁⟩ ⟨a₂, b₂⟩,
+  right : ∀a {b₁ b₂},     Rb a b₁ b₂ → lex ⟨a, b₁⟩  ⟨a, b₂⟩
   end
 
   context
@@ -53,23 +52,23 @@ namespace sigma
       : f a b c == f a' b' c' :=
   hcongr (hcongr_arg2 f Ha Hb) (hcongr_arg2 D Ha Hb) Hc
 
-  definition lex.accessible {a} (aca : acc Ra a) (acb : ∀a, well_founded (Rb a)) : ∀ (b : B a), acc (lex Ra Rb) (dpair a b) :=
+  definition lex.accessible {a} (aca : acc Ra a) (acb : ∀a, well_founded (Rb a)) : ∀ (b : B a), acc (lex Ra Rb) ⟨a, b⟩ :=
   acc.rec_on aca
-    (λxa aca (iHa : ∀y, Ra y xa → ∀b : B y, acc (lex Ra Rb) (dpair y b)),
+    (λxa aca (iHa : ∀y, Ra y xa → ∀b : B y, acc (lex Ra Rb) ⟨y, b⟩),
       λb : B xa, acc.rec_on (acb xa b)
         (λxb acb
-          (iHb : ∀y, Rb xa y xb → acc (lex Ra Rb) (dpair xa y)),
-          acc.intro (dpair xa xb) (λp (lt : p ≺ (dpair xa xb)),
+          (iHb : ∀y, Rb xa y xb → acc (lex Ra Rb) ⟨xa, y⟩),
+          acc.intro ⟨xa, xb⟩ (λp (lt : p ≺ ⟨xa, xb⟩),
             have aux : xa = xa → xb == xb → acc (lex Ra Rb) p, from
-              @lex.rec_on A B Ra Rb (λp₁ p₂, dpr1 p₂ = xa → dpr2 p₂ == xb → acc (lex Ra Rb) p₁)
-                         p (dpair xa xb) lt
+              @lex.rec_on A B Ra Rb (λp₁ p₂, p₂.1 = xa → p₂.2 == xb → acc (lex Ra Rb) p₁)
+                         p ⟨xa, xb⟩ lt
                 (λa₁ b₁ a₂ b₂ (H : Ra a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ == xb),
-                  show acc (lex Ra Rb) (dpair a₁ b₁), from
+                  show acc (lex Ra Rb) ⟨a₁, b₁⟩, from
                   have Ra₁  : Ra a₁ xa, from eq.rec_on eq₂ H,
                   iHa a₁ Ra₁ b₁)
                 (λa b₁ b₂ (H : Rb a b₁ b₂) (eq₂ : a = xa) (eq₃ : b₂ == xb),
                   -- TODO(Leo): cleanup this proof
-                  show acc (lex Ra Rb) (dpair a b₁), from
+                  show acc (lex Ra Rb) ⟨a, b₁⟩, from
                   let b₁' : B xa := eq.rec_on eq₂ b₁ in
                   have aux₁ : b₁ == b₁', from
                     heq.symm (eq_rec_heq eq₂ b₁),
@@ -77,11 +76,11 @@ namespace sigma
                     heq.to_eq (hcongr_arg3 Rb eq₂ aux₁ eq₃),
                   have aux₃ : Rb xa b₁' xb, from
                     eq.rec_on aux₂ H,
-                  have aux₄ : acc (lex Ra Rb) (dpair xa b₁'), from
+                  have aux₄ : acc (lex Ra Rb) ⟨xa, b₁'⟩, from
                     iHb b₁' aux₃,
-                  have aux₅ : ∀ (b₁ b₂ : B a) (H₁ : a = a) (H₂ : b₁ == b₂), acc (lex Ra Rb) (dpair a b₁) → acc (lex Ra Rb) (dpair a b₂), from
+                  have aux₅ : ∀ (b₁ b₂ : B a) (H₁ : a = a) (H₂ : b₁ == b₂), acc (lex Ra Rb) ⟨a, b₁⟩ → acc (lex Ra Rb) ⟨a, b₂⟩, from
                     λ b₁ b₂ H₁ H₂ Ha, eq.rec_on (heq.to_eq H₂) Ha,
-                  have aux₆ : ∀ (b₁ : B xa) (b₂ : B a) (H₁ : a = xa) (H₂ : b₁ == b₂), acc (lex Ra Rb) (dpair xa b₁) → acc (lex Ra Rb) (dpair a b₂), from
+                  have aux₆ : ∀ (b₁ : B xa) (b₂ : B a) (H₁ : a = xa) (H₂ : b₁ == b₂), acc (lex Ra Rb) ⟨xa, b₁⟩ → acc (lex Ra Rb) ⟨a, b₂⟩, from
                     eq.rec_on eq₂ aux₅,
                   aux₆ b₁' b₁ eq₂ (heq.symm aux₁) aux₄),
             aux rfl !heq.refl)))