refine' ⟨B \ {b}, ⟨b, ⟨hb.1, hb.2⟩, rfl⟩⟩
case Js₁_none.intro
α : 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
b : α
hb : b ∈ B ∧ b ∉ Y
⊢ Js₁.Nonempty
no goals