feat: more simp lemmas about streams (#3929)

This marks many existing lemmas for `Stream'` as simp, and adds a few new ones.  Notably, I've removed the simp attribute from `take_succ` because that lemma can result in huge goal states (since it duplicates the stream).

Mathlib/Data/Seq/Computation.lean

@@ -178,7 +178,7 @@ theorem tail_pure (a : α) : tail (pure a) = pure a :=
 
 @[simp]
 theorem tail_think (s : Computation α) : tail (think s) = s := by
-  cases' s with f al ; apply Subtype.eq ; dsimp [tail, think] ; rw [Stream'.tail_cons]
+  cases' s with f al ; apply Subtype.eq ; dsimp [tail, think]
 #align computation.tail_think Computation.tail_think
 
 @[simp]
@@ -719,7 +719,6 @@ theorem map_id : ∀ s : Computation α, map id s = s
 theorem map_comp (f : α → β) (g : β → γ) : ∀ s : Computation α, map (g ∘ f) s = map g (map f s)
   | ⟨s, al⟩ => by
     apply Subtype.eq ; dsimp [map]
-    rw [Stream'.map_map]
     apply congr_arg fun f : _ → Option γ => Stream'.map f s
     ext ⟨⟩ <;> rfl
 #align computation.map_comp Computation.map_comp

Mathlib/Data/Seq/Seq.lean

@@ -244,7 +244,7 @@ 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]; rw [Stream'.tail_cons]
+    apply Subtype.eq; dsimp [tail]
 #align stream.seq.destruct_cons Stream'.Seq.destruct_cons
 
 -- porting note: needed universe annotation to avoid universe issues
@@ -272,7 +272,6 @@ theorem tail_cons (a : α) (s) : tail (cons a s) = s := by
   cases' s with f al
   apply Subtype.eq
   dsimp [tail, cons]
-  rw [Stream'.tail_cons]
 #align stream.seq.tail_cons Stream'.Seq.tail_cons
 
 @[simp]
@@ -710,13 +709,12 @@ theorem map_id : ∀ s : Seq α, map id s = s
 
 @[simp]
 theorem map_tail (f : α → β) : ∀ s, map f (tail s) = tail (map f s)
-  | ⟨s, al⟩ => by apply Subtype.eq ; dsimp [tail, map] ; rw [Stream'.map_tail]
+  | ⟨s, al⟩ => by apply Subtype.eq ; dsimp [tail, map]
 #align stream.seq.map_tail Stream'.Seq.map_tail
 
 theorem map_comp (f : α → β) (g : β → γ) : ∀ s : Seq α, map (g ∘ f) s = map g (map f s)
   | ⟨s, al⟩ => by
     apply Subtype.eq ; dsimp [map]
-    rw [Stream'.map_map]
     apply congr_arg fun f : _ → Option γ => Stream'.map f s
     ext ⟨⟩ <;> rfl
 #align stream.seq.map_comp Stream'.Seq.map_comp

Mathlib/Data/Stream/Defs.lean

@@ -10,26 +10,21 @@ Authors: Leonardo de Moura
 -/
 import Mathlib.Mathport.Rename
 import Mathlib.Init.Data.Nat.Notation
+
 /-!
 # Definition of `Stream'` and functions on streams
 
 A stream `Stream' α` is an infinite sequence of elements of `α`. One can also think about it as an
 infinite list. In this file we define `Stream'` and some functions that take and/or return streams.
 Note that we already have `Stream` to represent a similar object, hence the awkward naming.
-
 -/
 
-universe u v w
 /-- A stream `Stream' α` is an infinite sequence of elements of `α`. -/
 def Stream' (α : Type u) := ℕ → α
 #align stream Stream'
 
-open Nat
-
 namespace Stream'
 
-variable {α : Type u} {β : Type v} {δ : Type w}
-
 /-- Prepend an element to a stream. -/
 def cons (a : α) (s : Stream' α) : Stream' α
   | 0 => a
@@ -38,22 +33,22 @@ def cons (a : α) (s : Stream' α) : Stream' α
 
 scoped infixr:67 " :: " => cons
 
+/-- `n`-th element of a stream. -/
+def nth (s : Stream' α) (n : ℕ) : α := s n
+#align stream.nth Stream'.nth
+
 /-- Head of a stream: `Stream'.head s = Stream'.nth s 0`. -/
-def head (s : Stream' α) : α := s 0
+abbrev head (s : Stream' α) : α := s.nth 0
 #align stream.head Stream'.head
 
 /-- Tail of a stream: `Stream'.tail (h :: t) = t`. -/
-def tail (s : Stream' α) : Stream' α := fun i => s (i + 1)
+def tail (s : Stream' α) : Stream' α := fun i => s.nth (i + 1)
 #align stream.tail Stream'.tail
 
 /-- Drop first `n` elements of a stream. -/
-def drop (n : Nat) (s : Stream' α) : Stream' α := fun i => s (i + n)
+def drop (n : Nat) (s : Stream' α) : Stream' α := fun i => s.nth (i + n)
 #align stream.drop Stream'.drop
 
-/-- `n`-th element of a stream. -/
-def nth (s : Stream' α) (n : ℕ) : α := s n
-#align stream.nth Stream'.nth
-
 /-- Proposition saying that all elements of a stream satisfy a predicate. -/
 def All (p : α → Prop) (s : Stream' α) := ∀ n, p (nth s n)
 #align stream.all Stream'.All
@@ -111,7 +106,7 @@ def corecState {σ α} (cmd : StateM σ α) (s : σ) : Stream' α :=
 #align stream.corec_state Stream'.corecState
 
 -- corec is also known as unfold
-def unfolds (g : α → β) (f : α → α) (a : α) : Stream' β :=
+abbrev unfolds (g : α → β) (f : α → α) (a : α) : Stream' β :=
   corec g f a
 #align stream.unfolds Stream'.unfolds