rw [← P.compl_left, conn_compl_dual, P.compl_left]
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ M✶.conn P.dual.left P.dual.right = M.conn P.left P.right
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ M✶.conn P.dual.left P.dual.right = M✶.conn P.left P.right