have hxEI : x ∈ M.E \ I := by exact (Set.mem_diff x).mpr ⟨hx, hxI⟩
case neg
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max✝ : M.relRank I (insert x I) ≠ 0
hI_max : M.relRank I (insert x I) > 0
⊢ M.Indep (insert x I)
case neg
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hXI : ¬X = I
S : Set (Set α) := {x | ∃ x_1 ∈ X \ I, insert x_1 I = x}
x : α
hx_mem : x ∈ X \ I
hxX : x ∈ X
hxI : x ∉ I
hx : x ∈ M.E
hI_max✝ : M.relRank I (insert x I) ≠ 0
hI_max : M.relRank I (insert x I) > 0
hxEI : x ∈ M.E \ I
⊢ M.Indep (insert x I)