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

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