Commit 2024-05-12 02:17 ad584cd8

feat(Data/Matroid/*): add Indep as a structure field to Matroid. (#12665) This PR slightly shuffles the design of Matroid to improve defeq. Specifically, we add Indep as a structure field of Matroid together with a rule that Indep relates correctly to Base, where previously Matroid.Indep was defined after the fact. This has the consequence that, when a matroid M is built using a user-supplied independence predicate Indep (via IndepMatroid.matroid) , the terms M.Indep and Indep are defeq, where previously this needed to be proved by simp. This turns a few proofs already appearing in mathlib into Iff.rfl, and this same benefit will apply to many future API additions, since the independence predicate is the most common way to construct a matroid in practice. The tradeoff is that independence is no longer definitionally the same as being a subset of a base, but this seems to be worth it; it is simply a matter of using Indep.exists_base_superset where needed. The fact that now Matroid.mk is a bit 'heavier' than before is almost irrelevant, since matroids are essentially always going to be defined in terms of one of the alternative constructors, which are unchanged.