change M✶.conn _ _ = M.conn _ _
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ P.dual.conn = P.conn
α : 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