feat(Data/Matroid/Constructions): Instances for basic matroids (#20886)

We add some instances for the matroids in `Data/Matroid/Constructions`, and also a `RkPos -> Nonempty` instance in `Matroid.Basic`.

Author: apnelson1

Mathlib/Data/Matroid/Basic.lean

@@ -263,6 +263,12 @@ instance finiteRk_of_finite (M : Matroid α) [M.Finite] : FiniteRk M :=
   /-- The empty set isn't a base -/
   empty_not_base : ¬M.Base ∅
 
+instance rkPos_nonempty {M : Matroid α} [M.RkPos] : M.Nonempty := by
+  obtain ⟨B, hB⟩ := M.exists_base
+  obtain rfl | ⟨e, heB⟩ := B.eq_empty_or_nonempty
+  · exact False.elim <| RkPos.empty_not_base hB
+  exact ⟨e, M.subset_ground B hB heB ⟩
+
 @[deprecated (since := "2025-01-20")] alias rkPos_iff_empty_not_base := rkPos_iff
 
 section exchange

Mathlib/Data/Matroid/Constructions.lean

@@ -128,6 +128,9 @@ theorem eq_loopyOn_or_rkPos (M : Matroid α) : M = loopyOn M.E ∨ RkPos M := by
 theorem not_rkPos_iff : ¬RkPos M ↔ M = loopyOn M.E := by
   rw [rkPos_iff, not_iff_comm, empty_base_iff]
 
+instance loopyOn_finiteRk : FiniteRk (loopyOn E) :=
+  ⟨∅, by simp⟩
+
 end LoopyOn
 
 section FreeOn
@@ -183,6 +186,13 @@ theorem restrict_eq_freeOn_iff : M ↾ I = freeOn I ↔ M.Indep I := by
 theorem Indep.restrict_eq_freeOn (hI : M.Indep I) : M ↾ I = freeOn I := by
   rwa [restrict_eq_freeOn_iff]
 
+instance freeOn_finitary : Finitary (freeOn E) := by
+  simp only [finitary_iff, freeOn_indep_iff]
+  exact fun I h e heI ↦ by simpa using h {e} (by simpa)
+
+lemma freeOn_rkPos (hE : E.Nonempty) : RkPos (freeOn E) := by
+  simp [rkPos_iff, hE.ne_empty.symm]
+
 end FreeOn
 
 section uniqueBaseOn
@@ -243,6 +253,20 @@ theorem uniqueBaseOn_restrict (h : I ⊆ E) (R : Set α) :
     (uniqueBaseOn I E) ↾ R = uniqueBaseOn (I ∩ R) R := by
   rw [uniqueBaseOn_restrict', inter_right_comm, inter_eq_self_of_subset_left h]
 
+lemma uniqueBaseOn_finiteRk (hI : I.Finite) : FiniteRk (uniqueBaseOn I E) := by
+  rw [← uniqueBaseOn_inter_ground_eq]
+  refine ⟨I ∩ E, ?_⟩
+  rw [uniqueBaseOn_base_iff inter_subset_right, and_iff_right rfl]
+  exact hI.subset inter_subset_left
+
+instance uniqueBaseOn_finitary : Finitary (uniqueBaseOn I E) := by
+  refine ⟨fun K hK ↦ ?_⟩
+  simp only [uniqueBaseOn_indep_iff'] at hK ⊢
+  exact fun e heK ↦ singleton_subset_iff.1 <| hK _ (by simpa) (by simp)
+
+lemma uniqueBaseOn_rkPos (hIE : I ⊆ E) (hI : I.Nonempty) : RkPos (uniqueBaseOn I E) where
+  empty_not_base := by simpa [uniqueBaseOn_base_iff hIE] using Ne.symm <| hI.ne_empty
+
 end uniqueBaseOn
 
 end Matroid