Theorem: Matroid.ModularCut.cl_mem_of_mem (Matroid/Extension.lean)

State before:
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hF : F ∈ U
⊢ M.cl F ∈ U
Tactic:
rwa [(U.flat_of_mem hF).cl]
State after:
no goals