have' hdj := hsk.disjoint_of_indep_subset_right (hK.indep.diff _) Subset.rfl
case intro.intro
α : 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)
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk
case intro.intro
α : 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)
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J).encard + (M ↾ (I' ∪ J))✶.erk