refine ⟨a, b, by simp [P.union_eq.symm, hb], by simp [P.union_eq.symm, ha], fun hconn ↦ ?_⟩
case refine_1.intro.intro
α : 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
a : α
ha : a ∈ P.left
b : α
hb : b ∈ P.right
⊢ ∃ x, ∃ x_1 ∈ M.E, x ∈ M.E ∧ ¬M.ConnectedTo x x_1
case refine_1.intro.intro
α : 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
a : α
ha : a ∈ P.left
b : α
hb : b ∈ P.right
hconn : M.ConnectedTo a b
⊢ False