refine' ⟨fun h ↦ _, fun h ↦ by rw [h]⟩
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
⊢ M ＼ (D₁ ∩ M.E) = M ＼ (D₂ ∩ M.E) ↔ D₁ ∩ M.E = D₂ ∩ M.E
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
h : M ＼ (D₁ ∩ M.E) = M ＼ (D₂ ∩ M.E)
⊢ D₁ ∩ M.E = D₂ ∩ M.E