contrapose! hr
case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : M.relRank I X = 0
⊢ I ∈ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
case refine_2
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI : I ⊆ X
hI_indep : M.Indep I
hr : I ∉ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
⊢ M.relRank I X ≠ 0