rw [Set.diff_diff_right] at h
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h : M.relRank A B ≤ (B \ A).encard
⊢ M.relRank A B ≤ 1
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
hI_indep : M.Indep I
hx : x ∈ M.E \ I
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
B : Set α := Set.insert x I \ {y}
hr : M.relRank B C ≤ 0
A : Set α := I \ {y}
h₂ : B ⊆ C
h₃ : A ⊆ B
h : M.relRank A B ≤ (B \ I ∪ B ∩ {y}).encard
⊢ M.relRank A B ≤ 1