From 0c29987a82945134b596fde5ef8e725fd38dffad Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 8 Mar 2021 18:19:15 -0800
Subject: [PATCH] chore: clenaup test

---
 tests/lean/run/do_eqv.lean | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/tests/lean/run/do_eqv.lean b/tests/lean/run/do_eqv.lean
index 139f75aa66..7773000d75 100644
--- a/tests/lean/run/do_eqv.lean
+++ b/tests/lean/run/do_eqv.lean
@@ -1,9 +1,6 @@
 theorem byCases_Bool_bind [Monad m] (x : m Bool) (f g : Bool → m β) (isTrue : f true = g true) (isFalse : f false = g false) : (x >>= f) = (x >>= g) := by
   have f = g by
-    funext b
-    cases b with
-    | true  => exact isTrue
-    | false => exact isFalse
+    funext b; cases b <;> assumption
   rw [this]
 
 theorem eq_findM [Monad m] [LawfulMonad m] (p : α → m Bool) (xs : List α) :
@@ -16,7 +13,7 @@ theorem eq_findM [Monad m] [LawfulMonad m] (p : α → m Bool) (xs : List α) :
     xs.findM? p := by
   induction xs with simp [List.findM?]
   | cons x xs ih =>
-    rw[← ih]; simp
+    rw [← ih]; simp
     apply byCases_Bool_bind <;> simp
 
 theorem eq_findSomeM_findM [Monad m] [LawfulMonad m] (p : α → m Bool) (xss : List (List α)) :