simp [P.union_eq.symm, hb]
α : 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
⊢ b ∈ M.E
no goals