simp_rw [union_diff_right, hdj.1.sdiff_eq_left, hYI.sdiff_eq_left] at hu
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y✝ Z K C C₁ C₂ : Set α
h : M.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
Y : Set α
hYI : Disjoint Y I
hYi : M.Indep (Y ∪ I)
hYX : Y ⊆ X
hJY : J ⊆ Y
hu : (J ∪ I) \ I = (Y ∪ I) \ I
⊢ J = Y
α : Type u_1
M M' N : Matroid α
e f : α
I J R B X Y✝ Z K C C₁ C₂ : Set α
h : M.Basis (J ∪ I) (X ∪ I)
hdj : Disjoint J I ∧ Disjoint X I
hI : M.Indep I
Y : Set α
hYI : Disjoint Y I
hYi : M.Indep (Y ∪ I)
hYX : Y ⊆ X
hJY : J ⊆ Y
hu : J = Y
⊢ J = Y