rw [← union_insert_eq] at h_ind
α : Type u_1
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
a b : α
X : Set α
hne : a ≠ b
h_ind : M.Indep (insert a (insert b X))
h_a : M.cl (insert a X) ∈ C
h_b : M.cl (insert b X) ∈ C
⊢ M.cl X ∈ C
α : Type u_1
M : Matroid α
C : Set (Set α)
hC : M.Modular_cut C
a b : α
X : Set α
hne : a ≠ b
h_ind : M.Indep (insert b X ∪ insert a X)
h_a : M.cl (insert a X) ∈ C
h_b : M.cl (insert b X) ∈ C
⊢ M.cl X ∈ C