From 800b4af15d0653fb1f3dd1ca9b4e7e98c95c1e58 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 22 Dec 2020 14:53:03 -0800
Subject: [PATCH] test: indentation

---
 tests/lean/run/newfrontend1.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean
index d695a56db8..ed8a462d3f 100644
--- a/tests/lean/run/newfrontend1.lean
+++ b/tests/lean/run/newfrontend1.lean
@@ -113,7 +113,10 @@ focus
   refine! Eq.trans ?pre ?post
   first
     | exact h1
-    | exact y; exact h3; assumption
+      assumption
+    | exact y
+      exact h3
+      assumption
 
 theorem simple9b (x y z : Nat) : y = z → x = x → x = y → x = z := by
 intros h1 _ h3