rw [← ab_cl_inter_eq]
α : 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
ab_cl_inter_eq : ⋂₀ {M.cl (insert b X), M.cl (insert a X)} = M.cl X
⊢ 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
ab_cl_inter_eq : ⋂₀ {M.cl (insert b X), M.cl (insert a X)} = M.cl X
⊢ ⋂₀ {M.cl (insert b X), M.cl (insert a X)} ∈ C