simp only [Connected, show M.Nonempty by assumption, true_and, not_forall, Classical.not_imp,
  exists_and_left, exists_prop, exists_and_left, Partition.IsTutteSep, Nat.cast_one,
  ENat.lt_one_iff, one_le_encard_iff_nonempty]
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
⊢ (∃ P, P.IsTutteSep 1) ↔ ¬M.Connected
α : 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