calc
  M.relRank A B = M.relRank I A + M.relRank A B := by
    rw [hIA]; simp only [zero_add]
  _ = M.relRank I B := by
    exact eq_comm.mp (M.relRank_add_cancel hI_subset hA)
  _ = M.relRank I J + M.relRank J B := by
    exact M.relRank_add_cancel hI hJ_subset
  _ = M.relRank I J := by
    rw [hJB]; simp only [add_zero]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : 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 = M.relRank I J
no goals