rw [insert_comm]
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ insert a X ⊆ insert a (insert b X)
α : Type u_1
M : Matroid α
I B : Set α
Ys Xs : Set (Set α)
a b : α
X : Set α
C : M.ModularCut
hI : M.Indep (insert a (insert b X))
ha : M.cl (insert a X) ∈ C
hb : M.cl (insert b X) ∈ C
hne : a ≠ b
⊢ insert a X ⊆ insert b (insert a X)