refine fun B hB ↦ ⟨Indep.basis_of_subset_of_subset_cl ?_ ?_ ?_, ?_⟩
α : Type u_1
M : Matroid α
B B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
⊢ ∀ ⦃B : Set α⦄, M.Basis B (M.cl I) → (M ／ (K \ I)).Basis B (B ∪ J \ (K \ I)) ∧ K \ I ⊆ B ∪ J
case refine_1
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ (M ／ (K \ I)).Indep B

case refine_2
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ B ⊆ B ∪ J \ (K \ I)

case refine_3
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ B ∪ J \ (K \ I) ⊆ (M ／ (K \ I)).cl B

case refine_4
α : Type u_1
M : Matroid α
B✝ B' I I' J K✝ X Y : Set α
hI : M.Indep I
hI' : M.Indep I'
hII' : M.cl I = M.cl I'
hJ : M.Indep J
K : Set α
hK : M.Basis K (I ∪ J)
hIK : I ⊆ K
hsk : M.Skew (M.cl I) (K \ I)
hdj : Disjoint (M.cl I) (K \ I)
B : Set α
hB : M.Basis B (M.cl I)
⊢ K \ I ⊆ B ∪ J