cleanup

leanprover-community · Jan 4, 2025 · 6b6ea49 · 6b6ea49
1 parent 42e5c0e
commit 6b6ea49
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 3 deletions.
diff --git 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
@@ -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