refactor(Mathlib/Data/Seq/Seq): make Sequence.mem_rec_on more useful

[Komyyy]

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

to

theorem mem_rec_on {a} {C : (s : Seq' α) → a ∈ s → Prop} {s} (M : a ∈ s)
    (mem_cons : ∀ s, C (cons a s) (mem_cons a s))
    (mem_cons_of_mem : ∀ (y) {s} (h : a ∈ s), C s h → C (cons y s) (mem_cons_of_mem y h)) :
    C s M

This change make Seq'.mem_rec_on available in induction tactic.

---

• depends on: chore(Mathlib/Data/Seq/Seq): add cases_eliminators to Sequence.recOn #13361

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

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• chore(Mathlib/Data/Seq/Seq): add cases_eliminators to Sequence.recOn #13361
  By Dependent Issues (🤖). Happy coding!

[github-actions]

Import summary

No significant changes to the import graph

[github-actions]

PR summary b7756f5b4c

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 α)
+ mem_think_of_mem
+ 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
-+-+ 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
--++ mem_rec_on
--++-+ 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