refactor(Mathlib/Data/Seq/Seq): make `Seq'.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: #13361

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

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• leanprover-community/mathlib4#13361 By Dependent Issues (🤖). Happy coding!

[github-actions[bot]]

Import summary

No significant changes to the import graph

[github-actions[bot]]

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