tauto
case h.e'_5.h.e'_3.h
α : Type u_1
M : Matroid α
I✝ J✝ B F₀ F F' X Y : Set α
e f : α
U✝ U : M.ModularCut
hXE : X ⊆ insert e M.E
I : Set α
hI : U.ExtIndep e I
hIX : I ⊆ X
J : Set α
hIJ : I ⊆ J
hJ : J ∈ maximals (fun x x_1 => x ⊆ x_1) {K | U.ExtIndep e K ∧ K ⊆ X}
x✝ : Set α
⊢ U.ExtIndep e x✝ ∧ I ⊆ x✝ ∧ x✝ ⊆ X ↔ (U.ExtIndep e x✝ ∧ x✝ ⊆ X) ∧ I ⊆ x✝
no goals