simp only [Partition.conn_eq_zero_iff, and_self,
  skew_iff_forall_circuit (Partition.disjoint _) (Partition.left_subset_ground _)
    (Partition.right_subset_ground _)]
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
⊢ (∃ P, P.conn = 0 ∧ P.left.Nonempty ∧ P.right.Nonempty) ↔ ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
⊢ (∃ P,
      (∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right) ∧
        P.left.Nonempty ∧ P.right.Nonempty) ↔
    ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1