diff --git a/library/init/core.lean b/library/init/core.lean
index c04946bdde..77a9a78345 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -1278,9 +1278,9 @@ instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) :=
 {decEq := λ ⟨a, b⟩ ⟨a', b'⟩,
   match (decEq a a') with
   | (isTrue e₁) :=
-    match (decEq b b') with
-    | (isTrue e₂)  := isTrue (Eq.recOn e₁ (Eq.recOn e₂ rfl))
-    | (isFalse n₂) := isFalse (assume h, Prod.noConfusion h (λ e₁' e₂', absurd e₂' n₂))
+    (match (decEq b b') with
+     | (isTrue e₂)  := isTrue (Eq.recOn e₁ (Eq.recOn e₂ rfl))
+     | (isFalse n₂) := isFalse (assume h, Prod.noConfusion h (λ e₁' e₂', absurd e₂' n₂)))
   | (isFalse n₁) := isFalse (assume h, Prod.noConfusion h (λ e₁' e₂', absurd e₁' n₁))}
 
 instance [HasLess α] [HasLess β] : HasLess (α × β) :=