Theorem: Matroid.Basis'.conn_eq (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
⊢ M.conn X Y = (I ∩ J).encard + (M ↾ (I ∪ J))✶.erk
Tactic:
simp_rw [conn, hI.encard_dual_switch_switch_eq (M.exists_basis' X).choose_spec hJ
  (M.exists_basis' Y).choose_spec]
State after:
no goals