suffices h : ∀ {A B}, A ⊆ B → B ⊆ M.E → M.relRank A B = M.matroid.relRank A B by
  set A' := A ∩ M.E
  set B' := (B ∩ M.E) ∪ A'
  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]
  simp only [matroid_E]
  refine h Set.subset_union_right ?_
  rw [<-Set.union_inter_distrib_right]
  exact Set.inter_subset_right
α : Type u_1
A✝ B✝ I J X : Set α
M✝ : RankMatroid α
x : α
M : RankMatroid α
A B : Set α
⊢ 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 α
⊢ ∀ {A B : Set α}, A ⊆ B → B ⊆ M.E → M.relRank A B = M.matroid.relRank A B