From f89d34e0dc46b3260fbe33e30477ccc5c9896719 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 25 Oct 2020 09:37:26 -0700
Subject: [PATCH] chore: cleanup

---
 src/Init/Core.lean | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/Init/Core.lean b/src/Init/Core.lean
index 09954d9016..7425e59b2c 100644
--- a/src/Init/Core.lean
+++ b/src/Init/Core.lean
@@ -148,18 +148,19 @@ structure Iff (a b : Prop) : Prop :=
 
 @[elabAsEliminator]
 theorem Eq.subst {α : Sort u} {P : α → Prop} {a b : α} (h₁ : a = b) (h₂ : P a) : P b :=
-Eq.ndrec h₂ h₁
+  Eq.ndrec h₂ h₁
 
 theorem Eq.trans {α : Sort u} {a b c : α} (h₁ : a = b) (h₂ : b = c) : a = c :=
-h₂ ▸ h₁
+  h₂ ▸ h₁
 
 theorem Eq.symm {α : Sort u} {a b : α} (h : a = b) : b = a :=
-h ▸ rfl
+  h ▸ rfl
 
 @[macroInline] def cast {α β : Sort u} (h : α = β) (a : α) : β :=
-Eq.rec (motive := fun α _ => α) a h
+  Eq.rec (motive := fun α _ => α) a h
 
-@[matchPattern] def HEq.rfl {α : Sort u} {a : α} : a ≅ a := HEq.refl a
+@[matchPattern] def HEq.rfl {α : Sort u} {a : α} : a ≅ a :=
+  HEq.refl a
 
 theorem eqOfHEq {α : Sort u} {a a' : α} (h : a ≅ a') : a = a' := by
   have (α β : Sort u) → (a : α) → (b : β) → a ≅ b → (h : α = β) → cast h a = b by