From e0b52ebd9827672996c3134e8a7e25bb878d162f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= <vi.hdz.p@gmail.com>
Date: Wed, 30 Oct 2024 11:39:41 -0600
Subject: [PATCH] golf

---
 Mathlib/Data/List/Chain.lean | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/Mathlib/Data/List/Chain.lean b/Mathlib/Data/List/Chain.lean
index d9fa41b6a6518..8b844a1f6243c 100644
--- a/Mathlib/Data/List/Chain.lean
+++ b/Mathlib/Data/List/Chain.lean
@@ -333,12 +333,7 @@ theorem chain'_attachWith {l : List α} {p : α → Prop} (h : ∀ x ∈ l, p x)
     · simp_rw [hb, Option.pbind_some] at hc
       have hb' := h b (mem_cons_of_mem a (mem_of_mem_head? hb))
       exact ⟨h a (mem_cons_self a l), hb', hc ⟨b, hb'⟩ rfl⟩
-    · cases l with
-      | nil => cases hb
-      | cons b l =>
-        obtain ⟨_, _, rfl⟩ := hb
-        obtain ⟨_, _, hr⟩ := hc b rfl
-        exact hr
+    · cases l <;> aesop
 
 theorem chain'_attach {l : List α} {r : {a // a ∈ l} → {a // a ∈ l} → Prop} :
     l.attach.Chain' r ↔ l.Chain' fun a b ↦ ∃ ha hb, r ⟨a, ha⟩ ⟨b, hb⟩ :=