contrapose! hI_max
case neg
α : Type u_1
A B I J X : Set α
x✝ : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hI_max : I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
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
⊢ M.relRank I (insert x I) = 0
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
⊢ I ∉ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}