refactor: move slim_check to plausible

[hargoniX]

This moves Mathlib to the now pulled out (and already slightly improved)
version of slim_check at https://github.com/leanprover-community/plausible/.
I removed both all instances and logic as well as all tests that are already
covered by plausible itself and only left what Mathlib needs for itself.

---

[github-actions]

PR summary 27e644c811

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Tactic.SlimCheck	442	0	-442 (-100.00%)
Mathlib.Testing.SlimCheck.Gen	361	0	-361 (-100.00%)
Mathlib.Testing.SlimCheck.Sampleable	440	0	-440 (-100.00%)
Mathlib.Testing.SlimCheck.Testable	441	0	-441 (-100.00%)
Mathlib.Tactic	2331	2322	-9 (-0.39%)

Import changes for all files

Files	Import difference
Mathlib.Testing.SlimCheck.Functions	-697
Mathlib.Tactic.SlimCheck	-442
Mathlib.Testing.SlimCheck.Testable	-441
Mathlib.Testing.SlimCheck.Sampleable	-440
Mathlib.Testing.SlimCheck.Gen	-361
Mathlib.Tactic	-9
Mathlib.Testing.Plausible.Testable	57
Mathlib.Testing.Plausible.Sampleable	413
Mathlib.Testing.Plausible.Functions	685

---

Declarations diff

- And.printableProp
- Bool.printableProp
- Bool.sampleableExt
- Bool.shrinkable
- Char.sampleable
- Char.sampleableDefault
- Char.shrinkable
- Configuration
- DecorationsOf
- Eq.printableProp
- False.printableProp
- Fin.sampleableExt
- Fin.shrinkable
- Gen
- Gen.run
- Iff.printableProp
- Imp.printableProp
- Int.sampleableExt
- Int.shrinkable
- LE.printableProp
- LT.printableProp
- List.sampleableExt
- List.shrinkable
- List.toFinmap'
- MyType
- NamedBinder
- Nat.sampleableExt
- Nat.shrink
- Nat.shrinkable
- Ne.printableProp
- NoShrink
- Not.printableProp
- Or.printableProp
- Pi.sampleableExt
- PrintableProp
- Prod.sampleableExt
- Prod.shrinkable
- Prop.sampleableExt
- SampleableExt
- Shrinkable
- Sigma.shrinkable
- TestResult
- Testable
- Testable.check
- Testable.checkIO
- Testable.runSuite
- Testable.runSuiteAux
- TotalFunction
- TotalFunction.inhabited
- True.printableProp
- addInfo
- addShrinks
- addVarInfo
- and
- andTestable
- apply
- arrayOf
- choose
- chooseAny
- chooseNatLt
- chooseNatLt_aux
- combine
- comp
- decGuardTestable
- elements
- foo
- forallTypesTestable
- formatFailure
- get
- getSize
- giveUp
- iff
- iffTestable
- imp
- inhabited
- instance (priority := 2000) PiPred.sampleableExt [SampleableExt (α → Bool)] :
- instance (priority := 2000) PiUncurry.sampleableExt [SampleableExt (α × β → γ)] :
- instance (priority := 2000) subtypeVarTestable {p : α → Prop} {β : α → Prop}
- instance (priority := high) unusedVarTestable {β : Prop} [Nonempty α] [Testable β] :
- instance (priority := low) : PrintableProp p
- instance (priority := low) decidableTestable {p : Prop} [PrintableProp p] [Decidable p] :
- instance (α : Type u) (β : Type v) [Repr α] [Repr β] : Repr (TotalFunction α β)
- instance : SampleableExt MyType
- instance : Shrinkable MyType
- instance : ToExpr Configuration
- instance : ToString (TestResult p) := ⟨toString⟩
- instance {α : Type u} {m : Type u → Type*} [Pure m] : Inhabited (OptionT m α)
- interpSample
- isFailure
- listOf
- minimize
- mk
- mkGenerator
- mkSelfContained
- oneOf
- or
- orTestable
- permutationOf
- printSamples
- prodOf
- propVarTestable
- reprAux
- resize
- retry
- runProp
- sampleableExt
- shrink
- shrinkable
- slimTrace
- testBit_pred
- toString
- varTestable
- verbose
-- repr

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.

[eric-wieser]

I think we should keep the slim_check tactic around in mathlib as a deprecated alias for plausible, so as to automatically correct the muscle memory of anyone using the old name.