Theorem: Matroid.Basis'.conn_eq_of_disjoint (Matroid/Connectivity.lean)

State before:
α : Type u_1
M : Matroid α
B B' I I' J K X Y : Set α
hI : M.Basis' I X
hJ : M.Basis' J Y
hXY : Disjoint X Y
⊢ M.conn X Y = (M ↾ (I ∪ J))✶.erk
Tactic:
rw [hI.conn_eq hJ, (hXY.mono hI.subset hJ.subset).inter_eq, encard_empty, zero_add]
State after:
no goals