exact absurd rfl (x_mem (B \ {x}) ⟨x, xBY, rfl⟩).2
case Js_inter_eq.h.e'_3.h.refine'_1
α : Type u_1
M✝ : Matroid α
I B✝ : Set α
Ys Xs : Set (Set α)
M : Matroid α
C : M.ModularCut
B Y : Set α
hB₁ : M.Indep B
hB₂ : Y ⊆ B
h_remove : ∀ b ∈ B \ Y, M.cl (B \ {b}) ∈ C
h_B : M.cl B ∈ C
Js : Set (Set α) := {x | ∃ b ∈ B \ Y, M.cl (B \ {b}) = x}
Js₁ : Set (Set α) := {x | ∃ b ∈ B \ Y, B \ {b} = x}
h_ne : Y ≠ B
Js₁_none : Js₁.Nonempty
Js₁_sInter_sub_B : ⋂₀ Js₁ ⊆ B
Js_biInter_eq : ⋂ J ∈ Js, J = ⋂ J₁ ∈ Js₁, M.cl J₁
x : α
x_mem : ∀ t ∈ Js₁, x ∈ t
x_notin_Y : x ∉ Y
xBY : x ∈ B \ Y
⊢ False
no goals