rw [← cl_insert_cl_eq_cl_insert, ← hI.cl_eq_cl, cl_insert_cl_eq_cl_insert] at hmax
case intro.intro.intro.inr.inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
y : α
hy : y ∈ J \ I
hyx : y ≠ x
hyE : y ∈ M.E
hyX : y ∉ M.cl X
hyY : y ∈ Y
hmax : M.cl (insert y X) ∈ U
⊢ M.cl (J \ {x}) ∈ U
case intro.intro.intro.inr.inr.intro.intro
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X✝ Y✝ : Set α
e f : α
U✝ U : M.ModularCut
X Y : Set α
hXY : M.cl X ⊆ M.cl Y
I : Set α
hXU : M.cl I ∉ U
hI : M.Basis' I X
J : Set α
hYU : M.cl J ∈ U
hJ : M.Basis' J (X ∪ Y)
hIJ : I ⊆ J
hJ' : M.Basis J (M.cl Y)
hnt : (J \ I).Nontrivial
hssu : I ⊂ J
x✝ : ¬(M.cl I ⋖[M] M.cl J)
x : α
hx : x ∈ J \ I
y : α
hy : y ∈ J \ I
hyx : y ≠ x
hyE : y ∈ M.E
hyX : y ∉ M.cl X
hyY : y ∈ Y
hmax : M.cl (insert y I) ∈ U
⊢ M.cl (J \ {x}) ∈ U