have h₃ : A ⊆ B := Set.diff_subset
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
h₂ : B ⊆ C
⊢ M.relRank A C = M.relRank A B + M.relRank B C
α : Type u_1
A✝ B✝ I J X : Set α
x : α
M : RankMatroid α
y : α
hxy : ¬x = y
C : Set α := Set.insert x I
hy : y ∈ C
hr : M.relRank (C \ {y}) C ≤ 0
B : Set α := I
hI_indep : M.Indep B
hx : x ∈ M.E \ B
A : Set α := I \ {y}
h : M.relRank A C ≤ 1
h₂ : B ⊆ C
h₃ : A ⊆ B
⊢ M.relRank A C = M.relRank A B + M.relRank B C