mathlib3 SHA: 08aeb33b5b693fb1392a7568ae2c0b253516535e

porting notes:
1. The notation `$<` has been removed entirely. It is the same operation as `|>` in Lean 4 except with lower priority and a quick grep revealed it occurred literally nowhere in mathlib3.
2. The dubious translation errors were due to order of implicit arguments and have been `#alignₓ`ed (except `Sum.bind` I'm not sure what the issue was, see [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/why.20dubious.3F))
3. The `fish` definition is no longer needed because `>=>` has the correct (i.e., same as mathlib3's `fish`) binding precedence (`55`) in core Lean 4.
4. It should be noted that `>=>` was left-associative in Lean 3, but it is now right-associative in Lean 4. There is a comment to this effect near `fish_assoc`.

Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

* master:
  feat: port Data.Countable.Defs (#736)
  chore: bump to nightly-2022-11-26 (#747)
  feat(Algebra/Ring/Units): port file (#746)
  style(Algebra/Order/Monoid/Lemmas): Update to current naming convention (#743)
  feat: stubs in ad-hoc ported files for linarith algebra requirements (#733)
  feat: port algebra.group.semiconj (#717)
  chore: make argument to mul_inv_cancel implicit (#737)
  feat(Algebra/Ring/InjSurj): port file (#734)
  chore: bump to nightly-2022-11-25 (#731)
  feat: port order.minmax (#728)
  chore: make the 'p' argument to Nat.find implicit (#730)
  feat: port Control.Basic (#588)
  feat: port data.finite.defs (#698)
  feat: port:  Data.DList.Basic (#616)
  chore: reduce imports in Algebra.Group.Defs (#727)
  chore(Algebra/Order/Hom/Basic): remove outParam (#692)

mathlib3 SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7

- [x] depends on: #588

Notes: 
1. There is a discrepancy between the Lean 3 and Lean 4 types of `has_seq.seq` and `Seq.seq`. I added an `ₓ` for alignment.
2. There were one or two places where the existing `simp` or `rw` calls didn't succeed, but I'm not entirely sure why.
3. In `Functor.Comp.functor_comp_id` and `Functor.Comp.functor_id_comp` I had to use `Id` instead of `id`, because only the former has the `Monad` instance.
4. I had to change the imports, but I think what is there now is minimal.

Co-authored-by: ADedecker <anatolededecker@gmail.com>

mathlib3 SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7

- [x] depends on: #588

Notes: 
1. There is a discrepancy between the Lean 3 and Lean 4 types of `has_seq.seq` and `Seq.seq`. I added an `ₓ` for alignment.
2. There were one or two places where the existing `simp` or `rw` calls didn't succeed, but I'm not entirely sure why.
3. In `Functor.Comp.functor_comp_id` and `Functor.Comp.functor_id_comp` I had to use `Id` instead of `id`, because only the former has the `Monad` instance.
4. I had to change the imports, but I think what is there now is minimal.

Co-authored-by: ADedecker <anatolededecker@gmail.com>

mathlib3 SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7

- [x] depends on: #588

Notes: 
1. There is a discrepancy between the Lean 3 and Lean 4 types of `has_seq.seq` and `Seq.seq`. I added an `ₓ` for alignment.
2. There were one or two places where the existing `simp` or `rw` calls didn't succeed, but I'm not entirely sure why.
3. In `Functor.Comp.functor_comp_id` and `Functor.Comp.functor_id_comp` I had to use `Id` instead of `id`, because only the former has the `Monad` instance.
4. I had to change the imports, but I think what is there now is minimal.

Co-authored-by: ADedecker <anatolededecker@gmail.com>

mathlib3 SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7

- [x] depends on: #588

Notes: 
1. There is a discrepancy between the Lean 3 and Lean 4 types of `has_seq.seq` and `Seq.seq`. I added an `ₓ` for alignment.
2. There were one or two places where the existing `simp` or `rw` calls didn't succeed, but I'm not entirely sure why.
3. In `Functor.Comp.functor_comp_id` and `Functor.Comp.functor_id_comp` I had to use `Id` instead of `id`, because only the former has the `Monad` instance.
4. I had to change the imports, but I think what is there now is minimal.

Co-authored-by: ADedecker <anatolededecker@gmail.com>

mathlib3 SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7

- [x] depends on: #588

Notes: 
1. There is a discrepancy between the Lean 3 and Lean 4 types of `has_seq.seq` and `Seq.seq`. I added an `ₓ` for alignment.
2. There were one or two places where the existing `simp` or `rw` calls didn't succeed, but I'm not entirely sure why.
3. In `Functor.Comp.functor_comp_id` and `Functor.Comp.functor_id_comp` I had to use `Id` instead of `id`, because only the former has the `Monad` instance.
4. I had to change the imports, but I think what is there now is minimal.

Co-authored-by: ADedecker <anatolededecker@gmail.com>

mathlib3 SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7

- [x] depends on: #588

Notes: 
1. There is a discrepancy between the Lean 3 and Lean 4 types of `has_seq.seq` and `Seq.seq`. I added an `ₓ` for alignment.
2. There were one or two places where the existing `simp` or `rw` calls didn't succeed, but I'm not entirely sure why.
3. In `Functor.Comp.functor_comp_id` and `Functor.Comp.functor_id_comp` I had to use `Id` instead of `id`, because only the former has the `Monad` instance.
4. I had to change the imports, but I think what is there now is minimal.

Co-authored-by: ADedecker <anatolededecker@gmail.com>

mathlib3 SHA: 71ca477041bcd6d7c745fe555dc49735c12944b7

- [x] depends on: #588

Notes: 
1. There is a discrepancy between the Lean 3 and Lean 4 types of `has_seq.seq` and `Seq.seq`. I added an `ₓ` for alignment.
2. There were one or two places where the existing `simp` or `rw` calls didn't succeed, but I'm not entirely sure why.
3. In `Functor.Comp.functor_comp_id` and `Functor.Comp.functor_id_comp` I had to use `Id` instead of `id`, because only the former has the `Monad` instance.
4. I had to change the imports, but I think what is there now is minimal.

Co-authored-by: ADedecker <anatolededecker@gmail.com>