diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index 295ec4bf1..c0606ee87 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -201,7 +201,7 @@ exists_intro (pr1 (rep a))
   (exists_intro (pr2 (rep a))
     (calc
       a = psub (rep a) : (psub_rep a)⁻¹
-    ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {(prod_ext (rep a))⁻¹}))
+    ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {(prod.eta (rep a))⁻¹}))
 
 -- TODO it should not be opaque.
 protected opaque definition has_decidable_eq [instance] : decidable_eq ℤ :=
@@ -312,7 +312,7 @@ or.imp_or (or.swap (proj_zero_or (rep a)))
     exists_intro (pr1 (rep a))
       (calc
         a = psub (rep a) : (psub_rep a)⁻¹
-          ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {(prod_ext (rep a))⁻¹}
+          ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {(prod.eta (rep a))⁻¹}
           ... = psub (pair (pr1 (rep a)) 0) : {H2}
           ... = of_nat (pr1 (rep a)) : rfl))
   (assume H : pr1 (proj (rep a)) = 0,
@@ -320,7 +320,7 @@ or.imp_or (or.swap (proj_zero_or (rep a)))
     exists_intro (pr2 (rep a))
       (calc
         a = psub (rep a) : (psub_rep a)⁻¹
-          ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {(prod_ext (rep a))⁻¹}
+          ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {(prod.eta (rep a))⁻¹}
           ... = psub (pair 0 (pr2 (rep a))) : {H2}
           ... = -(psub (pair (pr2 (rep a)) 0)) : by simp
           ... = -(of_nat (pr2 (rep a))) : rfl))
diff --git a/library/data/prod.lean b/library/data/prod.lean
index b32a8c247..6accd7425 100644
--- a/library/data/prod.lean
+++ b/library/data/prod.lean
@@ -37,7 +37,7 @@ namespace prod
   theorem pr2.pair : pr₂ (a, b) = b :=
   rfl
 
-  theorem prod_ext (p : prod A B) : pair (pr₁ p) (pr₂ p) = p :=
+  protected theorem eta (p : prod A B) : pair (pr₁ p) (pr₂ p) = p :=
   destruct p (λx y, eq.refl (x, y))
 
   variables {a₁ a₂ : A} {b₁ b₂ : B}
diff --git a/library/data/sigma.lean b/library/data/sigma.lean
index 34d51ca9a..10438836f 100644
--- a/library/data/sigma.lean
+++ b/library/data/sigma.lean
@@ -22,7 +22,7 @@ namespace sigma
   protected theorem destruct {P : sigma B → Prop} (p : sigma B) (H : ∀a b, P (dpair a b)) : P p :=
   rec H p
 
-  theorem dpair_ext (p : sigma B) : dpair (dpr1 p) (dpr2 p) = p :=
+  protected theorem eta (p : sigma B) : dpair (dpr1 p) (dpr2 p) = p :=
   destruct p (take a b, rfl)
 
   theorem dpair_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (H₁ : a₁ = a₂) (H₂ : eq.drec_on H₁ b₁ = b₂) :