simp only [Set.mem_setOf_eq, and_imp, not_and, not_forall, Classical.not_imp, exists_prop, exists_and_left] 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 ∉
    {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
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.Indep I → I ⊆ X → ∃ x, M.Indep x ∧ x ⊆ X ∧ I ⊆ x ∧ ¬x ⊆ I
⊢ M.relRank I X ≠ 0