From 7c9909983a3b23f5068843ce20aea8585447f4dd Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Wed, 25 Sep 2024 19:06:10 +1000
Subject: [PATCH] fix for leanprover/lean4#5464

---
 Mathlib/Data/Seq/WSeq.lean | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Data/Seq/WSeq.lean b/Mathlib/Data/Seq/WSeq.lean
index 8a167a30145c9..4817d9024ec51 100644
--- a/Mathlib/Data/Seq/WSeq.lean
+++ b/Mathlib/Data/Seq/WSeq.lean
@@ -717,12 +717,9 @@ theorem head_terminates_of_head_tail_terminates (s : WSeq α) [T : Terminates (h
     Terminates (head s) :=
   (head_terminates_iff _).2 <| by
     rcases (head_terminates_iff _).1 T with ⟨⟨a, h⟩⟩
-    simp? [tail] at h says simp only [tail, destruct_flatten] at h
+    simp? [tail] at h says simp only [tail, destruct_flatten, bind_map_left] at h
     rcases exists_of_mem_bind h with ⟨s', h1, _⟩
-    unfold Functor.map at h1
-    exact
-      let ⟨t, h3, _⟩ := Computation.exists_of_mem_map h1
-      Computation.terminates_of_mem h3
+    exact terminates_of_mem h1
 
 theorem destruct_some_of_destruct_tail_some {s : WSeq α} {a} (h : some a ∈ destruct (tail s)) :
     ∃ a', some a' ∈ destruct s := by