rw [restrictSubtype, ← comapOn_preimage_eq, comapOn_dual_eq_of_bijOn, restrict_ground_eq_self,
  ← dual_ground, comapOn_preimage_eq, restrictSubtype, restrict_ground_eq_self]
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I : Set α
M N : Matroid α
⊢ (M.restrictSubtype M.E)✶ = M✶.restrictSubtype M.E
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I : Set α
M N : Matroid α
⊢ BijOn Subtype.val (M.E ↓∩ (M ↾ M.E).E) (M ↾ M.E).E