From 6b6ea495b4512271b49135da425f275cd112f0df Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Sat, 4 Jan 2025 16:17:06 +1100
Subject: [PATCH] cleanup

---
 Aesop/Util/Basic.lean | 3 +--
 AesopTest/List.lean   | 2 +-
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/Aesop/Util/Basic.lean b/Aesop/Util/Basic.lean
index 36b1def..b7107f8 100644
--- a/Aesop/Util/Basic.lean
+++ b/Aesop/Util/Basic.lean
@@ -80,8 +80,7 @@ open DiscrTree
 -- For `type = ∀ (x₁, ..., xₙ), T`, returns keys that match `T * ... *` (with
 -- `n` stars).
 
-def getConclusionDiscrTreeKeys (type : Expr) :
-    MetaM (Array Key) :=
+def getConclusionDiscrTreeKeys (type : Expr) : MetaM (Array Key) :=
   withoutModifyingState do
     let (_, _, conclusion) ← forallMetaTelescope type
     mkDiscrTreePath conclusion
diff --git a/AesopTest/List.lean b/AesopTest/List.lean
index 4c6c793..e394961 100644
--- a/AesopTest/List.lean
+++ b/AesopTest/List.lean
@@ -892,7 +892,7 @@ theorem last_append (l₁ l₂ : List α) (h : l₂ ≠ []) :
   last (l₁ ++ l₂) (append_ne_nil_of_right_ne_nil l₁ h) = last l₂ h := by
   induction l₁ <;> aesop
 
-theorem last_concat {a : α} (l : List α) : last (concat l a) (by exact X.concat_ne_nil a l) = a := by
+theorem last_concat {a : α} (l : List α) : last (concat l a) (X.concat_ne_nil a l) = a := by
   aesop
 
 @[simp] theorem last_singleton (a : α) : last [a] (cons_ne_nil a []) = a := rfl