chore(Mathlib/Data/Seq/Seq): add cases_eliminators to Sequence.recOn

[Komyyy]

Add @[elab_as_elim, induction_eliminator, cases_eliminator] to Seq'.recOn.
This can make the proofs more brief.

---

• depends on: style(Mathlib/Data/Seq/Seq): rename Stream'.Seq to Sequence #13241

This PR consists Continued fractions makes an isomorphism between irrationals and baire space
project

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• style(Mathlib/Data/Seq/Seq): rename Stream'.Seq to Sequence #13241
  By Dependent Issues (🤖). Happy coding!

[github-actions]

Import summary

No significant changes to the import graph

[github-actions]

PR summary 9c0dc73c82

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Data.Seq.Parallel	-284
Mathlib.Data.Seq.WSeq	-283
Mathlib.Data.Seq.Seq	-279
Mathlib.Data.Seq.Computation	-276
Mathlib.Data.Sequence.Computation	276
Mathlib.Data.Sequence.Sequence	279
Mathlib.Data.Sequence.WSequence	283
Mathlib.Data.Sequence.Parallel	284

---

Declarations diff

+ IntFractPair.get?_sequence1_eq_succ_get?_stream
+ IntFractPair.sequence1_fst_eq_of
+ Sequence
+ Sequence1
+ Stream'.IsSequence
+ WSequence
+ instance : Functor Sequence where map := @map
+ instance : Inhabited (Sequence α)
+ instance : LawfulFunctor Sequence
+ instance : Membership α (Sequence α)
+ instance [Inhabited α] : Inhabited (Sequence1 α)
+ of_h_eq_intFractPair_sequence1_fst_b
+ of_terminatedAt_iff_intFractPair_sequence1_terminatedAt
+ sequence1
+ stream_isSequence
- IntFractPair.get?_seq1_eq_succ_get?_stream
- IntFractPair.seq1_fst_eq_of
- IsSeq
- Seq
- Seq1
- WSeq
- instance : Functor Seq where map := @map
- instance : Inhabited (Seq α)
- instance : LawfulFunctor Seq
- instance : Membership α (Seq α)
- instance [Inhabited α] : Inhabited (Seq1 α)
- of_h_eq_intFractPair_seq1_fst_b
- of_terminatedAt_iff_intFractPair_seq1_terminatedAt
- seq1
- stream_isSeq
-+-+ BisimO
-+-+ Mem
-+-+ append
-+-+ append_assoc
-+-+ append_nil
-+-+ bind
-+-+ bind_assoc
-+-+ coeList
-+-+ coeStream
-+-+ cons
-+-+ destruct
-+-+ destruct_nil
-+-+ drop
-+-+ dropn_add
-+-+ dropn_tail
-+-+ exists_of_mem_map
-+-+ get?
-+-+ get?_tail
-+-+ head
-+-+ head_nil
-+-+ join_append
-+-+ join_join
-+-+ join_map_ret
-+-+ lawfulMonad
-+-+ map_comp
-+-+ mem_append_left
-+-+ mem_cons
-+-+ mem_cons_iff
-+-+ mem_cons_of_mem
-+-+ mem_map
-+-+ mem_rec_on
-+-+ monad
-+-+ nil
-+-+ nil_append
-+-+ ofList
-+-+ ofList_nil
-+-+ ofStream
-+-+ of_mem_append
-+-+ recOn
-+-+ ret
-+-+ ret_bind
-+-+ splitAt
-+-+ tail
-+-+ tail_nil
-+-+ take
-+-+ toList
-+-+ toSeq
-+-+ zip
-+-+ zipWith
-+-+-+ join_nil
-+--++ join
-+--++ map_id
--++ coeSeq
--++-+ map

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[Komyyy]

❗This project is temporarily frozen, PRs are all closed for a moment(I keep the branch as it may be revived someday). Detail