unfold maximals at 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 : I ∉ maximals (fun x x_1 => x ⊆ x_1) {S | M.Indep S ∧ S ⊆ X}
⊢ M.relRank I X ≠ 0
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 ∉
    {a |
      a ∈ {S | M.Indep S ∧ S ⊆ X} ∧
        ∀ ⦃b : Set α⦄, b ∈ {S | M.Indep S ∧ S ⊆ X} → (fun x x_1 => x ⊆ x_1) a b → (fun x x_1 => x ⊆ x_1) b a}
⊢ M.relRank I X ≠ 0