refine' fun K hK ↦ ⟨K ∩ M.E, _, inter_subset_left⟩
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B : Set α
⊢ ∀ x ∈ {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty},
    ∃ y ∈ {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E}, y ⊆ x
α : Type u_1
M : Matroid α
C C' I X C₁ C₂ R : Set α
e f x y : α
B K : Set α
hK : K ∈ {X | ∀ (B : Set α), M.Base B → (X ∩ B).Nonempty}
⊢ K ∩ M.E ∈ {X | (X ⊆ M.E → ∀ (x : Set α), M.Base x → x ⊆ M.E → (x ∩ X).Nonempty) ∧ X ⊆ M.E}