rw [hcv.eq_cl_insert_of_mem_diff ⟨M.mem_cl_of_mem ⟨hi, hxe⟩, hind.1.2⟩,
  cl_insert_cl_eq_cl_insert] at h
case pos.inr.intro
α : 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
x : α
hxI : x ∉ I
hi : x ∈ X
hind : x ∈ M.E \ M.cl (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
hcv : M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})
h : M.cl (X \ {e}) ∈ U
⊢ False
case pos.inr.intro
α : 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
x : α
hxI : x ∉ I
hi : x ∈ X
hind : x ∈ M.E \ M.cl (I \ {e}) ∧ M.cl (insert x (I \ {e})) ∉ U
heI : e ∈ I
hxe : x ≠ e
hcv : M.cl (I \ {e}) ⋖[M] M.cl (X \ {e})
h : M.cl (insert x (I \ {e})) ∈ U
⊢ False