[Merged by Bors] - feat(Data/Seq): structural lemmas

[vasnesterov]

• Add several theorems about Stream'.Seq, mainly on sequence operations with nil and cons.
• Introduce the fold operation for sequences and prove a few structural lemmas about it.
• Rename Seq.destruct_eq_nil as Seq.destruct_eq_none.

---

• depends on: [Merged by Bors] - refactor(Data/Seq): mark Seq.recOn with cases_eliminator #19829

This PR is necessary for a new tactic (#18486), which computes the asymptotics of real functions.

[github-actions]

PR summary 90e86dca78

Import changes exceeding 2%

%	File
+18.15%	Mathlib.Data.Seq.Parallel
+18.77%	Mathlib.Data.Seq.Seq

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Data.Seq.Seq	277	329	+52 (+18.77%)
Mathlib.Data.Seq.Parallel	281	332	+51 (+18.15%)

Import changes for all files

Files	Import difference
7 files Mathlib.Algebra.ContinuedFractions.Computation.Approximations Mathlib.Algebra.ContinuedFractions.Computation.Basic Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat Mathlib.Algebra.ContinuedFractions.Computation.Translations Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv Mathlib.Algebra.ContinuedFractions.Determinant	1
6 files Mathlib.Algebra.ContinuedFractions.Basic Mathlib.Algebra.ContinuedFractions.ContinuantsRecurrence Mathlib.Algebra.ContinuedFractions.TerminatedStable Mathlib.Algebra.ContinuedFractions.Translations Mathlib.Data.Seq.Parallel Mathlib.Data.Seq.WSeq	51
Mathlib.Data.Seq.Seq	52

---

Declarations diff

+ cons_eq_cons
+ cons_ne_nil
+ cons_not_terminatedAt_zero
+ cons_terminatedAt_succ_iff
+ corec_cons
+ corec_nil
+ destruct_eq_none
+ drop_get?
+ drop_nil
+ drop_succ_cons
+ fold
+ fold_cons
+ fold_head
+ fold_nil
+ get?_mem
+ get?_mem_take
+ head_eq_none
+ head_eq_none_iff
+ head_eq_some
+ length_take_le
+ nil_ne_cons
+ take_drop
+ take_nil
+ take_succ_cons
+ take_zero
+ terminates_cons_iff
+ val_eq_get
+ zipWith_cons_cons
+ zipWith_map
+ zipWith_map_left
+ zipWith_map_right
+ zipWith_nil_left
+ zipWith_nil_right
+ zip_cons_cons
+ zip_map
+ zip_map_left
+ zip_map_right
+ zip_nil_left
+ zip_nil_right
- destruct_eq_nil

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).

[vihdzp]

What's the reasoning here?

[vasnesterov]

When drop is marked with [simp], the simplifier unfolds (cons x s).drop (n + 1) as ((cons x s).drop n).tail instead of s.drop n, even when the drop_succ_cons simp-lemma is present. In general, I think that replacing s.drop (n + 1) with (s.drop n).tail is not what the user wants by default because it adds another sequence operation to the expression, which rarely is simplification.

With drop_nil and drop_succ_cons instead, the simplifier always simplifies the expression.

[vasnesterov]

In #20071 I reorganized this file, so some proofs from this PR are changed. It also removes "large-import".

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - refactor(Data/Seq): mark Seq.recOn with cases_eliminator #19829
  By Dependent Issues (🤖). Happy coding!

[digama0]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style