exact fun hdj _↦ ⟨fun h I hId hIC ↦ h hId (disjoint_of_subset_left hIC hdj) hIC,
  fun h I hI _ hIC ↦ h hI hIC⟩
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R C : Set α
⊢ Disjoint C D →
    M.Dep C → ((∀ ⦃I : Set α⦄, M.Dep I → Disjoint I D → I ⊆ C → I = C) ↔ ∀ ⦃I : Set α⦄, M.Dep I → I ⊆ C → I = C)
no goals