rw [<-relRank_inter_ground, relRank_eq_union_right, <-M.matroid.relRank_inter_ground_left,
    <-M.matroid.relRank_inter_ground_right, M.matroid.relRank_eq_union_right]
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
h : ∀ {A B : Set α}, A ⊆ B → B ⊆ M.E → M.relRank A B = M.matroid.relRank A B
A' : Set α := A ∩ M.E
B' : Set α := B ∩ M.E ∪ A'
⊢ M.relRank A B = M.matroid.relRank A B
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
h : ∀ {A B : Set α}, A ⊆ B → B ⊆ M.E → M.relRank A B = M.matroid.relRank A B
A' : Set α := A ∩ M.E
B' : Set α := B ∩ M.E ∪ A'
⊢ M.relRank (A ∩ M.E) (B ∩ M.E ∪ A ∩ M.E) = M.matroid.relRank (A ∩ M.matroid.E) (B ∩ M.matroid.E ∪ A ∩ M.matroid.E)