rw [hI.indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl hI'.indep
    (by rw [hI.cl_eq_cl, hI'.cl_eq_cl]) hJ.indep,
  inter_comm, union_comm, hJ.indep.encard_inter_add_erk_dual_eq_of_cl_eq_cl hJ'.indep
    (by rw [hJ.cl_eq_cl, hJ'.cl_eq_cl]) hI'.indep, inter_comm, union_comm]
α : Type u_1
M : Matroid α
B B' I✝ I'✝ J✝ K X✝ Y✝ I I' J J' X Y : Set α
hI : M.Basis' I X
hI' : M.Basis' I' X
hJ : M.Basis' J Y
hJ' : M.Basis' J' Y
⊢ (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk = (I' ∩ J').encard + (M ↾ (I' ∪ J'))✶.erk
no goals