obtain (hCA | hCB) := hc C hC (hC.subset_ground.trans_eq P.union_eq.symm)
case refine_1.intro.intro.intro.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
C : Set α
hC : M.Circuit C
haC : a ∈ C
hbC : b ∈ C
⊢ False
case refine_1.intro.intro.intro.intro.intro.inl
α : 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
C : Set α
hC : M.Circuit C
haC : a ∈ C
hbC : b ∈ C
hCA : C ⊆ P.left
⊢ False

case refine_1.intro.intro.intro.intro.intro.inr
α : 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
C : Set α
hC : M.Circuit C
haC : a ∈ C
hbC : b ∈ C
hCB : C ⊆ P.right
⊢ False