by_cases hxy : x = y
case refine_2.intro.intro
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hy : y ∈ Set.insert x I
hr : M.relRank (Set.insert x I \ {y}) (Set.insert x I) ≤ 0
⊢ M.relRank I (Set.insert x I) ≤ 0
case pos
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hy : y ∈ Set.insert x I
hr : M.relRank (Set.insert x I \ {y}) (Set.insert x I) ≤ 0
hxy : x = y
⊢ M.relRank I (Set.insert x I) ≤ 0

case neg
α : Type u_1
A B I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hy : y ∈ Set.insert x I
hr : M.relRank (Set.insert x I \ {y}) (Set.insert x I) ≤ 0
hxy : ¬x = y
⊢ M.relRank I (Set.insert x I) ≤ 0