Theorem: Matroid.Partition.compl_left (Matroid/Connectivity.lean)

State before:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ M.E \ P.left = P.right
Tactic:
simp [← P.union_eq, P.disjoint.symm]
State after:
no goals