Theorem: Matroid.restrictSubtype_dual' (Matroid/Map.lean)

State before:
α : Type u_1
β : Type u_2
f : α → β
E✝ I✝ s : Set α
M✝ : Matroid α
N✝ : Matroid β
E X I : Set α
M N : Matroid α
hM : M.E = E
⊢ (M.restrictSubtype E)✶ = M✶.restrictSubtype E
Tactic:
rw [← hM, restrictSubtype_dual]
State after:
no goals