From 4a941eb9471798ba849f203f03a7c5dab21da509 Mon Sep 17 00:00:00 2001
From: Vasily Nesterov <vas.nesterov63@gmail.com>
Date: Mon, 9 Dec 2024 11:52:32 +0300
Subject: [PATCH 01/24] make Seq.recOn cases_eliminator

---
 Mathlib/Data/Seq/Parallel.lean |   4 +-
 Mathlib/Data/Seq/Seq.lean      | 130 +++++++++++++++------------------
 2 files changed, 60 insertions(+), 74 deletions(-)

diff --git a/Mathlib/Data/Seq/Parallel.lean b/Mathlib/Data/Seq/Parallel.lean
index ee4bdac0f33db6..16ea3f436d55d5 100644
--- a/Mathlib/Data/Seq/Parallel.lean
+++ b/Mathlib/Data/Seq/Parallel.lean
@@ -157,9 +157,7 @@ theorem terminates_parallel {S : WSeq (Computation α)} {c} (h : c ∈ S) [T : T
       have TT : ∀ l', Terminates (corec parallel.aux1 (l', S.tail)) := by
         intro
         apply IH _ _ _ (Or.inr _) T
-        rw [a]
-        cases' S with f al
-        rfl
+        rw [a, Seq.get?_tail]
       induction' e : Seq.get? S 0 with o
       · have D : Seq.destruct S = none := by
           dsimp [Seq.destruct]
diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
index 8b25a1d0c7c0a5..d45af9a0910ef3 100644
--- a/Mathlib/Data/Seq/Seq.lean
+++ b/Mathlib/Data/Seq/Seq.lean
@@ -150,8 +150,10 @@ theorem ge_stable (s : Seq α) {aₙ : α} {n m : ℕ} (m_le_n : m ≤ n)
   have : s.get? m ≠ none := mt (s.le_stable m_le_n) this
   Option.ne_none_iff_exists'.mp this
 
+@[simp]
 theorem not_mem_nil (a : α) : a ∉ @nil α := fun ⟨_, (h : some a = none)⟩ => by injection h
 
+@[simp]
 theorem mem_cons (a : α) : ∀ s : Seq α, a ∈ cons a s
   | ⟨_, _⟩ => Stream'.mem_cons (some a) _
 
@@ -230,14 +232,16 @@ theorem get?_tail (s : Seq α) (n) : get? (tail s) n = get? s (n + 1) :=
   rfl
 
 /-- Recursion principle for sequences, compare with `List.recOn`. -/
-def recOn {C : Seq α → Sort v} (s : Seq α) (h1 : C nil) (h2 : ∀ x s, C (cons x s)) :
-    C s := by
+@[cases_eliminator]
+def recOn {motive : Seq α → Sort v} (s : Seq α) (nil : motive nil)
+    (cons : ∀ x s, motive (cons x s)) :
+    motive s := by
   cases' H : destruct s with v
   · rw [destruct_eq_nil H]
-    apply h1
+    apply nil
   · cases' v with a s'
     rw [destruct_eq_cons H]
-    apply h2
+    apply cons
 
 theorem mem_rec_on {C : Seq α → Prop} {a s} (M : a ∈ s)
     (h1 : ∀ b s', a = b ∨ C s' → C (cons b s')) : C s := by
@@ -251,10 +255,9 @@ theorem mem_rec_on {C : Seq α → Prop} {a s} (M : a ∈ s)
     rw [TH]
     apply h1 _ _ (Or.inl rfl)
   -- Porting note: had to reshuffle `intro`
-  revert e; apply s.recOn _ fun b s' => _
-  · intro e; injection e
-  · intro b s' e
-    have h_eq : (cons b s').val (Nat.succ k) = s'.val k := by cases s'; rfl
+  cases' s with b s'
+  · injection e
+  · have h_eq : (cons b s').val (Nat.succ k) = s'.val k := by cases s' using Subtype.recOn; rfl
     rw [h_eq] at e
     apply h1 _ _ (Or.inr (IH e))
 
@@ -331,20 +334,21 @@ theorem eq_of_bisim (bisim : IsBisimulation R) {s₁ s₂} (r : s₁ ~ s₂) : s
     match t₁, t₂, e with
     | _, _, ⟨s, s', rfl, rfl, r⟩ => by
       suffices head s = head s' ∧ R (tail s) (tail s') from
-        And.imp id (fun r => ⟨tail s, tail s', by cases s; rfl, by cases s'; rfl, r⟩) this
+        And.imp id (fun r => ⟨tail s, tail s', by cases s using Subtype.recOn; rfl,
+          by cases s' using Subtype.recOn; rfl, r⟩) this
       have := bisim r; revert r this
-      apply recOn s _ _ <;> apply recOn s' _ _
+      cases' s with x s <;> cases' s' with x' s'
       · intro r _
         constructor
         · rfl
         · assumption
-      · intro x s _ this
+      · intro _ this
         rw [destruct_nil, destruct_cons] at this
         exact False.elim this
-      · intro x s _ this
+      · intro _ this
         rw [destruct_nil, destruct_cons] at this
         exact False.elim this
-      · intro x s x' s' _ this
+      · intro _ this
         rw [destruct_cons, destruct_cons] at this
         rw [head_cons, head_cons, tail_cons, tail_cons]
         cases' this with h1 h2
@@ -568,10 +572,10 @@ def toListOrStream (s : Seq α) [Decidable s.Terminates] : List α ⊕ Stream' 
 theorem nil_append (s : Seq α) : append nil s = s := by
   apply coinduction2; intro s
   dsimp [append]; rw [corec_eq]
-  dsimp [append]; apply recOn s _ _
+  dsimp [append]
+  cases' s with x s
   · trivial
-  · intro x s
-    rw [destruct_cons]
+  · rw [destruct_cons]
     dsimp
     exact ⟨rfl, s, rfl, rfl⟩
 
@@ -718,10 +722,9 @@ theorem cons_append (a : α) (s t) : append (cons a s) t = cons a (append s t) :
 @[simp]
 theorem append_nil (s : Seq α) : append s nil = s := by
   apply coinduction2 s; intro s
-  apply recOn s _ _
+  cases' s with x s
   · trivial
-  · intro x s
-    rw [cons_append, destruct_cons, destruct_cons]
+  · rw [cons_append, destruct_cons, destruct_cons]
     dsimp
     exact ⟨rfl, s, rfl, rfl⟩
 
@@ -732,15 +735,12 @@ theorem append_assoc (s t u : Seq α) : append (append s t) u = append s (append
     exact
       match s1, s2, h with
       | _, _, ⟨s, t, u, rfl, rfl⟩ => by
-        apply recOn s <;> simp
-        · apply recOn t <;> simp
-          · apply recOn u <;> simp
-            · intro _ u
-              refine ⟨nil, nil, u, ?_, ?_⟩ <;> simp
-          · intro _ t
-            refine ⟨nil, t, u, ?_, ?_⟩ <;> simp
-        · intro _ s
-          exact ⟨s, t, u, rfl, rfl⟩
+        cases' s with _ s <;> simp
+        · cases' t with _ t <;> simp
+          · cases' u with _ u <;> simp
+            · refine ⟨nil, nil, u, ?_, ?_⟩ <;> simp
+          · refine ⟨nil, t, u, ?_, ?_⟩ <;> simp
+        · exact ⟨s, t, u, rfl, rfl⟩
   · exact ⟨s, t, u, rfl, rfl⟩
 
 @[simp]
@@ -776,12 +776,10 @@ theorem map_append (f : α → β) (s t) : map f (append s t) = append (map f s)
   exact
     match s1, s2, h with
     | _, _, ⟨s, t, rfl, rfl⟩ => by
-      apply recOn s <;> simp
-      · apply recOn t <;> simp
-        · intro _ t
-          refine ⟨nil, t, ?_, ?_⟩ <;> simp
-      · intro _ s
-        exact ⟨s, t, rfl, rfl⟩
+      cases' s with _ s <;> simp
+      · cases' t with _ t <;> simp
+        · refine ⟨nil, t, ?_, ?_⟩ <;> simp
+      · exact ⟨s, t, rfl, rfl⟩
 
 @[simp]
 theorem map_get? (f : α → β) : ∀ s n, get? (map f s) n = (get? s n).map f
@@ -835,15 +833,13 @@ theorem join_cons (a : α) (s S) : join (cons (a, s) S) = cons a (append s (join
   exact
     match s1, s2, h with
     | s, _, Or.inl <| Eq.refl s => by
-      apply recOn s; · trivial
-      · intro x s
-        rw [destruct_cons]
+      cases' s with x s; · trivial
+      · rw [destruct_cons]
         exact ⟨rfl, Or.inl rfl⟩
     | _, _, Or.inr ⟨a, s, S, rfl, rfl⟩ => by
-      apply recOn s
+      cases' s with x s
       · simp [join_cons_cons, join_cons_nil]
-      · intro x s
-        simpa [join_cons_cons, join_cons_nil] using Or.inr ⟨x, s, S, rfl, rfl⟩
+      · simpa [join_cons_cons, join_cons_nil] using Or.inr ⟨x, s, S, rfl, rfl⟩
 
 @[simp]
 theorem join_append (S T : Seq (Seq1 α)) : join (append S T) = append (join S) (join T) := by
@@ -854,18 +850,15 @@ theorem join_append (S T : Seq (Seq1 α)) : join (append S T) = append (join S)
     exact
       match s1, s2, h with
       | _, _, ⟨s, S, T, rfl, rfl⟩ => by
-        apply recOn s <;> simp
-        · apply recOn S <;> simp
-          · apply recOn T
+        cases' s with _ s <;> simp
+        · cases' S with s S <;> simp
+          · cases' T with s T
             · simp
-            · intro s T
-              cases' s with a s; simp only [join_cons, destruct_cons, true_and]
+            · cases' s with a s; simp only [join_cons, destruct_cons, true_and]
               refine ⟨s, nil, T, ?_, ?_⟩ <;> simp
-          · intro s S
-            cases' s with a s
+          · cases' s with a s
             simpa using ⟨s, S, T, rfl, rfl⟩
-        · intro _ s
-          exact ⟨s, S, T, rfl, rfl⟩
+        · exact ⟨s, S, T, rfl, rfl⟩
   · refine ⟨nil, S, T, ?_, ?_⟩ <;> simp
 
 @[simp]
@@ -920,11 +913,11 @@ theorem of_mem_append {s₁ s₂ : Seq α} {a : α} (h : a ∈ append s₁ s₂)
   generalize e : append s₁ s₂ = ss; intro h; revert s₁
   apply mem_rec_on h _
   intro b s' o s₁
-  apply s₁.recOn _ fun c t₁ => _
+  cases' s₁ with c t₁
   · intro m _
     apply Or.inr
     simpa using m
-  · intro c t₁ m e
+  · intro m e
     have this := congr_arg destruct e
     cases' show a = c ∨ a ∈ append t₁ s₂ by simpa using m with e' m
     · rw [e']
@@ -1002,7 +995,7 @@ def bind (s : Seq1 α) (f : α → Seq1 β) : Seq1 β :=
 
 @[simp]
 theorem join_map_ret (s : Seq α) : Seq.join (Seq.map ret s) = s := by
-  apply coinduction2 s; intro s; apply recOn s <;> simp [ret]
+  apply coinduction2 s; intro s; cases s <;> simp [ret]
 
 @[simp]
 theorem bind_ret (f : α → β) : ∀ s, bind s (ret ∘ f) = map f s
@@ -1016,7 +1009,7 @@ theorem bind_ret (f : α → β) : ∀ s, bind s (ret ∘ f) = map f s
 theorem ret_bind (a : α) (f : α → Seq1 β) : bind (ret a) f = f a := by
   simp only [bind, map, ret.eq_1, map_nil]
   cases' f a with a s
-  apply recOn s <;> intros <;> simp
+  cases s <;> simp
 
 @[simp]
 theorem map_join' (f : α → β) (S) : Seq.map f (Seq.join S) = Seq.join (Seq.map (map f) S) := by
@@ -1028,18 +1021,16 @@ theorem map_join' (f : α → β) (S) : Seq.map f (Seq.join S) = Seq.join (Seq.m
     exact
       match s1, s2, h with
       | _, _, ⟨s, S, rfl, rfl⟩ => by
-        apply recOn s <;> simp
-        · apply recOn S <;> simp
-          · intro x S
-            cases' x with a s
+        cases' s with _ s <;> simp
+        · cases' S with x S <;> simp
+          · cases' x with a s
             simpa [map] using ⟨_, _, rfl, rfl⟩
-        · intro _ s
-          exact ⟨s, S, rfl, rfl⟩
+        · exact ⟨s, S, rfl, rfl⟩
   · refine ⟨nil, S, ?_, ?_⟩ <;> simp
 
 @[simp]
 theorem map_join (f : α → β) : ∀ S, map f (join S) = join (map (map f) S)
-  | ((a, s), S) => by apply recOn s <;> intros <;> simp [map]
+  | ((a, s), S) => by cases s <;> simp [map]
 
 @[simp]
 theorem join_join (SS : Seq (Seq1 (Seq1 α))) :
@@ -1052,24 +1043,21 @@ theorem join_join (SS : Seq (Seq1 (Seq1 α))) :
     exact
       match s1, s2, h with
       | _, _, ⟨s, SS, rfl, rfl⟩ => by
-        apply recOn s <;> simp
-        · apply recOn SS <;> simp
-          · intro S SS
-            cases' S with s S; cases' s with x s
+        cases' s with _ s <;> simp
+        · cases' SS with S SS <;> simp
+          · cases' S with s S; cases' s with x s
             simp only [Seq.join_cons, join_append, destruct_cons]
-            apply recOn s <;> simp
+            cases' s with x s <;> simp
             · exact ⟨_, _, rfl, rfl⟩
-            · intro x s
-              refine ⟨Seq.cons x (append s (Seq.join S)), SS, ?_, ?_⟩ <;> simp
-        · intro _ s
-          exact ⟨s, SS, rfl, rfl⟩
+            · refine ⟨Seq.cons x (append s (Seq.join S)), SS, ?_, ?_⟩ <;> simp
+        · exact ⟨s, SS, rfl, rfl⟩
   · refine ⟨nil, SS, ?_, ?_⟩ <;> simp
 
 @[simp]
 theorem bind_assoc (s : Seq1 α) (f : α → Seq1 β) (g : β → Seq1 γ) :
     bind (bind s f) g = bind s fun x : α => bind (f x) g := by
   cases' s with a s
-  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): was `simp [bind, map]`.
+  -- porting note (#10745): was `simp [bind, map]`.
   simp only [bind, map_pair, map_join]
   rw [← map_comp]
   simp only [show (fun x => join (map g (f x))) = join ∘ (map g ∘ f) from rfl]
@@ -1080,7 +1068,7 @@ theorem bind_assoc (s : Seq1 α) (f : α → Seq1 β) (g : β → Seq1 γ) :
   --   give names to variables.
   induction' s using recOn with x s_1 <;> induction' S using recOn with x_1 s_2 <;> simp
   · cases' x_1 with x t
-    apply recOn t <;> intros <;> simp
+    cases t <;> simp
   · cases' x_1 with y t; simp
 
 instance monad : Monad Seq1 where

From e7dd2f69282018159226b0473c04f7ac57ed8de0 Mon Sep 17 00:00:00 2001
From: Vasily Nesterov <vas.nesterov63@gmail.com>
Date: Mon, 9 Dec 2024 12:41:09 +0300
Subject: [PATCH 02/24] revert some

---
 Mathlib/Data/Seq/Seq.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
index d45af9a0910ef3..78a7c424856dbd 100644
--- a/Mathlib/Data/Seq/Seq.lean
+++ b/Mathlib/Data/Seq/Seq.lean
@@ -150,10 +150,8 @@ theorem ge_stable (s : Seq α) {aₙ : α} {n m : ℕ} (m_le_n : m ≤ n)
   have : s.get? m ≠ none := mt (s.le_stable m_le_n) this
   Option.ne_none_iff_exists'.mp this
 
-@[simp]
 theorem not_mem_nil (a : α) : a ∉ @nil α := fun ⟨_, (h : some a = none)⟩ => by injection h
 
-@[simp]
 theorem mem_cons (a : α) : ∀ s : Seq α, a ∈ cons a s
   | ⟨_, _⟩ => Stream'.mem_cons (some a) _
 
@@ -1057,7 +1055,7 @@ theorem join_join (SS : Seq (Seq1 (Seq1 α))) :
 theorem bind_assoc (s : Seq1 α) (f : α → Seq1 β) (g : β → Seq1 γ) :
     bind (bind s f) g = bind s fun x : α => bind (f x) g := by
   cases' s with a s
-  -- porting note (#10745): was `simp [bind, map]`.
+  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): was `simp [bind, map]`.
   simp only [bind, map_pair, map_join]
   rw [← map_comp]
   simp only [show (fun x => join (map g (f x))) = join ∘ (map g ∘ f) from rfl]

From db575e957c7fa02b89e533cd0924b7bf3bc01066 Mon Sep 17 00:00:00 2001
From: Vasily Nesterov <vas.nesterov63@gmail.com>
Date: Tue, 10 Dec 2024 12:01:07 +0300
Subject: [PATCH 03/24] general lemmas

---
 Mathlib/Data/Seq/Seq.lean | 60 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 60 insertions(+)

diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
index 78a7c424856dbd..19e06221571b5f 100644
--- a/Mathlib/Data/Seq/Seq.lean
+++ b/Mathlib/Data/Seq/Seq.lean
@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 import Mathlib.Data.Option.NAry
 import Mathlib.Data.Seq.Computation
+import Mathlib.Tactic.ApplyFun
 
 /-!
 # Possibly infinite lists
@@ -64,6 +65,10 @@ theorem val_cons (s : Seq α) (x : α) : (cons x s).val = some x::s.val :=
 def get? : Seq α → ℕ → Option α :=
   Subtype.val
 
+@[simp]
+theorem val_eq_get {α : Type u} (li : Seq α) (n : ℕ) : li.val n = li.get? n := by
+  rfl
+
 @[simp]
 theorem get?_mk (f hf) : @get? α ⟨f, hf⟩ = f :=
   rfl
@@ -165,6 +170,11 @@ theorem eq_or_mem_of_mem_cons {a b : α} : ∀ {s : Seq α}, a ∈ cons b s →
 theorem mem_cons_iff {a b : α} {s : Seq α} : a ∈ cons b s ↔ a = b ∨ a ∈ s :=
   ⟨eq_or_mem_of_mem_cons, by rintro (rfl | m) <;> [apply mem_cons; exact mem_cons_of_mem _ m]⟩
 
+@[simp]
+theorem get?_mem {α : Type u} {li : Seq α} {n : ℕ} {x : α} (h : li.get? n = .some x) : x ∈ li := by
+  simp [Membership.mem, Seq.Mem, Any]
+  exact ⟨n, h.symm⟩
+
 /-- Destructor for a sequence, resulting in either `none` (for `nil`) or
   `some (a, s)` (for `cons a s`). -/
 def destruct (s : Seq α) : Option (Seq1 α) :=
@@ -241,6 +251,46 @@ def recOn {motive : Seq α → Sort v} (s : Seq α) (nil : motive nil)
     rw [destruct_eq_cons H]
     apply cons
 
+@[simp]
+theorem noConfusion {α : Type u} {hd : α} {tl : Seq α} : (cons hd tl) ≠ .nil := by
+  intro h
+  apply_fun head at h
+  simp at h
+
+@[simp]
+theorem noConfusion_symm {α : Type u} {hd : α} {tl : Seq α} : .nil ≠ (cons hd tl) := by
+  symm
+  simp
+
+theorem cons_eq_cons {α : Type u} {hd hd' : α} {tl tl' : Seq α} :
+    (cons hd tl = cons hd' tl') ↔ (hd = hd' ∧ tl = tl') := by
+  constructor
+  · intro h
+    constructor
+    · apply_fun head at h
+      simpa using h
+    · apply_fun tail at h
+      simpa using h
+  · rintro ⟨h_hd, h_tl⟩
+    congr
+
+theorem head_eq_some {α : Type u} {li : Seq α} {hd : α} (h : li.head = some hd) :
+    li = cons hd li.tail := by
+  cases' li with hd' tl <;> simp at h
+  simpa [cons_eq_cons]
+
+theorem head_eq_none {α : Type u} {li : Seq α} (h : li.head = none) : li = nil := by
+  cases' li with hd tl
+  · rfl
+  · simp at h
+
+@[simp]
+theorem head_eq_none_iff {α : Type u} {li : Seq α} : li.head = none ↔ li = nil := by
+  constructor
+  · apply head_eq_none
+  · intro h
+    simp [h]
+
 theorem mem_rec_on {C : Seq α → Prop} {a s} (M : a ∈ s)
     (h1 : ∀ b s', a = b ∨ C s' → C (cons b s')) : C s := by
   cases' M with k e; unfold Stream'.get at e
@@ -303,6 +353,16 @@ theorem corec_eq (f : β → Option (α × β)) (b : β) :
   rw [Stream'.corec'_eq, Stream'.tail_cons]
   dsimp [Corec.f]; rw [h]
 
+theorem corec_nil {α : Type u} {β : Type u} (g : β → Option (α × β)) (b : β)
+    (h : g b = .none) : corec g b = nil := by
+  apply destruct_eq_nil
+  simp [h]
+
+theorem corec_cons {α : Type u} {β : Type u} {g : β → Option (α × β)} {b : β} {hd : α} {tl : β}
+    (h : g b = .some (hd, tl)) : corec g b = cons hd (corec g tl) := by
+  apply destruct_eq_cons
+  simp [h]
+
 section Bisim
 
 variable (R : Seq α → Seq α → Prop)

From 6c0d1eb014a4c55e1b4a6fe109709435315dea4a Mon Sep 17 00:00:00 2001
From: Vasily Nesterov <vas.nesterov63@gmail.com>
Date: Tue, 10 Dec 2024 12:04:47 +0300
Subject: [PATCH 04/24] drop lemmas

---
 Mathlib/Data/Seq/Seq.lean | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
index 19e06221571b5f..75c81e9ee5c551 100644
--- a/Mathlib/Data/Seq/Seq.lean
+++ b/Mathlib/Data/Seq/Seq.lean
@@ -943,6 +943,15 @@ def toList' {α} (s : Seq α) : Computation (List α) :=
       | some (a, s') => Sum.inr (a::l, s'))
     ([], s)
 
+@[simp]
+theorem drop_get? {α : Type u} {n m : ℕ} {li : Seq α} : (li.drop n).get? m = li.get? (n + m) := by
+  induction n generalizing m with
+  | zero => simp
+  | succ k ih =>
+    simp [Seq.get?_tail]
+    rw [show k + 1 + m = k + (m + 1) by omega]
+    apply ih
+
 theorem dropn_add (s : Seq α) (m) : ∀ n, drop s (m + n) = drop (drop s m) n
   | 0 => rfl
   | n + 1 => congr_arg tail (dropn_add s _ n)
@@ -955,6 +964,19 @@ theorem head_dropn (s : Seq α) (n) : head (drop s n) = get? s n := by
   induction' n with n IH generalizing s; · rfl
   rw [← get?_tail, ← dropn_tail]; apply IH
 
+theorem drop_succ_cons {α : Type u} {hd : α} {tl : Seq α} {n : ℕ} :
+    (cons hd tl).drop (n + 1) = tl.drop n := by
+  rw [← dropn_tail]
+  simp
+
+@[simp]
+theorem drop_nil {α : Type u} {n : ℕ} : (@nil α).drop n = nil := by
+  induction n with
+  | zero =>
+    simp
+  | succ m ih =>
+    simp [← dropn_tail, ih]
+
 theorem mem_map (f : α → β) {a : α} : ∀ {s : Seq α}, a ∈ s → f a ∈ map f s
   | ⟨_, _⟩ => Stream'.mem_map (Option.map f)
 

From de0847bf0a797b63ce3ebd9a528c0e4068d21831 Mon Sep 17 00:00:00 2001
From: Vasily Nesterov <vas.nesterov63@gmail.com>
Date: Tue, 10 Dec 2024 12:15:12 +0300
Subject: [PATCH 05/24] termination lemmas

---
 Mathlib/Data/Seq/Seq.lean | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
index 75c81e9ee5c551..70281770063562 100644
--- a/Mathlib/Data/Seq/Seq.lean
+++ b/Mathlib/Data/Seq/Seq.lean
@@ -661,11 +661,29 @@ theorem terminatedAt_ofList (l : List α) :
 theorem terminates_ofList (l : List α) : (ofList l).Terminates :=
   ⟨_, terminatedAt_ofList l⟩
 
-theorem terminatedAt_nil : TerminatedAt (nil : Seq α) 0 := rfl
+@[simp]
+theorem terminatedAt_nil {n : ℕ} : TerminatedAt (nil : Seq α) n := rfl
+
+@[simp]
+theorem cons_not_terminatedAt_zero {α : Type u} {hd : α} {tl : Seq α} :
+    ¬(cons hd tl).TerminatedAt 0 := by
+  simp [TerminatedAt]
+
+@[simp]
+theorem cons_terminatedAt_succ_iff {α : Type u} {hd : α} {tl : Seq α} {n : ℕ} :
+    (cons hd tl).TerminatedAt (n + 1) ↔ tl.TerminatedAt n := by
+  simp [TerminatedAt]
 
 @[simp]
 theorem terminates_nil : Terminates (nil : Seq α) := ⟨0, rfl⟩
 
+@[simp]
+theorem terminates_cons_iff {hd : α} {tl : Seq α} :
+    (cons hd tl).Terminates ↔ tl.Terminates := by
+  constructor <;> intro ⟨n, h⟩
+  · exact ⟨n, cons_terminatedAt_succ_iff.mp (terminated_stable _ (Nat.le_succ _) h)⟩
+  · exact ⟨n + 1, cons_terminatedAt_succ_iff.mpr h⟩
+
 @[simp]
 theorem length_nil : length (nil : Seq α) terminates_nil = 0 := rfl
 

From d0c4d00d80d7ad37819a71180bf3f274e0c09b1d Mon Sep 17 00:00:00 2001
From: Vasily Nesterov <vas.nesterov63@gmail.com>
Date: Tue, 10 Dec 2024 12:21:29 +0300
Subject: [PATCH 06/24] take lemmas

---
 Mathlib/Data/Seq/Seq.lean | 62 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 62 insertions(+)

diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
index 70281770063562..192ef92a630de4 100644
--- a/Mathlib/Data/Seq/Seq.lean
+++ b/Mathlib/Data/Seq/Seq.lean
@@ -637,6 +637,19 @@ theorem nil_append (s : Seq α) : append nil s = s := by
     dsimp
     exact ⟨rfl, s, rfl, rfl⟩
 
+@[simp]
+theorem take_nil {α : Type u} {n : ℕ} : (nil (α := α)).take n = List.nil := by
+  cases n <;> rfl
+
+@[simp]
+theorem take_zero {α : Type u} {li : Seq α} : li.take 0 = [] := by
+  cases li <;> rfl
+
+@[simp]
+theorem take_succ_cons {α : Type u} {n : ℕ} {hd : α} {tl : Seq α} :
+    (cons hd tl).take (n + 1) = hd :: tl.take n := by
+  rfl
+
 @[simp]
 theorem getElem?_take : ∀ (n k : ℕ) (s : Seq α),
     (s.take k)[n]? = if n < k then s.get? n else none
@@ -654,6 +667,27 @@ theorem getElem?_take : ∀ (n k : ℕ) (s : Seq α),
         | 0 => simp
         | n+1 => simp [List.get?_cons_succ, Nat.add_lt_add_iff_right, get?_cons_succ, getElem?_take]
 
+theorem get?_mem_take {α : Type u} {li : Seq α} {m n : ℕ} (h_mn : m < n) {x : α}
+    (h_get : li.get? m = .some x) : x ∈ li.take n := by
+  induction m generalizing n li with
+  | zero =>
+    obtain ⟨l, hl⟩ := Nat.exists_add_one_eq.mpr h_mn
+    rw [← hl]
+    rw [take, head_eq_some h_get]
+    simp
+  | succ k ih =>
+    obtain ⟨l, hl⟩ := Nat.exists_eq_add_of_lt h_mn
+    subst hl
+    have : ∃ y, li.get? 0 = .some y := by
+      apply ge_stable _ _ h_get
+      simp
+    obtain ⟨y, hy⟩ := this
+    rw [take, head_eq_some hy]
+    simp
+    right
+    apply ih (by omega)
+    rwa [get?_tail]
+
 theorem terminatedAt_ofList (l : List α) :
     (ofList l).TerminatedAt l.length := by
   simp [ofList, TerminatedAt]
@@ -741,6 +775,18 @@ theorem lt_length_iff {s : Seq α} {n : ℕ} {h : s.Terminates} :
     n < s.length h ↔ ∃ a, a ∈ s.get? n := by
   rw [← lt_length_iff']; simp [h]
 
+theorem length_take_le {α : Type u} {li : Seq α} {n : ℕ} : (li.take n).length ≤ n := by
+  induction n generalizing li with
+  | zero => simp
+  | succ m ih =>
+    rw [take]
+    cases li.destruct with
+    | none => simp
+    | some v =>
+      obtain ⟨x, r⟩ := v
+      simp
+      apply ih
+
 theorem length_take_of_le_length {s : Seq α} {n : ℕ}
     (hle : ∀ h : s.Terminates, n ≤ s.length h) : (s.take n).length = n := by
   induction n generalizing s with
@@ -982,6 +1028,7 @@ theorem head_dropn (s : Seq α) (n) : head (drop s n) = get? s n := by
   induction' n with n IH generalizing s; · rfl
   rw [← get?_tail, ← dropn_tail]; apply IH
 
+@[simp]
 theorem drop_succ_cons {α : Type u} {hd : α} {tl : Seq α} {n : ℕ} :
     (cons hd tl).drop (n + 1) = tl.drop n := by
   rw [← dropn_tail]
@@ -995,6 +1042,21 @@ theorem drop_nil {α : Type u} {n : ℕ} : (@nil α).drop n = nil := by
   | succ m ih =>
     simp [← dropn_tail, ih]
 
+theorem take_drop {α : Type u} {li : Seq α} {n m : ℕ} :
+    (li.take n).drop m = (li.drop m).take (n - m) := by
+  induction m generalizing n li with
+  | zero => simp
+  | succ k ih =>
+    cases' li with hd tl
+    · simp
+    cases n with
+    | zero => simp
+    | succ l =>
+      simp only [take, destruct_cons, List.drop_succ_cons, Nat.reduceSubDiff]
+      rw [ih]
+      congr 1
+      rw [drop_succ_cons]
+
 theorem mem_map (f : α → β) {a : α} : ∀ {s : Seq α}, a ∈ s → f a ∈ map f s
   | ⟨_, _⟩ => Stream'.mem_map (Option.map f)
 

From b4b2f7b07f8929b0a65e3e01390a62221b6afddf Mon Sep 17 00:00:00 2001
From: Vasily Nesterov <vas.nesterov63@gmail.com>
Date: Tue, 10 Dec 2024 12:35:00 +0300
Subject: [PATCH 07/24] fold lemmas

---
 Mathlib/Data/Seq/Seq.lean | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
index 192ef92a630de4..781ce7b64181a3 100644
--- a/Mathlib/Data/Seq/Seq.lean
+++ b/Mathlib/Data/Seq/Seq.lean
@@ -570,6 +570,15 @@ def splitAt : ℕ → Seq α → List α × Seq α
       let (l, r) := splitAt n s'
       (List.cons x l, r)
 
+/-- Folds a sequence using `f`, producing sequence of intermedieate values, i.e.
+`[init, f init li.head, f (f init li.head) li.tail.head, ...]`. -/
+def fold {α : Type u} {β : Type v} (li : Seq α) (init : β) (f : β → α → β) : Seq β :=
+  let g : β × Seq α → Option (β × (β × Seq α)) := fun (acc, x) =>
+    match destruct x with
+    | none => .none
+    | some (hd, tl) => .some (f acc hd, f acc hd, tl)
+  cons init <| corec g (init, li)
+
 section ZipWith
 
 /-- Combine two sequences with a function -/
@@ -1098,6 +1107,26 @@ theorem enum_cons (s : Seq α) (x : α) :
   · simp only [get?_enum, get?_cons_succ, map_get?, Option.map_map]
     congr
 
+@[simp]
+theorem fold_nil {α : Type u} {β : Type u} (init : β) (f : β → α → β) :
+    nil.fold init f = cons init nil := by
+  unfold fold
+  simp [corec_nil]
+
+@[simp]
+theorem fold_cons {α : Type u} {β : Type u} (init : β) (f : β → α → β) (hd : α) (tl : Seq α) :
+    (cons hd tl).fold init f = cons init (tl.fold (f init hd) f) := by
+  unfold fold
+  simp only
+  congr
+  rw [corec_cons]
+  simp
+
+@[simp]
+theorem fold_head {α : Type u} {β : Type u} (init : β) (f : β → α → β) (li : Seq α) :
+    (li.fold init f).head = init := by
+  simp [fold]
+
 end Seq
 
 namespace Seq1

From 620f8cab1c29d6913da47603fd4ce91bd5c60fe3 Mon Sep 17 00:00:00 2001
From: Vasily Nesterov <vas.nesterov63@gmail.com>
Date: Tue, 10 Dec 2024 12:45:35 +0300
Subject: [PATCH 08/24] rename

---
 Mathlib/Data/Seq/Seq.lean | 106 +++++++++++++++++++-------------------
 1 file changed, 53 insertions(+), 53 deletions(-)

diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
index 781ce7b64181a3..1417854243361f 100644
--- a/Mathlib/Data/Seq/Seq.lean
+++ b/Mathlib/Data/Seq/Seq.lean
@@ -66,7 +66,7 @@ def get? : Seq α → ℕ → Option α :=
   Subtype.val
 
 @[simp]
-theorem val_eq_get {α : Type u} (li : Seq α) (n : ℕ) : li.val n = li.get? n := by
+theorem val_eq_get (s : Seq α) (n : ℕ) : s.val n = s.get? n := by
   rfl
 
 @[simp]
@@ -171,7 +171,7 @@ theorem mem_cons_iff {a b : α} {s : Seq α} : a ∈ cons b s ↔ a = b ∨ a 
   ⟨eq_or_mem_of_mem_cons, by rintro (rfl | m) <;> [apply mem_cons; exact mem_cons_of_mem _ m]⟩
 
 @[simp]
-theorem get?_mem {α : Type u} {li : Seq α} {n : ℕ} {x : α} (h : li.get? n = .some x) : x ∈ li := by
+theorem get?_mem {s : Seq α} {n : ℕ} {x : α} (h : s.get? n = .some x) : x ∈ s := by
   simp [Membership.mem, Seq.Mem, Any]
   exact ⟨n, h.symm⟩
 
@@ -252,18 +252,18 @@ def recOn {motive : Seq α → Sort v} (s : Seq α) (nil : motive nil)
     apply cons
 
 @[simp]
-theorem noConfusion {α : Type u} {hd : α} {tl : Seq α} : (cons hd tl) ≠ .nil := by
+theorem noConfusion {x : α} {s : Seq α} : (cons x s) ≠ .nil := by
   intro h
   apply_fun head at h
   simp at h
 
 @[simp]
-theorem noConfusion_symm {α : Type u} {hd : α} {tl : Seq α} : .nil ≠ (cons hd tl) := by
+theorem noConfusion_symm {x : α} {s : Seq α} : .nil ≠ (cons x s) := by
   symm
   simp
 
-theorem cons_eq_cons {α : Type u} {hd hd' : α} {tl tl' : Seq α} :
-    (cons hd tl = cons hd' tl') ↔ (hd = hd' ∧ tl = tl') := by
+theorem cons_eq_cons {x x' : α} {s s' : Seq α} :
+    (cons x s = cons x' s') ↔ (x = x' ∧ s = s') := by
   constructor
   · intro h
     constructor
@@ -271,21 +271,21 @@ theorem cons_eq_cons {α : Type u} {hd hd' : α} {tl tl' : Seq α} :
       simpa using h
     · apply_fun tail at h
       simpa using h
-  · rintro ⟨h_hd, h_tl⟩
+  · rintro ⟨hx, hs⟩
     congr
 
-theorem head_eq_some {α : Type u} {li : Seq α} {hd : α} (h : li.head = some hd) :
-    li = cons hd li.tail := by
-  cases' li with hd' tl <;> simp at h
+theorem head_eq_some {s : Seq α} {x : α} (h : s.head = some x) :
+    s = cons x s.tail := by
+  cases' s with x' tl <;> simp at h
   simpa [cons_eq_cons]
 
-theorem head_eq_none {α : Type u} {li : Seq α} (h : li.head = none) : li = nil := by
-  cases' li with hd tl
+theorem head_eq_none {s : Seq α} (h : s.head = none) : s = nil := by
+  cases' s with x tl
   · rfl
   · simp at h
 
 @[simp]
-theorem head_eq_none_iff {α : Type u} {li : Seq α} : li.head = none ↔ li = nil := by
+theorem head_eq_none_iff {s : Seq α} : s.head = none ↔ s = nil := by
   constructor
   · apply head_eq_none
   · intro h
@@ -353,13 +353,13 @@ theorem corec_eq (f : β → Option (α × β)) (b : β) :
   rw [Stream'.corec'_eq, Stream'.tail_cons]
   dsimp [Corec.f]; rw [h]
 
-theorem corec_nil {α : Type u} {β : Type u} (g : β → Option (α × β)) (b : β)
-    (h : g b = .none) : corec g b = nil := by
+theorem corec_nil (f : β → Option (α × β)) (b : β)
+    (h : f b = .none) : corec f b = nil := by
   apply destruct_eq_nil
   simp [h]
 
-theorem corec_cons {α : Type u} {β : Type u} {g : β → Option (α × β)} {b : β} {hd : α} {tl : β}
-    (h : g b = .some (hd, tl)) : corec g b = cons hd (corec g tl) := by
+theorem corec_cons {f : β → Option (α × β)} {b : β} {x : α} {s : β}
+    (h : f b = .some (x, s)) : corec f b = cons x (corec f s) := by
   apply destruct_eq_cons
   simp [h]
 
@@ -571,13 +571,13 @@ def splitAt : ℕ → Seq α → List α × Seq α
       (List.cons x l, r)
 
 /-- Folds a sequence using `f`, producing sequence of intermedieate values, i.e.
-`[init, f init li.head, f (f init li.head) li.tail.head, ...]`. -/
-def fold {α : Type u} {β : Type v} (li : Seq α) (init : β) (f : β → α → β) : Seq β :=
-  let g : β × Seq α → Option (β × (β × Seq α)) := fun (acc, x) =>
+`[init, f init s.head, f (f init s.head) s.tail.head, ...]`. -/
+def fold (s : Seq α) (init : β) (f : β → α → β) : Seq β :=
+  let f : β × Seq α → Option (β × (β × Seq α)) := fun (acc, x) =>
     match destruct x with
     | none => .none
-    | some (hd, tl) => .some (f acc hd, f acc hd, tl)
-  cons init <| corec g (init, li)
+    | some (x, s) => .some (f acc x, f acc x, s)
+  cons init <| corec f (init, s)
 
 section ZipWith
 
@@ -647,16 +647,16 @@ theorem nil_append (s : Seq α) : append nil s = s := by
     exact ⟨rfl, s, rfl, rfl⟩
 
 @[simp]
-theorem take_nil {α : Type u} {n : ℕ} : (nil (α := α)).take n = List.nil := by
+theorem take_nil {n : ℕ} : (nil (α := α)).take n = List.nil := by
   cases n <;> rfl
 
 @[simp]
-theorem take_zero {α : Type u} {li : Seq α} : li.take 0 = [] := by
-  cases li <;> rfl
+theorem take_zero {s : Seq α} : s.take 0 = [] := by
+  cases s <;> rfl
 
 @[simp]
-theorem take_succ_cons {α : Type u} {n : ℕ} {hd : α} {tl : Seq α} :
-    (cons hd tl).take (n + 1) = hd :: tl.take n := by
+theorem take_succ_cons {n : ℕ} {x : α} {s : Seq α} :
+    (cons x s).take (n + 1) = x :: s.take n := by
   rfl
 
 @[simp]
@@ -676,9 +676,9 @@ theorem getElem?_take : ∀ (n k : ℕ) (s : Seq α),
         | 0 => simp
         | n+1 => simp [List.get?_cons_succ, Nat.add_lt_add_iff_right, get?_cons_succ, getElem?_take]
 
-theorem get?_mem_take {α : Type u} {li : Seq α} {m n : ℕ} (h_mn : m < n) {x : α}
-    (h_get : li.get? m = .some x) : x ∈ li.take n := by
-  induction m generalizing n li with
+theorem get?_mem_take {s : Seq α} {m n : ℕ} (h_mn : m < n) {x : α}
+    (h_get : s.get? m = .some x) : x ∈ s.take n := by
+  induction m generalizing n s with
   | zero =>
     obtain ⟨l, hl⟩ := Nat.exists_add_one_eq.mpr h_mn
     rw [← hl]
@@ -687,7 +687,7 @@ theorem get?_mem_take {α : Type u} {li : Seq α} {m n : ℕ} (h_mn : m < n) {x
   | succ k ih =>
     obtain ⟨l, hl⟩ := Nat.exists_eq_add_of_lt h_mn
     subst hl
-    have : ∃ y, li.get? 0 = .some y := by
+    have : ∃ y, s.get? 0 = .some y := by
       apply ge_stable _ _ h_get
       simp
     obtain ⟨y, hy⟩ := this
@@ -708,21 +708,21 @@ theorem terminates_ofList (l : List α) : (ofList l).Terminates :=
 theorem terminatedAt_nil {n : ℕ} : TerminatedAt (nil : Seq α) n := rfl
 
 @[simp]
-theorem cons_not_terminatedAt_zero {α : Type u} {hd : α} {tl : Seq α} :
-    ¬(cons hd tl).TerminatedAt 0 := by
+theorem cons_not_terminatedAt_zero {x : α} {s : Seq α} :
+    ¬(cons x s).TerminatedAt 0 := by
   simp [TerminatedAt]
 
 @[simp]
-theorem cons_terminatedAt_succ_iff {α : Type u} {hd : α} {tl : Seq α} {n : ℕ} :
-    (cons hd tl).TerminatedAt (n + 1) ↔ tl.TerminatedAt n := by
+theorem cons_terminatedAt_succ_iff {x : α} {s : Seq α} {n : ℕ} :
+    (cons x s).TerminatedAt (n + 1) ↔ s.TerminatedAt n := by
   simp [TerminatedAt]
 
 @[simp]
 theorem terminates_nil : Terminates (nil : Seq α) := ⟨0, rfl⟩
 
 @[simp]
-theorem terminates_cons_iff {hd : α} {tl : Seq α} :
-    (cons hd tl).Terminates ↔ tl.Terminates := by
+theorem terminates_cons_iff {x : α} {s : Seq α} :
+    (cons x s).Terminates ↔ s.Terminates := by
   constructor <;> intro ⟨n, h⟩
   · exact ⟨n, cons_terminatedAt_succ_iff.mp (terminated_stable _ (Nat.le_succ _) h)⟩
   · exact ⟨n + 1, cons_terminatedAt_succ_iff.mpr h⟩
@@ -784,12 +784,12 @@ theorem lt_length_iff {s : Seq α} {n : ℕ} {h : s.Terminates} :
     n < s.length h ↔ ∃ a, a ∈ s.get? n := by
   rw [← lt_length_iff']; simp [h]
 
-theorem length_take_le {α : Type u} {li : Seq α} {n : ℕ} : (li.take n).length ≤ n := by
-  induction n generalizing li with
+theorem length_take_le {s : Seq α} {n : ℕ} : (s.take n).length ≤ n := by
+  induction n generalizing s with
   | zero => simp
   | succ m ih =>
     rw [take]
-    cases li.destruct with
+    cases s.destruct with
     | none => simp
     | some v =>
       obtain ⟨x, r⟩ := v
@@ -1017,7 +1017,7 @@ def toList' {α} (s : Seq α) : Computation (List α) :=
     ([], s)
 
 @[simp]
-theorem drop_get? {α : Type u} {n m : ℕ} {li : Seq α} : (li.drop n).get? m = li.get? (n + m) := by
+theorem drop_get? {n m : ℕ} {s : Seq α} : (s.drop n).get? m = s.get? (n + m) := by
   induction n generalizing m with
   | zero => simp
   | succ k ih =>
@@ -1038,25 +1038,25 @@ theorem head_dropn (s : Seq α) (n) : head (drop s n) = get? s n := by
   rw [← get?_tail, ← dropn_tail]; apply IH
 
 @[simp]
-theorem drop_succ_cons {α : Type u} {hd : α} {tl : Seq α} {n : ℕ} :
-    (cons hd tl).drop (n + 1) = tl.drop n := by
+theorem drop_succ_cons {x : α} {s : Seq α} {n : ℕ} :
+    (cons x s).drop (n + 1) = s.drop n := by
   rw [← dropn_tail]
   simp
 
 @[simp]
-theorem drop_nil {α : Type u} {n : ℕ} : (@nil α).drop n = nil := by
+theorem drop_nil {n : ℕ} : (@nil α).drop n = nil := by
   induction n with
   | zero =>
     simp
   | succ m ih =>
     simp [← dropn_tail, ih]
 
-theorem take_drop {α : Type u} {li : Seq α} {n m : ℕ} :
-    (li.take n).drop m = (li.drop m).take (n - m) := by
-  induction m generalizing n li with
+theorem take_drop {s : Seq α} {n m : ℕ} :
+    (s.take n).drop m = (s.drop m).take (n - m) := by
+  induction m generalizing n s with
   | zero => simp
   | succ k ih =>
-    cases' li with hd tl
+    cases' s with x tl
     · simp
     cases n with
     | zero => simp
@@ -1108,14 +1108,14 @@ theorem enum_cons (s : Seq α) (x : α) :
     congr
 
 @[simp]
-theorem fold_nil {α : Type u} {β : Type u} (init : β) (f : β → α → β) :
+theorem fold_nil (init : β) (f : β → α → β) :
     nil.fold init f = cons init nil := by
   unfold fold
   simp [corec_nil]
 
 @[simp]
-theorem fold_cons {α : Type u} {β : Type u} (init : β) (f : β → α → β) (hd : α) (tl : Seq α) :
-    (cons hd tl).fold init f = cons init (tl.fold (f init hd) f) := by
+theorem fold_cons (init : β) (f : β → α → β) (x : α) (s : Seq α) :
+    (cons x s).fold init f = cons init (s.fold (f init x) f) := by
   unfold fold
   simp only
   congr
@@ -1123,8 +1123,8 @@ theorem fold_cons {α : Type u} {β : Type u} (init : β) (f : β → α → β)
   simp
 
 @[simp]
-theorem fold_head {α : Type u} {β : Type u} (init : β) (f : β → α → β) (li : Seq α) :
-    (li.fold init f).head = init := by
+theorem fold_head (init : β) (f : β → α → β) (s : Seq α) :
+    (s.fold init f).head = init := by
   simp [fold]
 
 end Seq

From d5c4cb61f38662f96c290c0f7d7b6bdb217c57a4 Mon Sep 17 00:00:00 2001
From: Vasily Nesterov <vas.nesterov63@gmail.com>
Date: Tue, 10 Dec 2024 12:59:57 +0300
Subject: [PATCH 09/24] fix

---
 Mathlib/Data/Seq/Seq.lean | 17 +++++++----------
 1 file changed, 7 insertions(+), 10 deletions(-)

diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
index 1417854243361f..809240ca0fe494 100644
--- a/Mathlib/Data/Seq/Seq.lean
+++ b/Mathlib/Data/Seq/Seq.lean
@@ -549,7 +549,7 @@ def drop (s : Seq α) : ℕ → Seq α
   | 0 => s
   | n + 1 => tail (drop s n)
 
-attribute [simp] drop
+-- attribute [simp] drop
 
 /-- Take the first `n` elements of the sequence (producing a list) -/
 def take : ℕ → Seq α → List α
@@ -1019,9 +1019,9 @@ def toList' {α} (s : Seq α) : Computation (List α) :=
 @[simp]
 theorem drop_get? {n m : ℕ} {s : Seq α} : (s.drop n).get? m = s.get? (n + m) := by
   induction n generalizing m with
-  | zero => simp
+  | zero => simp [drop]
   | succ k ih =>
-    simp [Seq.get?_tail]
+    simp [Seq.get?_tail, drop]
     rw [show k + 1 + m = k + (m + 1) by omega]
     apply ih
 
@@ -1040,21 +1040,18 @@ theorem head_dropn (s : Seq α) (n) : head (drop s n) = get? s n := by
 @[simp]
 theorem drop_succ_cons {x : α} {s : Seq α} {n : ℕ} :
     (cons x s).drop (n + 1) = s.drop n := by
-  rw [← dropn_tail]
-  simp
+  simp [← dropn_tail]
 
 @[simp]
 theorem drop_nil {n : ℕ} : (@nil α).drop n = nil := by
   induction n with
-  | zero =>
-    simp
-  | succ m ih =>
-    simp [← dropn_tail, ih]
+  | zero => simp [drop]
+  | succ m ih => simp [← dropn_tail, ih]
 
 theorem take_drop {s : Seq α} {n m : ℕ} :
     (s.take n).drop m = (s.drop m).take (n - m) := by
   induction m generalizing n s with
-  | zero => simp
+  | zero => simp [drop]
   | succ k ih =>
     cases' s with x tl
     · simp

From 6204386651cd35675c32dfff48c018bd93ab40fb Mon Sep 17 00:00:00 2001
From: Vasily Nesterov <vas.nesterov63@gmail.com>
Date: Tue, 10 Dec 2024 13:11:36 +0300
Subject: [PATCH 10/24] golf

---
 Mathlib/Data/Seq/Seq.lean | 22 ++++++++--------------
 1 file changed, 8 insertions(+), 14 deletions(-)

diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
index 809240ca0fe494..d4469299bf2988 100644
--- a/Mathlib/Data/Seq/Seq.lean
+++ b/Mathlib/Data/Seq/Seq.lean
@@ -171,9 +171,7 @@ theorem mem_cons_iff {a b : α} {s : Seq α} : a ∈ cons b s ↔ a = b ∨ a 
   ⟨eq_or_mem_of_mem_cons, by rintro (rfl | m) <;> [apply mem_cons; exact mem_cons_of_mem _ m]⟩
 
 @[simp]
-theorem get?_mem {s : Seq α} {n : ℕ} {x : α} (h : s.get? n = .some x) : x ∈ s := by
-  simp [Membership.mem, Seq.Mem, Any]
-  exact ⟨n, h.symm⟩
+theorem get?_mem {s : Seq α} {n : ℕ} {x : α} (h : s.get? n = .some x) : x ∈ s := ⟨n, h.symm⟩
 
 /-- Destructor for a sequence, resulting in either `none` (for `nil`) or
   `some (a, s)` (for `cons a s`). -/
@@ -258,9 +256,7 @@ theorem noConfusion {x : α} {s : Seq α} : (cons x s) ≠ .nil := by
   simp at h
 
 @[simp]
-theorem noConfusion_symm {x : α} {s : Seq α} : .nil ≠ (cons x s) := by
-  symm
-  simp
+theorem noConfusion_symm {x : α} {s : Seq α} : .nil ≠ (cons x s) := noConfusion.symm
 
 theorem cons_eq_cons {x x' : α} {s s' : Seq α} :
     (cons x s = cons x' s') ↔ (x = x' ∧ s = s') := by
@@ -271,7 +267,7 @@ theorem cons_eq_cons {x x' : α} {s s' : Seq α} :
       simpa using h
     · apply_fun tail at h
       simpa using h
-  · rintro ⟨hx, hs⟩
+  · intro ⟨hx, hs⟩
     congr
 
 theorem head_eq_some {s : Seq α} {x : α} (h : s.head = some x) :
@@ -681,8 +677,7 @@ theorem get?_mem_take {s : Seq α} {m n : ℕ} (h_mn : m < n) {x : α}
   induction m generalizing n s with
   | zero =>
     obtain ⟨l, hl⟩ := Nat.exists_add_one_eq.mpr h_mn
-    rw [← hl]
-    rw [take, head_eq_some h_get]
+    rw [← hl, take, head_eq_some h_get]
     simp
   | succ k ih =>
     obtain ⟨l, hl⟩ := Nat.exists_eq_add_of_lt h_mn
@@ -793,8 +788,7 @@ theorem length_take_le {s : Seq α} {n : ℕ} : (s.take n).length ≤ n := by
     | none => simp
     | some v =>
       obtain ⟨x, r⟩ := v
-      simp
-      apply ih
+      simpa using ih
 
 theorem length_take_of_le_length {s : Seq α} {n : ℕ}
     (hle : ∀ h : s.Terminates, n ≤ s.length h) : (s.take n).length = n := by
@@ -1022,8 +1016,8 @@ theorem drop_get? {n m : ℕ} {s : Seq α} : (s.drop n).get? m = s.get? (n + m)
   | zero => simp [drop]
   | succ k ih =>
     simp [Seq.get?_tail, drop]
-    rw [show k + 1 + m = k + (m + 1) by omega]
-    apply ih
+    convert ih using 2
+    omega
 
 theorem dropn_add (s : Seq α) (m) : ∀ n, drop s (m + n) = drop (drop s m) n
   | 0 => rfl
@@ -1114,7 +1108,7 @@ theorem fold_nil (init : β) (f : β → α → β) :
 theorem fold_cons (init : β) (f : β → α → β) (x : α) (s : Seq α) :
     (cons x s).fold init f = cons init (s.fold (f init x) f) := by
   unfold fold
-  simp only
+  dsimp only
   congr
   rw [corec_cons]
   simp

From f47f46318f061d864e0e667bfd78c9fc000fa9fe Mon Sep 17 00:00:00 2001
From: Vasily Nesterov <vas.nesterov63@gmail.com>
Date: Sat, 14 Dec 2024 03:13:07 +0300
Subject: [PATCH 11/24] suggestions

---
 Mathlib/Data/Seq/Seq.lean | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
index d4469299bf2988..8b1138ab8e8ad8 100644
--- a/Mathlib/Data/Seq/Seq.lean
+++ b/Mathlib/Data/Seq/Seq.lean
@@ -250,13 +250,13 @@ def recOn {motive : Seq α → Sort v} (s : Seq α) (nil : motive nil)
     apply cons
 
 @[simp]
-theorem noConfusion {x : α} {s : Seq α} : (cons x s) ≠ .nil := by
+theorem cons_ne_nil {x : α} {s : Seq α} : (cons x s) ≠ .nil := by
   intro h
   apply_fun head at h
   simp at h
 
 @[simp]
-theorem noConfusion_symm {x : α} {s : Seq α} : .nil ≠ (cons x s) := noConfusion.symm
+theorem nil_ne_cons {x : α} {s : Seq α} : .nil ≠ (cons x s) := cons_ne_nil.symm
 
 theorem cons_eq_cons {x x' : α} {s s' : Seq α} :
     (cons x s = cons x' s') ↔ (x = x' ∧ s = s') := by
@@ -267,7 +267,7 @@ theorem cons_eq_cons {x x' : α} {s s' : Seq α} :
       simpa using h
     · apply_fun tail at h
       simpa using h
-  · intro ⟨hx, hs⟩
+  · intro ⟨_, _⟩
     congr
 
 theorem head_eq_some {s : Seq α} {x : α} (h : s.head = some x) :
@@ -545,8 +545,6 @@ def drop (s : Seq α) : ℕ → Seq α
   | 0 => s
   | n + 1 => tail (drop s n)
 
--- attribute [simp] drop
-
 /-- Take the first `n` elements of the sequence (producing a list) -/
 def take : ℕ → Seq α → List α
   | 0, _ => []
@@ -566,7 +564,7 @@ def splitAt : ℕ → Seq α → List α × Seq α
       let (l, r) := splitAt n s'
       (List.cons x l, r)
 
-/-- Folds a sequence using `f`, producing sequence of intermedieate values, i.e.
+/-- Folds a sequence using `f`, producing a sequence of intermediate values, i.e.
 `[init, f init s.head, f (f init s.head) s.tail.head, ...]`. -/
 def fold (s : Seq α) (init : β) (f : β → α → β) : Seq β :=
   let f : β × Seq α → Option (β × (β × Seq α)) := fun (acc, x) =>

From 65a2c3f82b1be79979c47bda66a38131c6b40d91 Mon Sep 17 00:00:00 2001
From: Vasily Nesterov <vas.nesterov63@gmail.com>
Date: Thu, 19 Dec 2024 14:32:04 +0300
Subject: [PATCH 12/24] rearrange

---
 Mathlib/Data/Seq/Parallel.lean |   2 +-
 Mathlib/Data/Seq/Seq.lean      | 806 ++++++++++++++++++---------------
 2 files changed, 431 insertions(+), 377 deletions(-)

diff --git a/Mathlib/Data/Seq/Parallel.lean b/Mathlib/Data/Seq/Parallel.lean
index 16ea3f436d55d5..5bc0a9d1e2e954 100644
--- a/Mathlib/Data/Seq/Parallel.lean
+++ b/Mathlib/Data/Seq/Parallel.lean
@@ -166,7 +166,7 @@ theorem terminates_parallel {S : WSeq (Computation α)} {c} (h : c ∈ S) [T : T
         rw [D]
         simp only
         have TT := TT l'
-        rwa [Seq.destruct_eq_nil D, Seq.tail_nil] at TT
+        rwa [Seq.destruct_eq_none D, Seq.tail_nil] at TT
       · have D : Seq.destruct S = some (o, S.tail) := by
           dsimp [Seq.destruct]
           rw [e]
diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
index 8b1138ab8e8ad8..c088739361c4d1 100644
--- a/Mathlib/Data/Seq/Seq.lean
+++ b/Mathlib/Data/Seq/Seq.lean
@@ -43,6 +43,40 @@ namespace Seq
 
 variable {α : Type u} {β : Type v} {γ : Type w}
 
+/-- Get the nth element of a sequence (if it exists) -/
+def get? : Seq α → ℕ → Option α :=
+  Subtype.val
+
+@[simp]
+theorem val_eq_get (s : Seq α) (n : ℕ) : s.val n = s.get? n := by
+  rfl
+
+@[simp]
+theorem get?_mk (f hf) : @get? α ⟨f, hf⟩ = f :=
+  rfl
+
+theorem le_stable (s : Seq α) {m n} (h : m ≤ n) : s.get? m = none → s.get? n = none := by
+  cases' s with f al
+  induction' h with n _ IH
+  exacts [id, fun h2 => al (IH h2)]
+
+/-- If `s.get? n = some aₙ` for some value `aₙ`, then there is also some value `aₘ` such
+that `s.get? = some aₘ` for `m ≤ n`.
+-/
+theorem ge_stable (s : Seq α) {aₙ : α} {n m : ℕ} (m_le_n : m ≤ n)
+    (s_nth_eq_some : s.get? n = some aₙ) : ∃ aₘ : α, s.get? m = some aₘ :=
+  have : s.get? n ≠ none := by simp [s_nth_eq_some]
+  have : s.get? m ≠ none := mt (s.le_stable m_le_n) this
+  Option.ne_none_iff_exists'.mp this
+
+@[ext]
+protected theorem ext {s t : Seq α} (h : ∀ n : ℕ, s.get? n = t.get? n) : s = t :=
+  Subtype.eq <| funext h
+
+/-!
+### Constructors
+-/
+
 /-- The empty sequence -/
 def nil : Seq α :=
   ⟨Stream'.const none, fun {_} _ => rfl⟩
@@ -61,21 +95,15 @@ def cons (a : α) (s : Seq α) : Seq α :=
 theorem val_cons (s : Seq α) (x : α) : (cons x s).val = some x::s.val :=
   rfl
 
-/-- Get the nth element of a sequence (if it exists) -/
-def get? : Seq α → ℕ → Option α :=
-  Subtype.val
-
-@[simp]
-theorem val_eq_get (s : Seq α) (n : ℕ) : s.val n = s.get? n := by
-  rfl
-
 @[simp]
-theorem get?_mk (f hf) : @get? α ⟨f, hf⟩ = f :=
+theorem get?_nil (n : ℕ) : (@nil α).get? n = none :=
   rfl
 
 @[simp]
-theorem get?_nil (n : ℕ) : (@nil α).get? n = none :=
-  rfl
+theorem get?_zero_eq_none {s : Seq α} : s.get? 0 = none ↔ s = nil := by
+  refine ⟨fun h => ?_, fun h => h ▸ rfl⟩
+  ext1 n
+  exact le_stable s (Nat.zero_le _) h
 
 @[simp]
 theorem get?_cons_zero (a : α) (s : Seq α) : (cons a s).get? 0 = some a :=
@@ -85,9 +113,14 @@ theorem get?_cons_zero (a : α) (s : Seq α) : (cons a s).get? 0 = some a :=
 theorem get?_cons_succ (a : α) (s : Seq α) (n : ℕ) : (cons a s).get? (n + 1) = s.get? n :=
   rfl
 
-@[ext]
-protected theorem ext {s t : Seq α} (h : ∀ n : ℕ, s.get? n = t.get? n) : s = t :=
-  Subtype.eq <| funext h
+@[simp]
+theorem cons_ne_nil {x : α} {s : Seq α} : (cons x s) ≠ .nil := by
+  intro h
+  apply_fun (·.get? 0) at h
+  simp at h
+
+@[simp]
+theorem nil_ne_cons {x : α} {s : Seq α} : .nil ≠ (cons x s) := cons_ne_nil.symm
 
 theorem cons_injective2 : Function.Injective2 (cons : α → Seq α → Seq α) := fun x y s t h =>
   ⟨by rw [← Option.some_inj, ← get?_cons_zero, h, get?_cons_zero],
@@ -99,26 +132,16 @@ theorem cons_left_injective (s : Seq α) : Function.Injective fun x => cons x s
 theorem cons_right_injective (x : α) : Function.Injective (cons x) :=
   cons_injective2.right _
 
-/-- A sequence has terminated at position `n` if the value at position `n` equals `none`. -/
-def TerminatedAt (s : Seq α) (n : ℕ) : Prop :=
-  s.get? n = none
-
-/-- It is decidable whether a sequence terminates at a given position. -/
-instance terminatedAtDecidable (s : Seq α) (n : ℕ) : Decidable (s.TerminatedAt n) :=
-  decidable_of_iff' (s.get? n).isNone <| by unfold TerminatedAt; cases s.get? n <;> simp
-
-/-- A sequence terminates if there is some position `n` at which it has terminated. -/
-def Terminates (s : Seq α) : Prop :=
-  ∃ n : ℕ, s.TerminatedAt n
-
-theorem not_terminates_iff {s : Seq α} : ¬s.Terminates ↔ ∀ n, (s.get? n).isSome := by
-  simp only [Terminates, TerminatedAt, ← Ne.eq_def, Option.ne_none_iff_isSome, not_exists, iff_self]
+theorem cons_eq_cons {x x' : α} {s s' : Seq α} :
+    (cons x s = cons x' s') ↔ (x = x' ∧ s = s') := by
+  constructor
+  · apply cons_injective2
+  · intro ⟨_, _⟩
+    congr
 
-/-- Functorial action of the functor `Option (α × _)` -/
-@[simp]
-def omap (f : β → γ) : Option (α × β) → Option (α × γ)
-  | none => none
-  | some (a, b) => some (a, f b)
+/-!
+### Destructors
+-/
 
 /-- Get the first element of a sequence -/
 def head (s : Seq α) : Option α :=
@@ -130,55 +153,31 @@ def tail (s : Seq α) : Seq α :=
     cases' s with f al
     exact al n'⟩
 
-/-- member definition for `Seq`-/
-protected def Mem (s : Seq α) (a : α) :=
-  some a ∈ s.1
-
-instance : Membership α (Seq α) :=
-  ⟨Seq.Mem⟩
-
-theorem le_stable (s : Seq α) {m n} (h : m ≤ n) : s.get? m = none → s.get? n = none := by
-  cases' s with f al
-  induction' h with n _ IH
-  exacts [id, fun h2 => al (IH h2)]
-
-/-- If a sequence terminated at position `n`, it also terminated at `m ≥ n`. -/
-theorem terminated_stable : ∀ (s : Seq α) {m n : ℕ}, m ≤ n → s.TerminatedAt m → s.TerminatedAt n :=
-  le_stable
-
-/-- If `s.get? n = some aₙ` for some value `aₙ`, then there is also some value `aₘ` such
-that `s.get? = some aₘ` for `m ≤ n`.
--/
-theorem ge_stable (s : Seq α) {aₙ : α} {n m : ℕ} (m_le_n : m ≤ n)
-    (s_nth_eq_some : s.get? n = some aₙ) : ∃ aₘ : α, s.get? m = some aₘ :=
-  have : s.get? n ≠ none := by simp [s_nth_eq_some]
-  have : s.get? m ≠ none := mt (s.le_stable m_le_n) this
-  Option.ne_none_iff_exists'.mp this
-
-theorem not_mem_nil (a : α) : a ∉ @nil α := fun ⟨_, (h : some a = none)⟩ => by injection h
-
-theorem mem_cons (a : α) : ∀ s : Seq α, a ∈ cons a s
-  | ⟨_, _⟩ => Stream'.mem_cons (some a) _
-
-theorem mem_cons_of_mem (y : α) {a : α} : ∀ {s : Seq α}, a ∈ s → a ∈ cons y s
-  | ⟨_, _⟩ => Stream'.mem_cons_of_mem (some y)
+/-- Destructor for a sequence, resulting in either `none` (for `nil`) or
+  `some (a, s)` (for `cons a s`). -/
+def destruct (s : Seq α) : Option (Seq1 α) :=
+  (fun a' => (a', s.tail)) <$> get? s 0
 
-theorem eq_or_mem_of_mem_cons {a b : α} : ∀ {s : Seq α}, a ∈ cons b s → a = b ∨ a ∈ s
-  | ⟨_, _⟩, h => (Stream'.eq_or_mem_of_mem_cons h).imp_left fun h => by injection h
+-- Porting note: needed universe annotation to avoid universe issues
+theorem head_eq_destruct (s : Seq α) : head.{u} s = Prod.fst.{u} <$> destruct.{u} s := by
+  unfold destruct head; cases get? s 0 <;> rfl
 
 @[simp]
-theorem mem_cons_iff {a b : α} {s : Seq α} : a ∈ cons b s ↔ a = b ∨ a ∈ s :=
-  ⟨eq_or_mem_of_mem_cons, by rintro (rfl | m) <;> [apply mem_cons; exact mem_cons_of_mem _ m]⟩
+theorem get?_tail (s : Seq α) (n) : get? (tail s) n = get? s (n + 1) :=
+  rfl
 
 @[simp]
-theorem get?_mem {s : Seq α} {n : ℕ} {x : α} (h : s.get? n = .some x) : x ∈ s := ⟨n, h.symm⟩
+theorem destruct_nil : destruct (nil : Seq α) = none :=
+  rfl
 
-/-- Destructor for a sequence, resulting in either `none` (for `nil`) or
-  `some (a, s)` (for `cons a s`). -/
-def destruct (s : Seq α) : Option (Seq1 α) :=
-  (fun a' => (a', s.tail)) <$> get? s 0
+@[simp]
+theorem destruct_cons (a : α) : ∀ s, destruct (cons a s) = some (a, s)
+  | ⟨f, al⟩ => by
+    unfold cons destruct Functor.map
+    apply congr_arg fun s => some (a, s)
+    apply Subtype.eq; dsimp [tail]
 
-theorem destruct_eq_nil {s : Seq α} : destruct s = none → s = nil := by
+theorem destruct_eq_none {s : Seq α} : destruct s = none → s = nil := by
   dsimp [destruct]
   induction' f0 : get? s 0 <;> intro h
   · apply Subtype.eq
@@ -200,21 +199,6 @@ theorem destruct_eq_cons {s : Seq α} {a s'} : destruct s = some (a, s') → s =
     rw [← f0]
     exact (Stream'.eta f).symm
 
-@[simp]
-theorem destruct_nil : destruct (nil : Seq α) = none :=
-  rfl
-
-@[simp]
-theorem destruct_cons (a : α) : ∀ s, destruct (cons a s) = some (a, s)
-  | ⟨f, al⟩ => by
-    unfold cons destruct Functor.map
-    apply congr_arg fun s => some (a, s)
-    apply Subtype.eq; dsimp [tail]
-
--- Porting note: needed universe annotation to avoid universe issues
-theorem head_eq_destruct (s : Seq α) : head.{u} s = Prod.fst.{u} <$> destruct.{u} s := by
-  unfold destruct head; cases get? s 0 <;> rfl
-
 @[simp]
 theorem head_nil : head (nil : Seq α) = none :=
   rfl
@@ -233,9 +217,25 @@ theorem tail_cons (a : α) (s) : tail (cons a s) = s := by
   apply Subtype.eq
   dsimp [tail, cons]
 
+theorem head_eq_some {s : Seq α} {x : α} (h : s.head = some x) :
+    s = cons x s.tail := by
+  ext1 n
+  cases' n <;> simp
+  exact h
+
+theorem head_eq_none {s : Seq α} (h : s.head = none) : s = nil :=
+  get?_zero_eq_none.mp h
+
 @[simp]
-theorem get?_tail (s : Seq α) (n) : get? (tail s) n = get? s (n + 1) :=
-  rfl
+theorem head_eq_none_iff {s : Seq α} : s.head = none ↔ s = nil := by
+  constructor
+  · apply head_eq_none
+  · intro h
+    simp [h]
+
+/-!
+### Recursion and corecursion principles
+-/
 
 /-- Recursion principle for sequences, compare with `List.recOn`. -/
 @[cases_eliminator]
@@ -243,67 +243,17 @@ def recOn {motive : Seq α → Sort v} (s : Seq α) (nil : motive nil)
     (cons : ∀ x s, motive (cons x s)) :
     motive s := by
   cases' H : destruct s with v
-  · rw [destruct_eq_nil H]
+  · rw [destruct_eq_none H]
     apply nil
   · cases' v with a s'
     rw [destruct_eq_cons H]
     apply cons
 
+/-- Functorial action of the functor `Option (α × _)` -/
 @[simp]
-theorem cons_ne_nil {x : α} {s : Seq α} : (cons x s) ≠ .nil := by
-  intro h
-  apply_fun head at h
-  simp at h
-
-@[simp]
-theorem nil_ne_cons {x : α} {s : Seq α} : .nil ≠ (cons x s) := cons_ne_nil.symm
-
-theorem cons_eq_cons {x x' : α} {s s' : Seq α} :
-    (cons x s = cons x' s') ↔ (x = x' ∧ s = s') := by
-  constructor
-  · intro h
-    constructor
-    · apply_fun head at h
-      simpa using h
-    · apply_fun tail at h
-      simpa using h
-  · intro ⟨_, _⟩
-    congr
-
-theorem head_eq_some {s : Seq α} {x : α} (h : s.head = some x) :
-    s = cons x s.tail := by
-  cases' s with x' tl <;> simp at h
-  simpa [cons_eq_cons]
-
-theorem head_eq_none {s : Seq α} (h : s.head = none) : s = nil := by
-  cases' s with x tl
-  · rfl
-  · simp at h
-
-@[simp]
-theorem head_eq_none_iff {s : Seq α} : s.head = none ↔ s = nil := by
-  constructor
-  · apply head_eq_none
-  · intro h
-    simp [h]
-
-theorem mem_rec_on {C : Seq α → Prop} {a s} (M : a ∈ s)
-    (h1 : ∀ b s', a = b ∨ C s' → C (cons b s')) : C s := by
-  cases' M with k e; unfold Stream'.get at e
-  induction' k with k IH generalizing s
-  · have TH : s = cons a (tail s) := by
-      apply destruct_eq_cons
-      unfold destruct get? Functor.map
-      rw [← e]
-      rfl
-    rw [TH]
-    apply h1 _ _ (Or.inl rfl)
-  -- Porting note: had to reshuffle `intro`
-  cases' s with b s'
-  · injection e
-  · have h_eq : (cons b s').val (Nat.succ k) = s'.val k := by cases s' using Subtype.recOn; rfl
-    rw [h_eq] at e
-    apply h1 _ _ (Or.inr (IH e))
+def omap (f : β → γ) : Option (α × β) → Option (α × γ)
+  | none => none
+  | some (a, b) => some (a, f b)
 
 /-- Corecursor over pairs of `Option` values -/
 def Corec.f (f : β → Option (α × β)) : Option β → Option α × Option β
@@ -351,7 +301,7 @@ theorem corec_eq (f : β → Option (α × β)) (b : β) :
 
 theorem corec_nil (f : β → Option (α × β)) (b : β)
     (h : f b = .none) : corec f b = nil := by
-  apply destruct_eq_nil
+  apply destruct_eq_none
   simp [h]
 
 theorem corec_cons {f : β → Option (α × β)} {b : β} {x : α} {s : β}
@@ -359,6 +309,10 @@ theorem corec_cons {f : β → Option (α × β)} {b : β} {x : α} {s : β}
   apply destruct_eq_cons
   simp [h]
 
+/-!
+### Bisimulation
+-/
+
 section Bisim
 
 variable (R : Seq α → Seq α → Prop)
@@ -430,6 +384,158 @@ theorem coinduction2 (s) (f g : Seq α → Seq β)
   intro s1 s2 h; rcases h with ⟨s, h1, h2⟩
   rw [h1, h2]; apply H
 
+/-!
+### Termination
+-/
+
+/-- A sequence has terminated at position `n` if the value at position `n` equals `none`. -/
+def TerminatedAt (s : Seq α) (n : ℕ) : Prop :=
+  s.get? n = none
+
+/-- It is decidable whether a sequence terminates at a given position. -/
+instance terminatedAtDecidable (s : Seq α) (n : ℕ) : Decidable (s.TerminatedAt n) :=
+  decidable_of_iff' (s.get? n).isNone <| by unfold TerminatedAt; cases s.get? n <;> simp
+
+/-- A sequence terminates if there is some position `n` at which it has terminated. -/
+def Terminates (s : Seq α) : Prop :=
+  ∃ n : ℕ, s.TerminatedAt n
+
+/-- The length of a terminating sequence. -/
+def length (s : Seq α) (h : s.Terminates) : ℕ :=
+  Nat.find h
+
+/-- If a sequence terminated at position `n`, it also terminated at `m ≥ n`. -/
+theorem terminated_stable : ∀ (s : Seq α) {m n : ℕ}, m ≤ n → s.TerminatedAt m → s.TerminatedAt n :=
+  le_stable
+
+theorem not_terminates_iff {s : Seq α} : ¬s.Terminates ↔ ∀ n, (s.get? n).isSome := by
+  simp only [Terminates, TerminatedAt, ← Ne.eq_def, Option.ne_none_iff_isSome, not_exists, iff_self]
+
+@[simp]
+theorem terminatedAt_nil {n : ℕ} : TerminatedAt (nil : Seq α) n := rfl
+
+@[simp]
+theorem cons_not_terminatedAt_zero {x : α} {s : Seq α} :
+    ¬(cons x s).TerminatedAt 0 := by
+  simp [TerminatedAt]
+
+@[simp]
+theorem cons_terminatedAt_succ_iff {x : α} {s : Seq α} {n : ℕ} :
+    (cons x s).TerminatedAt (n + 1) ↔ s.TerminatedAt n := by
+  simp [TerminatedAt]
+
+@[simp]
+theorem terminates_nil : Terminates (nil : Seq α) := ⟨0, rfl⟩
+
+@[simp]
+theorem terminates_cons_iff {x : α} {s : Seq α} :
+    (cons x s).Terminates ↔ s.Terminates := by
+  constructor <;> intro ⟨n, h⟩
+  · exact ⟨n, cons_terminatedAt_succ_iff.mp (terminated_stable _ (Nat.le_succ _) h)⟩
+  · exact ⟨n + 1, cons_terminatedAt_succ_iff.mpr h⟩
+
+@[simp]
+theorem length_nil : length (nil : Seq α) terminates_nil = 0 := rfl
+
+@[simp] theorem length_eq_zero {s : Seq α} {h : s.Terminates} :
+    s.length h = 0 ↔ s = nil := by
+  simp [length, TerminatedAt]
+
+theorem terminatedAt_zero_iff {s : Seq α} : s.TerminatedAt 0 ↔ s = nil := by
+  refine ⟨?_, ?_⟩
+  · intro h
+    ext n
+    rw [le_stable _ (Nat.zero_le _) h]
+    simp
+  · rintro rfl
+    simp [TerminatedAt]
+
+/-- The statement of `length_le_iff'` does not assume that the sequence terminates. For a
+simpler statement of the theorem where the sequence is known to terminate see `length_le_iff` -/
+theorem length_le_iff' {s : Seq α} {n : ℕ} :
+    (∃ h, s.length h ≤ n) ↔ s.TerminatedAt n := by
+  simp only [length, Nat.find_le_iff, TerminatedAt, Terminates, exists_prop]
+  refine ⟨?_, ?_⟩
+  · rintro ⟨_, k, hkn, hk⟩
+    exact le_stable s hkn hk
+  · intro hn
+    exact ⟨⟨n, hn⟩, ⟨n, le_rfl, hn⟩⟩
+
+/-- The statement of `length_le_iff` assumes that the sequence terminates. For a
+statement of the where the sequence is not known to terminate see `length_le_iff'` -/
+theorem length_le_iff {s : Seq α} {n : ℕ} {h : s.Terminates} :
+    s.length h ≤ n ↔ s.TerminatedAt n := by
+  rw [← length_le_iff']; simp [h]
+
+/-- The statement of `lt_length_iff'` does not assume that the sequence terminates. For a
+simpler statement of the theorem where the sequence is known to terminate see `lt_length_iff` -/
+theorem lt_length_iff' {s : Seq α} {n : ℕ} :
+    (∀ h : s.Terminates, n < s.length h) ↔ ∃ a, a ∈ s.get? n := by
+  simp only [Terminates, TerminatedAt, length, Nat.lt_find_iff, forall_exists_index, Option.mem_def,
+    ← Option.ne_none_iff_exists', ne_eq]
+  refine ⟨?_, ?_⟩
+  · intro h hn
+    exact h n hn n le_rfl hn
+  · intro hn _ _ k hkn hk
+    exact hn <| le_stable s hkn hk
+
+/-- The statement of `length_le_iff` assumes that the sequence terminates. For a
+statement of the where the sequence is not known to terminate see `length_le_iff'` -/
+theorem lt_length_iff {s : Seq α} {n : ℕ} {h : s.Terminates} :
+    n < s.length h ↔ ∃ a, a ∈ s.get? n := by
+  rw [← lt_length_iff']; simp [h]
+
+/-!
+### Membership
+-/
+
+/-- member definition for `Seq`-/
+protected def Mem (s : Seq α) (a : α) :=
+  some a ∈ s.1
+
+instance : Membership α (Seq α) :=
+  ⟨Seq.Mem⟩
+
+@[simp]
+theorem get?_mem {s : Seq α} {n : ℕ} {x : α} (h : s.get? n = .some x) : x ∈ s := ⟨n, h.symm⟩
+
+theorem not_mem_nil (a : α) : a ∉ @nil α := fun ⟨_, (h : some a = none)⟩ => by injection h
+
+theorem mem_cons (a : α) : ∀ s : Seq α, a ∈ cons a s
+  | ⟨_, _⟩ => Stream'.mem_cons (some a) _
+
+theorem mem_cons_of_mem (y : α) {a : α} : ∀ {s : Seq α}, a ∈ s → a ∈ cons y s
+  | ⟨_, _⟩ => Stream'.mem_cons_of_mem (some y)
+
+theorem eq_or_mem_of_mem_cons {a b : α} : ∀ {s : Seq α}, a ∈ cons b s → a = b ∨ a ∈ s
+  | ⟨_, _⟩, h => (Stream'.eq_or_mem_of_mem_cons h).imp_left fun h => by injection h
+
+@[simp]
+theorem mem_cons_iff {a b : α} {s : Seq α} : a ∈ cons b s ↔ a = b ∨ a ∈ s :=
+  ⟨eq_or_mem_of_mem_cons, by rintro (rfl | m) <;> [apply mem_cons; exact mem_cons_of_mem _ m]⟩
+
+theorem mem_rec_on {C : Seq α → Prop} {a s} (M : a ∈ s)
+    (h1 : ∀ b s', a = b ∨ C s' → C (cons b s')) : C s := by
+  cases' M with k e; unfold Stream'.get at e
+  induction' k with k IH generalizing s
+  · have TH : s = cons a (tail s) := by
+      apply destruct_eq_cons
+      unfold destruct get? Functor.map
+      rw [← e]
+      rfl
+    rw [TH]
+    apply h1 _ _ (Or.inl rfl)
+  -- Porting note: had to reshuffle `intro`
+  cases' s with b s'
+  · injection e
+  · have h_eq : (cons b s').val (Nat.succ k) = s'.val k := by cases s' using Subtype.recOn; rfl
+    rw [h_eq] at e
+    apply h1 _ _ (Or.inr (IH e))
+
+/-!
+### Converting from/to other types
+-/
+
 /-- Embed a list as a sequence -/
 @[coe]
 def ofList (l : List α) : Seq α :=
@@ -497,13 +603,42 @@ end MLList
 unsafe def forceToList (s : Seq α) : List α :=
   (toMLList s).force
 
-/-- The sequence of natural numbers some 0, some 1, ... -/
-def nats : Seq ℕ :=
-  Stream'.nats
+/-- Take the first `n` elements of the sequence (producing a list) -/
+def take : ℕ → Seq α → List α
+  | 0, _ => []
+  | n + 1, s =>
+    match destruct s with
+    | none => []
+    | some (x, r) => List.cons x (take n r)
 
-@[simp]
-theorem nats_get? (n : ℕ) : nats.get? n = some n :=
-  rfl
+/-- Convert a sequence which is known to terminate into a list -/
+def toList (s : Seq α) (h : s.Terminates) : List α :=
+  take (length s h) s
+
+/-- Convert a sequence which is known not to terminate into a stream -/
+def toStream (s : Seq α) (h : ¬s.Terminates) : Stream' α := fun n =>
+  Option.get _ <| not_terminates_iff.1 h n
+
+/-- Convert a sequence into either a list or a stream depending on whether
+  it is finite or infinite. (Without decidability of the infiniteness predicate,
+  this is not constructively possible.) -/
+def toListOrStream (s : Seq α) [Decidable s.Terminates] : List α ⊕ Stream' α :=
+  if h : s.Terminates then Sum.inl (toList s h) else Sum.inr (toStream s h)
+
+/-- Convert a sequence into a list, embedded in a computation to allow for
+  the possibility of infinite sequences (in which case the computation
+  never returns anything). -/
+def toList' {α} (s : Seq α) : Computation (List α) :=
+  @Computation.corec (List α) (List α × Seq α)
+    (fun ⟨l, s⟩ =>
+      match destruct s with
+      | none => Sum.inl l.reverse
+      | some (a, s') => Sum.inr (a::l, s'))
+    ([], s)
+
+/-!
+### Operations on sequences
+-/
 
 /-- Append two sequences. If `s₁` is infinite, then `s₁ ++ s₂ = s₁`,
   otherwise it puts `s₂` at the location of the `nil` in `s₁`. -/
@@ -545,14 +680,6 @@ def drop (s : Seq α) : ℕ → Seq α
   | 0 => s
   | n + 1 => tail (drop s n)
 
-/-- Take the first `n` elements of the sequence (producing a list) -/
-def take : ℕ → Seq α → List α
-  | 0, _ => []
-  | n + 1, s =>
-    match destruct s with
-    | none => []
-    | some (x, r) => List.cons x (take n r)
-
 /-- Split a sequence at `n`, producing a finite initial segment
   and an infinite tail. -/
 def splitAt : ℕ → Seq α → List α × Seq α
@@ -564,81 +691,56 @@ def splitAt : ℕ → Seq α → List α × Seq α
       let (l, r) := splitAt n s'
       (List.cons x l, r)
 
-/-- Folds a sequence using `f`, producing a sequence of intermediate values, i.e.
-`[init, f init s.head, f (f init s.head) s.tail.head, ...]`. -/
-def fold (s : Seq α) (init : β) (f : β → α → β) : Seq β :=
-  let f : β × Seq α → Option (β × (β × Seq α)) := fun (acc, x) =>
-    match destruct x with
-    | none => .none
-    | some (x, s) => .some (f acc x, f acc x, s)
-  cons init <| corec f (init, s)
-
-section ZipWith
-
 /-- Combine two sequences with a function -/
 def zipWith (f : α → β → γ) (s₁ : Seq α) (s₂ : Seq β) : Seq γ :=
   ⟨fun n => Option.map₂ f (s₁.get? n) (s₂.get? n), fun {_} hn =>
     Option.map₂_eq_none_iff.2 <| (Option.map₂_eq_none_iff.1 hn).imp s₁.2 s₂.2⟩
 
-@[simp]
-theorem get?_zipWith (f : α → β → γ) (s s' n) :
-    (zipWith f s s').get? n = Option.map₂ f (s.get? n) (s'.get? n) :=
-  rfl
-
-end ZipWith
-
 /-- Pair two sequences into a sequence of pairs -/
 def zip : Seq α → Seq β → Seq (α × β) :=
   zipWith Prod.mk
 
-theorem get?_zip (s : Seq α) (t : Seq β) (n : ℕ) :
-    get? (zip s t) n = Option.map₂ Prod.mk (get? s n) (get? t n) :=
-  get?_zipWith _ _ _ _
-
 /-- Separate a sequence of pairs into two sequences -/
 def unzip (s : Seq (α × β)) : Seq α × Seq β :=
   (map Prod.fst s, map Prod.snd s)
 
+/-- The sequence of natural numbers some 0, some 1, ... -/
+def nats : Seq ℕ :=
+  Stream'.nats
+
 /-- Enumerate a sequence by tagging each element with its index. -/
 def enum (s : Seq α) : Seq (ℕ × α) :=
   Seq.zip nats s
 
-@[simp]
-theorem get?_enum (s : Seq α) (n : ℕ) : get? (enum s) n = Option.map (Prod.mk n) (get? s n) :=
-  get?_zip _ _ _
+/-- Folds a sequence using `f`, producing a sequence of intermediate values, i.e.
+`[init, f init s.head, f (f init s.head) s.tail.head, ...]`. -/
+def fold (s : Seq α) (init : β) (f : β → α → β) : Seq β :=
+  let f : β × Seq α → Option (β × (β × Seq α)) := fun (acc, x) =>
+    match destruct x with
+    | none => .none
+    | some (x, s) => .some (f acc x, f acc x, s)
+  cons init <| corec f (init, s)
+
+section OfStream
 
 @[simp]
-theorem enum_nil : enum (nil : Seq α) = nil :=
-  rfl
+theorem ofStream_cons (a : α) (s) : ofStream (a::s) = cons a (ofStream s) := by
+  apply Subtype.eq; simp only [ofStream, cons]; rw [Stream'.map_cons]
 
-/-- The length of a terminating sequence. -/
-def length (s : Seq α) (h : s.Terminates) : ℕ :=
-  Nat.find h
+end OfStream
 
-/-- Convert a sequence which is known to terminate into a list -/
-def toList (s : Seq α) (h : s.Terminates) : List α :=
-  take (length s h) s
+section OfList
 
-/-- Convert a sequence which is known not to terminate into a stream -/
-def toStream (s : Seq α) (h : ¬s.Terminates) : Stream' α := fun n =>
-  Option.get _ <| not_terminates_iff.1 h n
+theorem terminatedAt_ofList (l : List α) :
+    (ofList l).TerminatedAt l.length := by
+  simp [ofList, TerminatedAt]
 
-/-- Convert a sequence into either a list or a stream depending on whether
-  it is finite or infinite. (Without decidability of the infiniteness predicate,
-  this is not constructively possible.) -/
-def toListOrStream (s : Seq α) [Decidable s.Terminates] : List α ⊕ Stream' α :=
-  if h : s.Terminates then Sum.inl (toList s h) else Sum.inr (toStream s h)
+theorem terminates_ofList (l : List α) : (ofList l).Terminates :=
+  ⟨_, terminatedAt_ofList l⟩
 
-@[simp]
-theorem nil_append (s : Seq α) : append nil s = s := by
-  apply coinduction2; intro s
-  dsimp [append]; rw [corec_eq]
-  dsimp [append]
-  cases' s with x s
-  · trivial
-  · rw [destruct_cons]
-    dsimp
-    exact ⟨rfl, s, rfl, rfl⟩
+end OfList
+
+section Take
 
 @[simp]
 theorem take_nil {n : ℕ} : (nil (α := α)).take n = List.nil := by
@@ -661,7 +763,7 @@ theorem getElem?_take : ∀ (n k : ℕ) (s : Seq α),
     rw [take]
     cases h : destruct s with
     | none =>
-      simp [destruct_eq_nil h]
+      simp [destruct_eq_none h]
     | some a =>
       match a with
       | (x, r) =>
@@ -690,93 +792,6 @@ theorem get?_mem_take {s : Seq α} {m n : ℕ} (h_mn : m < n) {x : α}
     apply ih (by omega)
     rwa [get?_tail]
 
-theorem terminatedAt_ofList (l : List α) :
-    (ofList l).TerminatedAt l.length := by
-  simp [ofList, TerminatedAt]
-
-theorem terminates_ofList (l : List α) : (ofList l).Terminates :=
-  ⟨_, terminatedAt_ofList l⟩
-
-@[simp]
-theorem terminatedAt_nil {n : ℕ} : TerminatedAt (nil : Seq α) n := rfl
-
-@[simp]
-theorem cons_not_terminatedAt_zero {x : α} {s : Seq α} :
-    ¬(cons x s).TerminatedAt 0 := by
-  simp [TerminatedAt]
-
-@[simp]
-theorem cons_terminatedAt_succ_iff {x : α} {s : Seq α} {n : ℕ} :
-    (cons x s).TerminatedAt (n + 1) ↔ s.TerminatedAt n := by
-  simp [TerminatedAt]
-
-@[simp]
-theorem terminates_nil : Terminates (nil : Seq α) := ⟨0, rfl⟩
-
-@[simp]
-theorem terminates_cons_iff {x : α} {s : Seq α} :
-    (cons x s).Terminates ↔ s.Terminates := by
-  constructor <;> intro ⟨n, h⟩
-  · exact ⟨n, cons_terminatedAt_succ_iff.mp (terminated_stable _ (Nat.le_succ _) h)⟩
-  · exact ⟨n + 1, cons_terminatedAt_succ_iff.mpr h⟩
-
-@[simp]
-theorem length_nil : length (nil : Seq α) terminates_nil = 0 := rfl
-
-@[simp]
-theorem get?_zero_eq_none {s : Seq α} : s.get? 0 = none ↔ s = nil := by
-  refine ⟨fun h => ?_, fun h => h ▸ rfl⟩
-  ext1 n
-  exact le_stable s (Nat.zero_le _) h
-
-@[simp] theorem length_eq_zero {s : Seq α} {h : s.Terminates} :
-    s.length h = 0 ↔ s = nil := by
-  simp [length, TerminatedAt]
-
-theorem terminatedAt_zero_iff {s : Seq α} : s.TerminatedAt 0 ↔ s = nil := by
-  refine ⟨?_, ?_⟩
-  · intro h
-    ext n
-    rw [le_stable _ (Nat.zero_le _) h]
-    simp
-  · rintro rfl
-    simp [TerminatedAt]
-
-/-- The statement of `length_le_iff'` does not assume that the sequence terminates. For a
-simpler statement of the theorem where the sequence is known to terminate see `length_le_iff` -/
-theorem length_le_iff' {s : Seq α} {n : ℕ} :
-    (∃ h, s.length h ≤ n) ↔ s.TerminatedAt n := by
-  simp only [length, Nat.find_le_iff, TerminatedAt, Terminates, exists_prop]
-  refine ⟨?_, ?_⟩
-  · rintro ⟨_, k, hkn, hk⟩
-    exact le_stable s hkn hk
-  · intro hn
-    exact ⟨⟨n, hn⟩, ⟨n, le_rfl, hn⟩⟩
-
-/-- The statement of `length_le_iff` assumes that the sequence terminates. For a
-statement of the where the sequence is not known to terminate see `length_le_iff'` -/
-theorem length_le_iff {s : Seq α} {n : ℕ} {h : s.Terminates} :
-    s.length h ≤ n ↔ s.TerminatedAt n := by
-  rw [← length_le_iff']; simp [h]
-
-/-- The statement of `lt_length_iff'` does not assume that the sequence terminates. For a
-simpler statement of the theorem where the sequence is known to terminate see `lt_length_iff` -/
-theorem lt_length_iff' {s : Seq α} {n : ℕ} :
-    (∀ h : s.Terminates, n < s.length h) ↔ ∃ a, a ∈ s.get? n := by
-  simp only [Terminates, TerminatedAt, length, Nat.lt_find_iff, forall_exists_index, Option.mem_def,
-    ← Option.ne_none_iff_exists', ne_eq]
-  refine ⟨?_, ?_⟩
-  · intro h hn
-    exact h n hn n le_rfl hn
-  · intro hn _ _ k hkn hk
-    exact hn <| le_stable s hkn hk
-
-/-- The statement of `length_le_iff` assumes that the sequence terminates. For a
-statement of the where the sequence is not known to terminate see `length_le_iff'` -/
-theorem lt_length_iff {s : Seq α} {n : ℕ} {h : s.Terminates} :
-    n < s.length h ↔ ∃ a, a ∈ s.get? n := by
-  rw [← lt_length_iff']; simp [h]
-
 theorem length_take_le {s : Seq α} {n : ℕ} : (s.take n).length ≤ n := by
   induction n generalizing s with
   | zero => simp
@@ -804,6 +819,10 @@ theorem length_take_of_le_length {s : Seq α} {n : ℕ}
       rw [le_stable s (Nat.succ_le_of_lt hmn) hs] at this
       simp at this
 
+end Take
+
+section ToList
+
 @[simp]
 theorem length_toList (s : Seq α) (h : s.Terminates) : (toList s h).length = length s h := by
   rw [toList, length_take_of_le_length]
@@ -836,12 +855,27 @@ theorem getLast?_toList (s : Seq α) (h : s.Terminates) :
     (toList s h).getLast? = s.get? (s.length h - 1) := by
   rw [List.getLast?_eq_getElem?, getElem?_toList, length_toList]
 
+end ToList
+
+section Append
+
 @[simp]
 theorem cons_append (a : α) (s t) : append (cons a s) t = cons a (append s t) :=
   destruct_eq_cons <| by
     dsimp [append]; rw [corec_eq]
     dsimp [append]; rw [destruct_cons]
 
+@[simp]
+theorem nil_append (s : Seq α) : append nil s = s := by
+  apply coinduction2; intro s
+  dsimp [append]; rw [corec_eq]
+  dsimp [append]
+  cases' s with x s
+  · trivial
+  · rw [destruct_cons]
+    dsimp
+    exact ⟨rfl, s, rfl, rfl⟩
+
 @[simp]
 theorem append_nil (s : Seq α) : append s nil = s := by
   apply coinduction2 s; intro s
@@ -866,6 +900,36 @@ theorem append_assoc (s t u : Seq α) : append (append s t) u = append s (append
         · exact ⟨s, t, u, rfl, rfl⟩
   · exact ⟨s, t, u, rfl, rfl⟩
 
+theorem of_mem_append {s₁ s₂ : Seq α} {a : α} (h : a ∈ append s₁ s₂) : a ∈ s₁ ∨ a ∈ s₂ := by
+  have := h; revert this
+  generalize e : append s₁ s₂ = ss; intro h; revert s₁
+  apply mem_rec_on h _
+  intro b s' o s₁
+  cases' s₁ with c t₁
+  · intro m _
+    apply Or.inr
+    simpa using m
+  · intro m e
+    have this := congr_arg destruct e
+    cases' show a = c ∨ a ∈ append t₁ s₂ by simpa using m with e' m
+    · rw [e']
+      exact Or.inl (mem_cons _ _)
+    · cases' show c = b ∧ append t₁ s₂ = s' by simpa with i1 i2
+      cases' o with e' IH
+      · simp [i1, e']
+      · exact Or.imp_left (mem_cons_of_mem _) (IH m i2)
+
+theorem mem_append_left {s₁ s₂ : Seq α} {a : α} (h : a ∈ s₁) : a ∈ append s₁ s₂ := by
+  apply mem_rec_on h; intros; simp [*]
+
+end Append
+
+section Map
+
+@[simp]
+theorem map_get? (f : α → β) : ∀ s n, get? (map f s) n = (get? s n).map f
+  | ⟨_, _⟩, _ => rfl
+
 @[simp]
 theorem map_nil (f : α → β) : map f nil = nil :=
   rfl
@@ -890,24 +954,6 @@ theorem map_comp (f : α → β) (g : β → γ) : ∀ s : Seq α, map (g ∘ f)
     apply congr_arg fun f : _ → Option γ => Stream'.map f s
     ext ⟨⟩ <;> rfl
 
-@[simp]
-theorem map_append (f : α → β) (s t) : map f (append s t) = append (map f s) (map f t) := by
-  apply
-    eq_of_bisim (fun s1 s2 => ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)) _
-      ⟨s, t, rfl, rfl⟩
-  intro s1 s2 h
-  exact
-    match s1, s2, h with
-    | _, _, ⟨s, t, rfl, rfl⟩ => by
-      cases' s with _ s <;> simp
-      · cases' t with _ t <;> simp
-        · refine ⟨nil, t, ?_, ?_⟩ <;> simp
-      · exact ⟨s, t, rfl, rfl⟩
-
-@[simp]
-theorem map_get? (f : α → β) : ∀ s n, get? (map f s) n = (get? s n).map f
-  | ⟨_, _⟩, _ => rfl
-
 @[simp]
 theorem terminatedAt_map_iff {f : α → β} {s : Seq α} {n : ℕ} :
     (map f s).TerminatedAt n ↔ s.TerminatedAt n := by
@@ -926,16 +972,39 @@ theorem length_map {s : Seq α} {f : α → β} (h : (s.map f).Terminates) :
   ext
   simp
 
-instance : Functor Seq where map := @map
+theorem mem_map (f : α → β) {a : α} : ∀ {s : Seq α}, a ∈ s → f a ∈ map f s
+  | ⟨_, _⟩ => Stream'.mem_map (Option.map f)
+
+theorem exists_of_mem_map {f} {b : β} : ∀ {s : Seq α}, b ∈ map f s → ∃ a, a ∈ s ∧ f a = b :=
+  fun {s} h => by match s with
+  | ⟨g, al⟩ =>
+    let ⟨o, om, oe⟩ := @Stream'.exists_of_mem_map _ _ (Option.map f) (some b) g h
+    cases' o with a
+    · injection oe
+    · injection oe with h'; exact ⟨a, om, h'⟩
+
+@[simp]
+theorem map_append (f : α → β) (s t) : map f (append s t) = append (map f s) (map f t) := by
+  apply
+    eq_of_bisim (fun s1 s2 => ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)) _
+      ⟨s, t, rfl, rfl⟩
+  intro s1 s2 h
+  exact
+    match s1, s2, h with
+    | _, _, ⟨s, t, rfl, rfl⟩ => by
+      cases' s with _ s <;> simp
+      · cases' t with _ t <;> simp
+        · refine ⟨nil, t, ?_, ?_⟩ <;> simp
+      · exact ⟨s, t, rfl, rfl⟩
+
+end Map
+
+section Join
 
-instance : LawfulFunctor Seq where
-  id_map := @map_id
-  comp_map := @map_comp
-  map_const := rfl
 
 @[simp]
 theorem join_nil : join nil = (nil : Seq α) :=
-  destruct_eq_nil rfl
+  destruct_eq_none rfl
 
 --@[simp] -- Porting note: simp can prove: `join_cons` is more general
 theorem join_cons_nil (a : α) (S) : join (cons (a, nil) S) = cons a (join S) :=
@@ -984,29 +1053,9 @@ theorem join_append (S T : Seq (Seq1 α)) : join (append S T) = append (join S)
         · exact ⟨s, S, T, rfl, rfl⟩
   · refine ⟨nil, S, T, ?_, ?_⟩ <;> simp
 
-@[simp]
-theorem ofStream_cons (a : α) (s) : ofStream (a::s) = cons a (ofStream s) := by
-  apply Subtype.eq; simp only [ofStream, cons]; rw [Stream'.map_cons]
-
-@[simp]
-theorem ofList_append (l l' : List α) : ofList (l ++ l') = append (ofList l) (ofList l') := by
-  induction l <;> simp [*]
-
-@[simp]
-theorem ofStream_append (l : List α) (s : Stream' α) :
-    ofStream (l ++ₛ s) = append (ofList l) (ofStream s) := by
-  induction l <;> simp [*, Stream'.nil_append_stream, Stream'.cons_append_stream]
+end Join
 
-/-- Convert a sequence into a list, embedded in a computation to allow for
-  the possibility of infinite sequences (in which case the computation
-  never returns anything). -/
-def toList' {α} (s : Seq α) : Computation (List α) :=
-  @Computation.corec (List α) (List α × Seq α)
-    (fun ⟨l, s⟩ =>
-      match destruct s with
-      | none => Sum.inl l.reverse
-      | some (a, s') => Sum.inr (a::l, s'))
-    ([], s)
+section Drop
 
 @[simp]
 theorem drop_get? {n m : ℕ} {s : Seq α} : (s.drop n).get? m = s.get? (n + m) := by
@@ -1055,38 +1104,30 @@ theorem take_drop {s : Seq α} {n m : ℕ} :
       congr 1
       rw [drop_succ_cons]
 
-theorem mem_map (f : α → β) {a : α} : ∀ {s : Seq α}, a ∈ s → f a ∈ map f s
-  | ⟨_, _⟩ => Stream'.mem_map (Option.map f)
+end Drop
 
-theorem exists_of_mem_map {f} {b : β} : ∀ {s : Seq α}, b ∈ map f s → ∃ a, a ∈ s ∧ f a = b :=
-  fun {s} h => by match s with
-  | ⟨g, al⟩ =>
-    let ⟨o, om, oe⟩ := @Stream'.exists_of_mem_map _ _ (Option.map f) (some b) g h
-    cases' o with a
-    · injection oe
-    · injection oe with h'; exact ⟨a, om, h'⟩
+section ZipWith
 
-theorem of_mem_append {s₁ s₂ : Seq α} {a : α} (h : a ∈ append s₁ s₂) : a ∈ s₁ ∨ a ∈ s₂ := by
-  have := h; revert this
-  generalize e : append s₁ s₂ = ss; intro h; revert s₁
-  apply mem_rec_on h _
-  intro b s' o s₁
-  cases' s₁ with c t₁
-  · intro m _
-    apply Or.inr
-    simpa using m
-  · intro m e
-    have this := congr_arg destruct e
-    cases' show a = c ∨ a ∈ append t₁ s₂ by simpa using m with e' m
-    · rw [e']
-      exact Or.inl (mem_cons _ _)
-    · cases' show c = b ∧ append t₁ s₂ = s' by simpa with i1 i2
-      cases' o with e' IH
-      · simp [i1, e']
-      · exact Or.imp_left (mem_cons_of_mem _) (IH m i2)
+@[simp]
+theorem get?_zipWith (f : α → β → γ) (s s' n) :
+    (zipWith f s s').get? n = Option.map₂ f (s.get? n) (s'.get? n) :=
+  rfl
 
-theorem mem_append_left {s₁ s₂ : Seq α} {a : α} (h : a ∈ s₁) : a ∈ append s₁ s₂ := by
-  apply mem_rec_on h; intros; simp [*]
+theorem get?_zip (s : Seq α) (t : Seq β) (n : ℕ) :
+    get? (zip s t) n = Option.map₂ Prod.mk (get? s n) (get? t n) :=
+  get?_zipWith _ _ _ _
+
+@[simp]
+theorem nats_get? (n : ℕ) : nats.get? n = some n :=
+  rfl
+
+@[simp]
+theorem get?_enum (s : Seq α) (n : ℕ) : get? (enum s) n = Option.map (Prod.mk n) (get? s n) :=
+  get?_zip _ _ _
+
+@[simp]
+theorem enum_nil : enum (nil : Seq α) = nil :=
+  rfl
 
 @[simp]
 theorem enum_cons (s : Seq α) (x : α) :
@@ -1096,6 +1137,10 @@ theorem enum_cons (s : Seq α) (x : α) :
   · simp only [get?_enum, get?_cons_succ, map_get?, Option.map_map]
     congr
 
+end ZipWith
+
+section Fold
+
 @[simp]
 theorem fold_nil (init : β) (f : β → α → β) :
     nil.fold init f = cons init nil := by
@@ -1116,6 +1161,15 @@ theorem fold_head (init : β) (f : β → α → β) (s : Seq α) :
     (s.fold init f).head = init := by
   simp [fold]
 
+end Fold
+
+instance : Functor Seq where map := @map
+
+instance : LawfulFunctor Seq where
+  id_map := @map_id
+  comp_map := @map_comp
+  map_const := rfl
+
 end Seq
 
 namespace Seq1

From 30befcfacded4e20581a5624a1876990f57ff9e9 Mon Sep 17 00:00:00 2001
From: Vasily Nesterov <vas.nesterov63@gmail.com>
Date: Thu, 19 Dec 2024 14:57:29 +0300
Subject: [PATCH 13/24] return lost lemmas

---
 Mathlib/Data/Seq/Seq.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
index c088739361c4d1..d8d1dcf257db13 100644
--- a/Mathlib/Data/Seq/Seq.lean
+++ b/Mathlib/Data/Seq/Seq.lean
@@ -922,6 +922,15 @@ theorem of_mem_append {s₁ s₂ : Seq α} {a : α} (h : a ∈ append s₁ s₂)
 theorem mem_append_left {s₁ s₂ : Seq α} {a : α} (h : a ∈ s₁) : a ∈ append s₁ s₂ := by
   apply mem_rec_on h; intros; simp [*]
 
+@[simp]
+theorem ofList_append (l l' : List α) : ofList (l ++ l') = append (ofList l) (ofList l') := by
+  induction l <;> simp [*]
+
+@[simp]
+theorem ofStream_append (l : List α) (s : Stream' α) :
+    ofStream (l ++ₛ s) = append (ofList l) (ofStream s) := by
+  induction l <;> simp [*, Stream'.nil_append_stream, Stream'.cons_append_stream]
+
 end Append
 
 section Map

From 55b86cbb08696fae43bb8a2b5e72bfdf8306db9c Mon Sep 17 00:00:00 2001
From: Vasily Nesterov <vas.nesterov63@gmail.com>
Date: Sat, 21 Dec 2024 21:02:47 +0300
Subject: [PATCH 14/24] zip lemmas

---
 Mathlib/Data/Seq/Seq.lean | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
index d8d1dcf257db13..40fd582594e4b2 100644
--- a/Mathlib/Data/Seq/Seq.lean
+++ b/Mathlib/Data/Seq/Seq.lean
@@ -1134,6 +1134,38 @@ theorem nats_get? (n : ℕ) : nats.get? n = some n :=
 theorem get?_enum (s : Seq α) (n : ℕ) : get? (enum s) n = Option.map (Prod.mk n) (get? s n) :=
   get?_zip _ _ _
 
+@[simp]
+theorem zipWith_nil_left {f : α → β → γ} {s} :
+    zipWith f nil s = nil :=
+  rfl
+
+@[simp]
+theorem zipWith_nil_right {f : α → β → γ} {s} :
+    zipWith f s nil = nil := by
+  ext1
+  simp
+
+@[simp]
+theorem zipWith_cons_cons {f : α → β → γ} {x s x' s'} :
+    zipWith f (cons x s) (cons x' s') = cons (f x x') (zipWith f s s') := by
+  ext1 n
+  cases' n <;> simp
+
+@[simp]
+theorem zip_nil_left {s : Seq α} :
+    zip (@nil α) s = nil :=
+  rfl
+
+@[simp]
+theorem zip_nil_right {s : Seq α} :
+    zip s (@nil α) = nil :=
+  zipWith_nil_right
+
+@[simp]
+theorem zip_cons_cons {s s' : Seq α} {x x'} :
+    zip (cons x s) (cons x' s') = cons (x, x') (zip s s') :=
+  zipWith_cons_cons
+
 @[simp]
 theorem enum_nil : enum (nil : Seq α) = nil :=
   rfl

From 66a3e875f0887aaddd5897b8342bcfcacaef4f23 Mon Sep 17 00:00:00 2001
From: Vasily Nesterov <vas.nesterov63@gmail.com>
Date: Sat, 21 Dec 2024 21:48:55 +0300
Subject: [PATCH 15/24] zip_map lemmas

---
 Mathlib/Data/Seq/Seq.lean | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)

diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
index 40fd582594e4b2..5730689c46564e 100644
--- a/Mathlib/Data/Seq/Seq.lean
+++ b/Mathlib/Data/Seq/Seq.lean
@@ -1122,6 +1122,7 @@ theorem get?_zipWith (f : α → β → γ) (s s' n) :
     (zipWith f s s').get? n = Option.map₂ f (s.get? n) (s'.get? n) :=
   rfl
 
+@[simp]
 theorem get?_zip (s : Seq α) (t : Seq β) (n : ℕ) :
     get? (zip s t) n = Option.map₂ Prod.mk (get? s n) (get? t n) :=
   get?_zipWith _ _ _ _
@@ -1178,6 +1179,41 @@ theorem enum_cons (s : Seq α) (x : α) :
   · simp only [get?_enum, get?_cons_succ, map_get?, Option.map_map]
     congr
 
+universe u' v'
+variable {α' : Type u'} {β' : Type v'}
+
+theorem zipWith_map (s₁ : Seq α) (s₂ : Seq β) (f₁ : α → α') (f₂ : β → β') (g : α' → β' → γ) :
+    zipWith g (s₁.map f₁) (s₂.map f₂) = zipWith (fun a b ↦ g (f₁ a) (f₂ b)) s₁ s₂ := by
+  ext1 n
+  simp only [get?_zipWith, map_get?]
+  cases s₁.get? n <;> cases s₂.get? n <;> simp
+
+theorem zipWith_map_left (s₁ : Seq α) (s₂ : Seq β) (f : α → α') (g : α' → β → γ) :
+    zipWith g (s₁.map f) s₂ = zipWith (fun a b ↦ g (f a) b) s₁ s₂ := by
+  convert zipWith_map _ _ _ (@id β) _
+  simp
+
+theorem zipWith_map_right (s₁ : Seq α) (s₂ : Seq β) (f : β → β') (g : α → β' → γ) :
+    zipWith g s₁ (s₂.map f) = zipWith (fun a b ↦ g a (f b)) s₁ s₂ := by
+  convert zipWith_map _ _ (@id α) _ _
+  simp
+
+theorem zip_map (s₁ : Seq α) (s₂ : Seq β) (f₁ : α → α') (f₂ : β → β') :
+    (s₁.map f₁).zip (s₂.map f₂) = (s₁.zip s₂).map (Prod.map f₁ f₂) := by
+  ext1 n
+  simp
+  cases s₁.get? n <;> cases s₂.get? n <;> simp
+
+theorem zip_map_left (s₁ : Seq α) (s₂ : Seq β) (f : α → α') :
+    (s₁.map f).zip s₂ = (s₁.zip s₂).map (Prod.map f id) := by
+  convert zip_map _ _ _ _
+  simp
+
+theorem zip_map_right (s₁ : Seq α) (s₂ : Seq β) (f : β → β') :
+    s₁.zip (s₂.map f) = (s₁.zip s₂).map (Prod.map id f) := by
+  convert zip_map _ _ _ _
+  simp
+
 end ZipWith
 
 section Fold

From 69496e602be7d9750d28424604f83bcacbbf413f Mon Sep 17 00:00:00 2001
From: Vasily Nesterov <vas.nesterov63@gmail.com>
Date: Sat, 18 Jan 2025 17:33:47 +0300
Subject: [PATCH 16/24] remove import

---
 Mathlib/Data/Seq/Seq.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
index 5730689c46564e..ec72992f0c6f2c 100644
--- a/Mathlib/Data/Seq/Seq.lean
+++ b/Mathlib/Data/Seq/Seq.lean
@@ -5,7 +5,6 @@ Authors: Mario Carneiro
 -/
 import Mathlib.Data.Option.NAry
 import Mathlib.Data.Seq.Computation
-import Mathlib.Tactic.ApplyFun
 
 /-!
 # Possibly infinite lists
@@ -116,8 +115,7 @@ theorem get?_cons_succ (a : α) (s : Seq α) (n : ℕ) : (cons a s).get? (n + 1)
 @[simp]
 theorem cons_ne_nil {x : α} {s : Seq α} : (cons x s) ≠ .nil := by
   intro h
-  apply_fun (·.get? 0) at h
-  simp at h
+  simpa using congrArg (·.get? 0) h
 
 @[simp]
 theorem nil_ne_cons {x : α} {s : Seq α} : .nil ≠ (cons x s) := cons_ne_nil.symm

From 14c7f1219b8ed18c3e26e59e68c5a0072894bbb2 Mon Sep 17 00:00:00 2001
From: Vasilii Nesterov <vas.nesterov63@gmail.com>
Date: Mon, 10 Mar 2025 18:20:44 +0300
Subject: [PATCH 17/24] fix

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

diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
index 31fd24f2526928..945b69471b30ad 100644
--- a/Mathlib/Data/Seq/Seq.lean
+++ b/Mathlib/Data/Seq/Seq.lean
@@ -317,7 +317,7 @@ variable (R : Seq α → Seq α → Prop)
 
 local infixl:50 " ~ " => R
 
-/-- Bisimilarity relation over `Option` of `Seq1 α`-/
+/-- Bisimilarity relation over `Option` of `Seq1 α` -/
 def BisimO : Option (Seq1 α) → Option (Seq1 α) → Prop
   | none, none => True
   | some (a, s), some (a', s') => a = a' ∧ R s s'
@@ -487,7 +487,7 @@ theorem lt_length_iff {s : Seq α} {n : ℕ} {h : s.Terminates} :
 ### Membership
 -/
 
-/-- member definition for `Seq`-/
+/-- member definition for `Seq` -/
 protected def Mem (s : Seq α) (a : α) :=
   some a ∈ s.1
 
@@ -768,7 +768,7 @@ theorem getElem?_take : ∀ (n k : ℕ) (s : Seq α),
         rw [destruct_eq_cons h]
         match n with
         | 0 => simp
-        | n+1 => simp [List.get?_cons_succ, Nat.add_lt_add_iff_right, get?_cons_succ, getElem?_take]
+        | n+1 => simp [Nat.add_lt_add_iff_right, get?_cons_succ, getElem?_take]
 
 theorem get?_mem_take {s : Seq α} {m n : ℕ} (h_mn : m < n) {x : α}
     (h_get : s.get? m = .some x) : x ∈ s.take n := by
@@ -831,7 +831,7 @@ theorem length_toList (s : Seq α) (h : s.Terminates) : (toList s h).length = le
 theorem getElem?_toList (s : Seq α) (h : s.Terminates) (n : ℕ) : (toList s h)[n]? = s.get? n := by
   ext k
   simp only [ofList, toList, get?_mk, Option.mem_def, getElem?_take, Nat.lt_find_iff, length,
-    Option.ite_none_right_eq_some, and_iff_right_iff_imp, TerminatedAt, List.get?_eq_getElem?]
+    Option.ite_none_right_eq_some, and_iff_right_iff_imp, TerminatedAt]
   intro h m hmn
   let ⟨a, ha⟩ := ge_stable s hmn h
   simp [ha]
@@ -839,7 +839,7 @@ theorem getElem?_toList (s : Seq α) (h : s.Terminates) (n : ℕ) : (toList s h)
 @[simp]
 theorem ofList_toList (s : Seq α) (h : s.Terminates) :
     ofList (toList s h) = s := by
-  ext n; simp [ofList, List.get?_eq_getElem?]
+  ext n; simp [ofList]
 
 @[simp]
 theorem toList_ofList (l : List α) : toList (ofList l) (terminates_ofList l) = l :=

From a5f003eadef80d03dcc95449d5c873131ec3950e Mon Sep 17 00:00:00 2001
From: Vasilii Nesterov <vas.nesterov63@gmail.com>
Date: Mon, 10 Mar 2025 18:38:59 +0300
Subject: [PATCH 18/24] shake

---
 scripts/noshake.json | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/scripts/noshake.json b/scripts/noshake.json
index 271e14a52afc9f..a4d36bc1271f24 100644
--- a/scripts/noshake.json
+++ b/scripts/noshake.json
@@ -403,6 +403,7 @@
   "Mathlib.Data.Vector.Basic": ["Mathlib.Control.Applicative"],
   "Mathlib.Data.Set.Image":
   ["Batteries.Tactic.Congr", "Mathlib.Data.Set.SymmDiff"],
+  "Mathlib.Data.Seq.WSeq": ["Mathlib.Data.Option.Basic"],
   "Mathlib.Data.Seq.Parallel": ["Mathlib.Init.Data.Prod"],
   "Mathlib.Data.PEquiv": ["Batteries.Tactic.Congr"],
   "Mathlib.Data.Ordmap.Ordnode": ["Mathlib.Data.Option.Basic"],
@@ -473,7 +474,6 @@
   ["Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital"],
   "Mathlib.AlgebraicTopology.DoldKan.Notations":
   ["Mathlib.AlgebraicTopology.AlternatingFaceMapComplex"],
-  "Mathlib.Algebra.Notation.Lemmas": ["Batteries.Tactic.Init"],
   "Mathlib.Algebra.Star.Module": ["Mathlib.Algebra.Module.LinearMap.Star"],
   "Mathlib.Algebra.Ring.CentroidHom": ["Mathlib.Algebra.Algebra.Defs"],
   "Mathlib.Algebra.Order.Ring.Nat": ["Mathlib.Algebra.Order.Group.Nat"],
@@ -483,6 +483,7 @@
   "Mathlib.Algebra.Order.Field.Subfield":
   ["Mathlib.Algebra.Order.Field.InjSurj"],
   "Mathlib.Algebra.Order.CauSeq.Basic": ["Mathlib.Data.Setoid.Basic"],
+  "Mathlib.Algebra.Notation.Lemmas": ["Batteries.Tactic.Init"],
   "Mathlib.Algebra.MonoidAlgebra.Basic":
   ["Mathlib.LinearAlgebra.Finsupp.SumProd"],
   "Mathlib.Algebra.Module.Submodule.Order":

From 9fc6f2ef066172fcefa43931050563023e0cbf73 Mon Sep 17 00:00:00 2001
From: Vasilii Nesterov <vas.nesterov63@gmail.com>
Date: Mon, 10 Mar 2025 18:47:08 +0300
Subject: [PATCH 19/24] merge 2

---
 Mathlib/Data/Seq/Seq.lean | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
index 945b69471b30ad..41789856fcc8c5 100644
--- a/Mathlib/Data/Seq/Seq.lean
+++ b/Mathlib/Data/Seq/Seq.lean
@@ -552,6 +552,9 @@ theorem ofList_nil : ofList [] = (nil : Seq α) :=
 theorem ofList_get? (l : List α) (n : ℕ) : (ofList l).get? n = l[n]? :=
   rfl
 
+@[deprecated (since := "2025-02-21")]
+alias ofList_get := ofList_get?
+
 @[simp]
 theorem ofList_cons (a : α) (l : List α) : ofList (a::l) = cons a (ofList l) := by
   ext1 (_ | n) <;> rfl
@@ -578,13 +581,9 @@ def ofMLList : MLList Id α → Seq α :=
     | .none => none
     | .some (a, l') => some (a, l')
 
-@[deprecated (since := "2024-07-26")] alias ofLazyList := ofMLList
-
 instance coeMLList : Coe (MLList Id α) (Seq α) :=
   ⟨ofMLList⟩
 
-@[deprecated (since := "2024-07-26")] alias coeLazyList := coeMLList
-
 /-- Translate a sequence into a `MLList`. -/
 unsafe def toMLList : Seq α → MLList Id α
   | s =>
@@ -592,8 +591,6 @@ unsafe def toMLList : Seq α → MLList Id α
     | none => .nil
     | some (a, s') => .cons a (toMLList s')
 
-@[deprecated (since := "2024-07-26")] alias toLazyList := toMLList
-
 end MLList
 
 /-- Translate a sequence to a list. This function will run forever if

From 85d6a0a38f428c68aaecb70c0fdc40286cf154a1 Mon Sep 17 00:00:00 2001
From: Vasilii Nesterov <vas.nesterov63@gmail.com>
Date: Mon, 10 Mar 2025 19:09:41 +0300
Subject: [PATCH 20/24] remove primed cases

---
 Mathlib/Data/Seq/Seq.lean | 144 +++++++++++++++++++++-----------------
 1 file changed, 79 insertions(+), 65 deletions(-)

diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
index 41789856fcc8c5..c898cde38bec0a 100644
--- a/Mathlib/Data/Seq/Seq.lean
+++ b/Mathlib/Data/Seq/Seq.lean
@@ -55,7 +55,7 @@ theorem get?_mk (f hf) : @get? α ⟨f, hf⟩ = f :=
   rfl
 
 theorem le_stable (s : Seq α) {m n} (h : m ≤ n) : s.get? m = none → s.get? n = none := by
-  cases' s with f al
+  obtain ⟨f, al⟩ := s
   induction' h with n _ IH
   exacts [id, fun h2 => al (IH h2)]
 
@@ -148,7 +148,7 @@ def head (s : Seq α) : Option α :=
 /-- Get the tail of a sequence (or `nil` if the sequence is `nil`) -/
 def tail (s : Seq α) : Seq α :=
   ⟨s.1.tail, fun n' => by
-    cases' s with f al
+    obtain ⟨f, al⟩ := s
     exact al n'⟩
 
 /-- Destructor for a sequence, resulting in either `none` (for `nil`) or
@@ -188,7 +188,7 @@ theorem destruct_eq_cons {s : Seq α} {a s'} : destruct s = some (a, s') → s =
   dsimp [destruct]
   induction' f0 : get? s 0 with a' <;> intro h
   · contradiction
-  · cases' s with f al
+  · obtain ⟨f, al⟩ := s
     injections _ h1 h2
     rw [← h2]
     apply Subtype.eq
@@ -211,14 +211,14 @@ theorem tail_nil : tail (nil : Seq α) = nil :=
 
 @[simp]
 theorem tail_cons (a : α) (s) : tail (cons a s) = s := by
-  cases' s with f al
+  obtain ⟨f, al⟩ := s
   apply Subtype.eq
   dsimp [tail, cons]
 
 theorem head_eq_some {s : Seq α} {x : α} (h : s.head = some x) :
     s = cons x s.tail := by
   ext1 n
-  cases' n <;> simp
+  cases n <;> simp
   exact h
 
 theorem head_eq_none {s : Seq α} (h : s.head = none) : s = nil :=
@@ -240,10 +240,10 @@ theorem head_eq_none_iff {s : Seq α} : s.head = none ↔ s = nil := by
 def recOn {motive : Seq α → Sort v} (s : Seq α) (nil : motive nil)
     (cons : ∀ x s, motive (cons x s)) :
     motive s := by
-  cases' H : destruct s with v
+  rcases H : destruct s with - | v
   · rw [destruct_eq_none H]
     apply nil
-  · cases' v with a s'
+  · obtain ⟨a, s'⟩ := v
     rw [destruct_eq_cons H]
     apply cons
 
@@ -270,13 +270,13 @@ def corec (f : β → Option (α × β)) (b : β) : Seq α := by
   revert h; generalize some b = o; revert o
   induction' n with n IH <;> intro o
   · change (Corec.f f o).1 = none → (Corec.f f (Corec.f f o).2).1 = none
-    cases' o with b <;> intro h
+    rcases o with - | b <;> intro h
     · rfl
     dsimp [Corec.f] at h
     dsimp [Corec.f]
-    revert h; cases' h₁ : f b with s <;> intro h
+    revert h; rcases h₁ : f b with - | s <;> intro h
     · rfl
-    · cases' s with a b'
+    · obtain ⟨a, b'⟩ := s
       contradiction
   · rw [Stream'.corec'_eq (Corec.f f) (Corec.f f o).2, Stream'.corec'_eq (Corec.f f) o]
     exact IH (Corec.f f o).2
@@ -290,7 +290,7 @@ theorem corec_eq (f : β → Option (α × β)) (b : β) :
   rw [h]
   dsimp [Corec.f]
   induction' h : f b with s; · rfl
-  cases' s with a b'; dsimp [Corec.f]
+  obtain ⟨a, b'⟩ := s; dsimp [Corec.f]
   apply congr_arg fun b' => some (a, b')
   apply Subtype.eq
   dsimp [corec, tail]
@@ -343,7 +343,7 @@ theorem eq_of_bisim (bisim : IsBisimulation R) {s₁ s₂} (r : s₁ ~ s₂) : s
         And.imp id (fun r => ⟨tail s, tail s', by cases s using Subtype.recOn; rfl,
           by cases s' using Subtype.recOn; rfl, r⟩) this
       have := bisim r; revert r this
-      cases' s with x s <;> cases' s' with x' s'
+      cases s <;> cases s'
       · intro r _
         constructor
         · rfl
@@ -357,7 +357,7 @@ theorem eq_of_bisim (bisim : IsBisimulation R) {s₁ s₂} (r : s₁ ~ s₂) : s
       · intro _ this
         rw [destruct_cons, destruct_cons] at this
         rw [head_cons, head_cons, tail_cons, tail_cons]
-        cases' this with h1 h2
+        obtain ⟨h1, h2⟩ := this
         constructor
         · rw [h1]
         · exact h2
@@ -514,7 +514,7 @@ theorem mem_cons_iff {a b : α} {s : Seq α} : a ∈ cons b s ↔ a = b ∨ a 
 
 theorem mem_rec_on {C : Seq α → Prop} {a s} (M : a ∈ s)
     (h1 : ∀ b s', a = b ∨ C s' → C (cons b s')) : C s := by
-  cases' M with k e; unfold Stream'.get at e
+  obtain ⟨k, e⟩ := M; unfold Stream'.get at e
   induction' k with k IH generalizing s
   · have TH : s = cons a (tail s) := by
       apply destruct_eq_cons
@@ -524,9 +524,10 @@ theorem mem_rec_on {C : Seq α → Prop} {a s} (M : a ∈ s)
     rw [TH]
     apply h1 _ _ (Or.inl rfl)
   -- Porting note: had to reshuffle `intro`
-  cases' s with b s'
-  · injection e
-  · have h_eq : (cons b s').val (Nat.succ k) = s'.val k := by cases s' using Subtype.recOn; rfl
+  cases s with
+  | nil => injection e
+  | cons b s' =>
+    have h_eq : (cons b s').val (Nat.succ k) = s'.val k := by cases s' using Subtype.recOn; rfl
     rw [h_eq] at e
     apply h1 _ _ (Or.inr (IH e))
 
@@ -865,20 +866,20 @@ theorem nil_append (s : Seq α) : append nil s = s := by
   apply coinduction2; intro s
   dsimp [append]; rw [corec_eq]
   dsimp [append]
-  cases' s with x s
+  cases s
   · trivial
   · rw [destruct_cons]
     dsimp
-    exact ⟨rfl, s, rfl, rfl⟩
+    exact ⟨rfl, _, rfl, rfl⟩
 
 @[simp]
 theorem append_nil (s : Seq α) : append s nil = s := by
   apply coinduction2 s; intro s
-  cases' s with x s
+  cases s
   · trivial
   · rw [cons_append, destruct_cons, destruct_cons]
     dsimp
-    exact ⟨rfl, s, rfl, rfl⟩
+    exact ⟨rfl, _, rfl, rfl⟩
 
 @[simp]
 theorem append_assoc (s t u : Seq α) : append (append s t) u = append s (append t u) := by
@@ -887,12 +888,14 @@ theorem append_assoc (s t u : Seq α) : append (append s t) u = append s (append
     exact
       match s1, s2, h with
       | _, _, ⟨s, t, u, rfl, rfl⟩ => by
-        cases' s with _ s <;> simp
-        · cases' t with _ t <;> simp
-          · cases' u with _ u <;> simp
-            · refine ⟨nil, nil, u, ?_, ?_⟩ <;> simp
-          · refine ⟨nil, t, u, ?_, ?_⟩ <;> simp
-        · exact ⟨s, t, u, rfl, rfl⟩
+        cases s <;> simp
+        case nil =>
+          cases t <;> simp
+          case nil =>
+            cases u <;> simp
+            case cons _ u => refine ⟨nil, nil, u, ?_, ?_⟩ <;> simp
+          case cons _ t => refine ⟨nil, t, u, ?_, ?_⟩ <;> simp
+        case cons _ s => exact ⟨s, t, u, rfl, rfl⟩
   · exact ⟨s, t, u, rfl, rfl⟩
 
 theorem of_mem_append {s₁ s₂ : Seq α} {a : α} (h : a ∈ append s₁ s₂) : a ∈ s₁ ∨ a ∈ s₂ := by
@@ -900,17 +903,19 @@ theorem of_mem_append {s₁ s₂ : Seq α} {a : α} (h : a ∈ append s₁ s₂)
   generalize e : append s₁ s₂ = ss; intro h; revert s₁
   apply mem_rec_on h _
   intro b s' o s₁
-  cases' s₁ with c t₁
-  · intro m _
+  cases s₁ with
+  | nil =>
+    intro m _
     apply Or.inr
     simpa using m
-  · intro m e
+  | cons c t₁ =>
+    intro m e
     have this := congr_arg destruct e
-    cases' show a = c ∨ a ∈ append t₁ s₂ by simpa using m with e' m
+    rcases show a = c ∨ a ∈ append t₁ s₂ by simpa using m with e' | m
     · rw [e']
       exact Or.inl (mem_cons _ _)
-    · cases' show c = b ∧ append t₁ s₂ = s' by simpa with i1 i2
-      cases' o with e' IH
+    · obtain ⟨i1, i2⟩ := show c = b ∧ append t₁ s₂ = s' by simpa
+      rcases o with e' | IH
       · simp [i1, e']
       · exact Or.imp_left (mem_cons_of_mem _) (IH m i2)
 
@@ -983,7 +988,7 @@ theorem exists_of_mem_map {f} {b : β} : ∀ {s : Seq α}, b ∈ map f s → ∃
   fun {s} h => by match s with
   | ⟨g, al⟩ =>
     let ⟨o, om, oe⟩ := @Stream'.exists_of_mem_map _ _ (Option.map f) (some b) g h
-    cases' o with a
+    rcases o with - | a
     · injection oe
     · injection oe with h'; exact ⟨a, om, h'⟩
 
@@ -996,10 +1001,11 @@ theorem map_append (f : α → β) (s t) : map f (append s t) = append (map f s)
   exact
     match s1, s2, h with
     | _, _, ⟨s, t, rfl, rfl⟩ => by
-      cases' s with _ s <;> simp
-      · cases' t with _ t <;> simp
-        · refine ⟨nil, t, ?_, ?_⟩ <;> simp
-      · exact ⟨s, t, rfl, rfl⟩
+      cases s <;> simp
+      case nil =>
+        cases t <;> simp
+        case cons _ t => refine ⟨nil, t, ?_, ?_⟩ <;> simp
+      case cons _ s => exact ⟨s, t, rfl, rfl⟩
 
 end Map
 
@@ -1029,13 +1035,13 @@ theorem join_cons (a : α) (s S) : join (cons (a, s) S) = cons a (append s (join
   exact
     match s1, s2, h with
     | s, _, Or.inl <| Eq.refl s => by
-      cases' s with x s; · trivial
+      cases s; · trivial
       · rw [destruct_cons]
         exact ⟨rfl, Or.inl rfl⟩
     | _, _, Or.inr ⟨a, s, S, rfl, rfl⟩ => by
-      cases' s with x s
+      cases s
       · simp [join_cons_cons, join_cons_nil]
-      · simpa [join_cons_cons, join_cons_nil] using Or.inr ⟨x, s, S, rfl, rfl⟩
+      · simpa [join_cons_cons, join_cons_nil] using Or.inr ⟨_, _, S, rfl, rfl⟩
 
 @[simp]
 theorem join_append (S T : Seq (Seq1 α)) : join (append S T) = append (join S) (join T) := by
@@ -1046,15 +1052,19 @@ theorem join_append (S T : Seq (Seq1 α)) : join (append S T) = append (join S)
     exact
       match s1, s2, h with
       | _, _, ⟨s, S, T, rfl, rfl⟩ => by
-        cases' s with _ s <;> simp
-        · cases' S with s S <;> simp
-          · cases' T with s T
-            · simp
-            · cases' s with a s; simp only [join_cons, destruct_cons, true_and]
+        cases s <;> simp
+        case nil =>
+          cases S <;> simp
+          case nil =>
+            cases T with
+            | nil => simp
+            | cons s T =>
+              obtain ⟨a, s⟩ := s; simp only [join_cons, destruct_cons, true_and]
               refine ⟨s, nil, T, ?_, ?_⟩ <;> simp
-          · cases' s with a s
+          case cons s S =>
+            obtain ⟨a, s⟩ := s
             simpa using ⟨s, S, T, rfl, rfl⟩
-        · exact ⟨s, S, T, rfl, rfl⟩
+        case cons _ s => exact ⟨s, S, T, rfl, rfl⟩
   · refine ⟨nil, S, T, ?_, ?_⟩ <;> simp
 
 end Join
@@ -1098,7 +1108,7 @@ theorem take_drop {s : Seq α} {n m : ℕ} :
   induction m generalizing n s with
   | zero => simp [drop]
   | succ k ih =>
-    cases' s with x tl
+    cases s
     · simp
     cases n with
     | zero => simp
@@ -1145,7 +1155,7 @@ theorem zipWith_nil_right {f : α → β → γ} {s} :
 theorem zipWith_cons_cons {f : α → β → γ} {x s x' s'} :
     zipWith f (cons x s) (cons x' s') = cons (f x x') (zipWith f s s') := by
   ext1 n
-  cases' n <;> simp
+  cases n <;> simp
 
 @[simp]
 theorem zip_nil_left {s : Seq α} :
@@ -1312,7 +1322,7 @@ theorem bind_ret (f : α → β) : ∀ s, bind s (ret ∘ f) = map f s
 @[simp]
 theorem ret_bind (a : α) (f : α → Seq1 β) : bind (ret a) f = f a := by
   simp only [bind, map, ret.eq_1, map_nil]
-  cases' f a with a s
+  obtain ⟨a, s⟩ := f a
   cases s <;> simp
 
 @[simp]
@@ -1325,11 +1335,13 @@ theorem map_join' (f : α → β) (S) : Seq.map f (Seq.join S) = Seq.join (Seq.m
     exact
       match s1, s2, h with
       | _, _, ⟨s, S, rfl, rfl⟩ => by
-        cases' s with _ s <;> simp
-        · cases' S with x S <;> simp
-          · cases' x with a s
+        cases s <;> simp
+        case nil =>
+          cases S <;> simp
+          case cons x S =>
+            obtain ⟨a, s⟩ := x
             simpa [map] using ⟨_, _, rfl, rfl⟩
-        · exact ⟨s, S, rfl, rfl⟩
+        case cons _ s => exact ⟨s, S, rfl, rfl⟩
   · refine ⟨nil, S, ?_, ?_⟩ <;> simp
 
 @[simp]
@@ -1347,20 +1359,22 @@ theorem join_join (SS : Seq (Seq1 (Seq1 α))) :
     exact
       match s1, s2, h with
       | _, _, ⟨s, SS, rfl, rfl⟩ => by
-        cases' s with _ s <;> simp
-        · cases' SS with S SS <;> simp
-          · cases' S with s S; cases' s with x s
+        cases s <;> simp
+        case nil =>
+          cases SS <;> simp
+          case cons S SS =>
+            obtain ⟨s, S⟩ := S; obtain ⟨x, s⟩ := s
             simp only [Seq.join_cons, join_append, destruct_cons]
-            cases' s with x s <;> simp
-            · exact ⟨_, _, rfl, rfl⟩
-            · refine ⟨Seq.cons x (append s (Seq.join S)), SS, ?_, ?_⟩ <;> simp
-        · exact ⟨s, SS, rfl, rfl⟩
+            cases s <;> simp
+            case nil => exact ⟨_, _, rfl, rfl⟩
+            case cons x s => refine ⟨Seq.cons x (append s (Seq.join S)), SS, ?_, ?_⟩ <;> simp
+        case cons _ s => exact ⟨s, SS, rfl, rfl⟩
   · refine ⟨nil, SS, ?_, ?_⟩ <;> simp
 
 @[simp]
 theorem bind_assoc (s : Seq1 α) (f : α → Seq1 β) (g : β → Seq1 γ) :
     bind (bind s f) g = bind s fun x : α => bind (f x) g := by
-  cases' s with a s
+  obtain ⟨a, s⟩ := s
   -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): was `simp [bind, map]`.
   simp only [bind, map_pair, map_join]
   rw [← map_comp]
@@ -1371,9 +1385,9 @@ theorem bind_assoc (s : Seq1 α) (f : α → Seq1 β) (g : β → Seq1 γ) :
   -- Porting note: Instead of `apply recOn s <;> intros`, `induction'` are used to
   --   give names to variables.
   induction' s using recOn with x s_1 <;> induction' S using recOn with x_1 s_2 <;> simp
-  · cases' x_1 with x t
+  · obtain ⟨x, t⟩ := x_1
     cases t <;> simp
-  · cases' x_1 with y t; simp
+  · obtain ⟨y, t⟩ := x_1; simp
 
 instance monad : Monad Seq1 where
   map := @map

From a42d99ac446c7ea94870594fc914c39370ce8423 Mon Sep 17 00:00:00 2001
From: Vasilii Nesterov <vas.nesterov63@gmail.com>
Date: Mon, 10 Mar 2025 19:43:57 +0300
Subject: [PATCH 21/24] revert to make diff smaller

---
 Mathlib/Data/Seq/Seq.lean | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
index c898cde38bec0a..493fe494298193 100644
--- a/Mathlib/Data/Seq/Seq.lean
+++ b/Mathlib/Data/Seq/Seq.lean
@@ -558,7 +558,7 @@ alias ofList_get := ofList_get?
 
 @[simp]
 theorem ofList_cons (a : α) (l : List α) : ofList (a::l) = cons a (ofList l) := by
-  ext1 (_ | n) <;> rfl
+  ext1 (_ | n) <;> simp
 
 theorem ofList_injective : Function.Injective (ofList : List α → _) :=
   fun _ _ h => List.ext_getElem? fun _ => congr_fun (Subtype.ext_iff.1 h) _
@@ -766,7 +766,8 @@ theorem getElem?_take : ∀ (n k : ℕ) (s : Seq α),
         rw [destruct_eq_cons h]
         match n with
         | 0 => simp
-        | n+1 => simp [Nat.add_lt_add_iff_right, get?_cons_succ, getElem?_take]
+        | n+1 =>
+          simp [List.getElem?_cons_succ, Nat.add_lt_add_iff_right, getElem?_take]
 
 theorem get?_mem_take {s : Seq α} {m n : ℕ} (h_mn : m < n) {x : α}
     (h_get : s.get? m = .some x) : x ∈ s.take n := by
@@ -1108,7 +1109,7 @@ theorem take_drop {s : Seq α} {n m : ℕ} :
   induction m generalizing n s with
   | zero => simp [drop]
   | succ k ih =>
-    cases s
+    cases' s with x tl
     · simp
     cases n with
     | zero => simp
@@ -1155,7 +1156,7 @@ theorem zipWith_nil_right {f : α → β → γ} {s} :
 theorem zipWith_cons_cons {f : α → β → γ} {x s x' s'} :
     zipWith f (cons x s) (cons x' s') = cons (f x x') (zipWith f s s') := by
   ext1 n
-  cases n <;> simp
+  cases' n <;> simp
 
 @[simp]
 theorem zip_nil_left {s : Seq α} :

From 7d51750751bd30b19a0573661543a061398735c2 Mon Sep 17 00:00:00 2001
From: Vasilii Nesterov <vas.nesterov63@gmail.com>
Date: Fri, 14 Mar 2025 10:44:24 +0300
Subject: [PATCH 22/24] merge

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

diff --git a/Mathlib/Data/Seq/Seq.lean b/Mathlib/Data/Seq/Seq.lean
index 7e3e3f4511e9c6..36fc6c9a37d88f 100644
--- a/Mathlib/Data/Seq/Seq.lean
+++ b/Mathlib/Data/Seq/Seq.lean
@@ -967,7 +967,7 @@ theorem terminatedAt_map_iff {f : α → β} {s : Seq α} {n : ℕ} :
   simp [TerminatedAt]
 
 @[simp]
-theorem terminates_map_iff {f : α → β} {s : Seq α}  :
+theorem terminates_map_iff {f : α → β} {s : Seq α} :
     (map f s).Terminates ↔ s.Terminates := by
   simp [Terminates]
 
@@ -1311,10 +1311,7 @@ theorem join_map_ret (s : Seq α) : Seq.join (Seq.map ret s) = s := by
 
 @[simp]
 theorem bind_ret (f : α → β) : ∀ s, bind s (ret ∘ f) = map f s
-  | ⟨a, s⟩ => by
-    dsimp [bind, map]
-    rw [map_comp, ret]
-    simp
+  | ⟨a, s⟩ => by simp [bind, map, map_comp, ret]
 
 @[simp]
 theorem ret_bind (a : α) (f : α → Seq1 β) : bind (ret a) f = f a := by

From 7a2992fea0bd44d705da18c482af9f2a78a3efff Mon Sep 17 00:00:00 2001
From: Vasilii Nesterov <vas.nesterov63@gmail.com>
Date: Mon, 12 May 2025 15:01:24 +0300
Subject: [PATCH 23/24] fix

---
 Mathlib/Data/WSeq/Basic.lean    | 1 +
 Mathlib/Data/WSeq/Relation.lean | 4 +++-
 scripts/noshake.json            | 1 -
 3 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Data/WSeq/Basic.lean b/Mathlib/Data/WSeq/Basic.lean
index 0059a585f234dc..cccaf54062338b 100644
--- a/Mathlib/Data/WSeq/Basic.lean
+++ b/Mathlib/Data/WSeq/Basic.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Data.Seq.Seq
+import Mathlib.Util.CompileInductive
 
 /-!
 # Partially defined possibly infinite lists
diff --git a/Mathlib/Data/WSeq/Relation.lean b/Mathlib/Data/WSeq/Relation.lean
index ae29f5e1db252e..960c45de746e05 100644
--- a/Mathlib/Data/WSeq/Relation.lean
+++ b/Mathlib/Data/WSeq/Relation.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Mathlib.Data.WSeq.Basic
+import Mathlib.Logic.Relation
 
 /-!
 # Relations between and equivalence of weak sequences
@@ -112,7 +113,8 @@ theorem LiftRel.refl (R : α → α → Prop) (H : Reflexive R) : Reflexive (Lif
     apply H
 
 theorem LiftRel.symm (R : α → α → Prop) (H : Symmetric R) : Symmetric (LiftRel R) :=
-  fun s1 s2 (h : Function.swap (LiftRel R) s2 s1) => by rwa [LiftRel.swap, H.swap_eq] at h
+  fun s1 s2 (h : Function.swap (LiftRel R) s2 s1) => by
+    rwa [LiftRel.swap, H.swap_eq] at h
 
 theorem LiftRel.trans (R : α → α → Prop) (H : Transitive R) : Transitive (LiftRel R) :=
   fun s t u h1 h2 => by
diff --git a/scripts/noshake.json b/scripts/noshake.json
index 7f4e65f0a89a0a..703b44536d7c0d 100644
--- a/scripts/noshake.json
+++ b/scripts/noshake.json
@@ -412,7 +412,6 @@
   "Mathlib.Data.Vector.Basic": ["Mathlib.Control.Applicative"],
   "Mathlib.Data.Set.Image":
   ["Batteries.Tactic.Congr", "Mathlib.Data.Set.SymmDiff"],
-  "Mathlib.Data.Seq.WSeq": ["Mathlib.Data.Option.Basic"],
   "Mathlib.Data.Seq.Parallel": ["Mathlib.Init.Data.Prod"],
   "Mathlib.Data.PEquiv": ["Batteries.Tactic.Congr"],
   "Mathlib.Data.Ordmap.Ordnode": ["Mathlib.Data.Option.Basic"],

From f2334cb2b155a923a2b893b47d78b3866866ac74 Mon Sep 17 00:00:00 2001
From: Vasilii Nesterov <vas.nesterov63@gmail.com>
Date: Mon, 12 May 2025 15:02:11 +0300
Subject: [PATCH 24/24] revert

---
 Mathlib/Data/WSeq/Relation.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Data/WSeq/Relation.lean b/Mathlib/Data/WSeq/Relation.lean
index 960c45de746e05..b879f5fa6be683 100644
--- a/Mathlib/Data/WSeq/Relation.lean
+++ b/Mathlib/Data/WSeq/Relation.lean
@@ -113,8 +113,7 @@ theorem LiftRel.refl (R : α → α → Prop) (H : Reflexive R) : Reflexive (Lif
     apply H
 
 theorem LiftRel.symm (R : α → α → Prop) (H : Symmetric R) : Symmetric (LiftRel R) :=
-  fun s1 s2 (h : Function.swap (LiftRel R) s2 s1) => by
-    rwa [LiftRel.swap, H.swap_eq] at h
+  fun s1 s2 (h : Function.swap (LiftRel R) s2 s1) => by rwa [LiftRel.swap, H.swap_eq] at h
 
 theorem LiftRel.trans (R : α → α → Prop) (H : Transitive R) : Transitive (LiftRel R) :=
   fun s t u h1 h2 => by