simp only [zero_add]
α : Type u_1
A✝¹ B✝¹ I✝ J✝ X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A✝ B✝ A B : Set α
hA : A ⊆ B
hB : B ⊆ M.E
I J : Set α
hI : I ⊆ J
right✝¹ : A ⊆ M.matroid.E
right✝ : B ⊆ M.matroid.E
hI_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ A → I ⊆ b → b ⊆ I
hI_indep : M.Indep I
hI_subset : I ⊆ A
hJ_max : ∀ ⦃b : Set α⦄, M.Indep b → b ⊆ B → J ⊆ b → b ⊆ J
hJ_indep : M.Indep J
hJ_subset : J ⊆ B
hIA : M.relRank I A = 0
hJB : M.relRank J B = 0
⊢ M.relRank A B = 0 + M.relRank A B
no goals