refine ⟨fun ⟨P, ⟨hc, hA, hB⟩⟩ ↦ ?_, fun ⟨x, y, hy, hx, h⟩ ↦ ?_⟩
α : 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
case refine_1
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
inst✝ : M.Nonempty
x✝ :
  ∃ P,
    (∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right) ∧ P.left.Nonempty ∧ P.right.Nonempty
P : M.Partition
hc : ∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right
hA : P.left.Nonempty
hB : P.right.Nonempty
⊢ ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1

case refine_2
α : Type u_1
M : Matroid α
k : ℕ
P : Set α → Prop
a b : α
inst✝ : M.Nonempty
x✝ : ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
x y : α
hy : y ∈ M.E
hx : x ∈ M.E
h : ¬M.ConnectedTo x y
⊢ ∃ P,
    (∀ (C : Set α), M.Circuit C → C ⊆ P.left ∪ P.right → C ⊆ P.left ∨ C ⊆ P.right) ∧ P.left.Nonempty ∧ P.right.Nonempty