refine .inr <| U.covBy_of_maximal_cl (M.cl_subset_cl hss) hcl hI.2 fun x ⟨hx, hxcl⟩ ↦ ?_
case refine_1.inl.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∈ I
hcl : M.cl (X \ {e}) ∈ U
⊢ M.cl (I \ {e}) = M.cl (X \ {e}) ∧ e ∉ X ∨ (M.cl (I \ {e}) ⋖[M] M.cl (X \ {e}))
case refine_1.inl.inl
α : Type u_1
M : Matroid α
I J B F₀ F F' X Y : Set α
e f : α
U : M.ModularCut
hX : X ⊆ insert e M.E
hI : M.Indep (I \ {e}) ∧ M.cl (I \ {e}) ∉ U
hIX : I ⊆ X
hss : I \ {e} ⊆ X \ {e}
hX' : X \ {e} ⊆ M.E
h :
  ∀ x ∉ I,
    x ∈ X →
      (M.Indep (insert x I) → e ∈ insert x I) ∧
        (M.Indep (insert x I \ {e}) → e ∈ insert x I → M.cl (insert x I \ {e}) ∈ U)
heI : e ∈ I
hcl : M.cl (X \ {e}) ∈ U
x : α
x✝ : x ∈ (X \ {e}) \ M.cl (I \ {e})
hx : x ∈ X \ {e}
hxcl : x ∉ M.cl (I \ {e})
⊢ M.cl (insert x (I \ {e})) ∈ U