feat(Mathlib/Data/Seq/Seq): prove `∀ a ∈ (s : Seq' α), p a` using coinduction

[Komyyy]

---

• [ ] depends on: #13509

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#13509 By Dependent Issues (🤖). Happy coding!

[github-actions[bot]]

Import summary

No significant changes to the import graph

[github-actions[bot]]

PR summary 86acf3119c

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 + all_coind + all_cons + all_nil + 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