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

State before:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ P.left ⊆ M.E
Tactic:
rw [← P.union_eq]
State after:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ P.left ⊆ P.left ∪ P.right

State before:
α : Type u_1
M : Matroid α
k : ℕ
P✝ : Set α → Prop
a b : α
P : M.Partition
⊢ P.left ⊆ P.left ∪ P.right
Tactic:
apply subset_union_left
State after:
no goals