[Merged by Bors] - refactor(Data/Seq): reorganize Seq.lean

[vasnesterov]

The Seq API in the Seq.lean file was somewhat disorganized. This PR reorganizes the file to make it more structured.

It arranges the API in the following way:

1. Definitions and the get? function.
2. Constructors: nil and cons.
3. Destructors: head, tail, and destruct.
4. Recursion and corecursion principles.
5. Bisimulation.
6. Terminates API.
7. Membership for sequences.
8. Conversion to and from other types (List, Stream, MLList) and take operation as it is required for conversion to List.
9. Definitions of other operations on sequences (append, map, join, etc.).
10. Lemmas about conversions and operations, organized into sections by the primary operation of each lemma.

---

I tried not to change any proofs here, but had to rewrite some of them due to dependencies and to avoid importing apply_fun. The proofs of the following lemmas were changed:

• head_eq_some
• head_eq_none
• cons_ne_nil
• cons_eq_cons
• ofList

I found it useful to run git diff --color-moved to verify that the actual difference is just these proofs and adding sections.

• depends on: [Merged by Bors] - feat(Data/Seq): structural lemmas #19859

[github-actions]

PR summary f2334cb2b1

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.Seq.Seq	331	258	-73 (-22.05%)
Mathlib.Data.WSeq.Basic	332	263	-69 (-20.78%)
Mathlib.Data.WSeq.Relation	333	265	-68 (-20.42%)

Import changes for all files

Files	Import difference
Mathlib.Data.Seq.Seq	-73
Mathlib.Algebra.ContinuedFractions.Basic	-72
5 files Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence Mathlib.Algebra.ContinuedFractions.TerminatedStable Mathlib.Algebra.ContinuedFractions.Translations Mathlib.Data.WSeq.Basic Mathlib.Data.WSeq.Defs	-69
4 files Mathlib.Data.Seq.Parallel Mathlib.Data.Seq.WSeq Mathlib.Data.WSeq.Productive Mathlib.Data.WSeq.Relation	-68
Mathlib.Algebra.ContinuedFractions.Determinant	-8
Mathlib.Algebra.ContinuedFractions.Computation.Basic Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv	-7
Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating Mathlib.Algebra.ContinuedFractions.Computation.Translations	-6
Mathlib.Algebra.ContinuedFractions.Computation.Approximations Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat	-1

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(Data/Seq): structural lemmas #19859
  By Dependent Issues (🤖). Happy coding!

[j-loreaux]

Thanks for this tip: git diff --color-moved, it was helpful in reviewing!

[j-loreaux]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by j-loreaux.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Build failed:

• Build

[vasnesterov]

@jcommelin Should it be merged again?

[j-loreaux]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build