refine ⟨fun hY ↦ ?_, fun hY ↦ ?_⟩
case h
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
y : α
⊢ y ∈ I \ {x} ↔ y ∈ I ∩ (J \ {x})
case h.refine_1
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
y : α
hY : y ∈ I \ {x}
⊢ y ∈ I ∩ (J \ {x})

case h.refine_2
α : Type u_1
A✝ B✝ I J X : Set α
x✝ : α
M : RankMatroid α
hJ✝ : M.Indep J
x : α
A : Set α := I
rIJ : A ⊆ J
hx : x ∈ A
B : Set α := J \ {x}
hJ : M.relRank B J > 0
hAUB : J = I ∪ J \ {x}
y : α
hY : y ∈ I ∩ (J \ {x})
⊢ y ∈ I \ {x}