feat: (Data.Matroid) basic matroid theory (#6352)

This PR is the first in a series that are intended to add matroid theory to mathlib. The file `Data.Matroid.Basic` contains the definition of (possibly infinite) matroids, API relating bases, independent/dependent sets and bases of sets, and some simple typeclasses related to finiteness/nonemptiness of matroids. We also define a tactic whose job is to prove that a set is contained in the ground set of a matroid (using aesop); it is imperfect, but does an ok job. 
 
Alternative axiomatizations, duality, minors, rank, circuits, closure, flats, etc etc are all ready to go, and will be added in a sequence of future PRs. 



Co-authored-by: Kyle Miller <kmill31415@gmail.com>

Author: apnelson1

Mathlib.lean

@@ -1611,6 +1611,8 @@ import Mathlib.Data.Matrix.Notation
 import Mathlib.Data.Matrix.PEquiv
 import Mathlib.Data.Matrix.Rank
 import Mathlib.Data.Matrix.Reflection
+import Mathlib.Data.Matroid.Basic
+import Mathlib.Data.Matroid.Init
 import Mathlib.Data.Multiset.Antidiagonal
 import Mathlib.Data.Multiset.Basic
 import Mathlib.Data.Multiset.Bind