Theorem: Matroid.Restriction.exists_eq_delete (Matroid/Minor/Basic.lean)

State before:
α : Type u_1
M M' N : Matroid α
e f : α
I J R✝ B X Y Z K D D₁ D₂ R : Set α
hNM : N ≤r M
⊢ N = M ＼ (M.E \ N.E)
Tactic:
obtain ⟨R, hR, rfl⟩ := hNM
State after:
case intro.intro
α : Type u_1
M M' : Matroid α
e f : α
I J R✝¹ B X Y Z K D D₁ D₂ R✝ R : Set α
hR : R ⊆ M.E
⊢ M ↾ R = M ＼ (M.E \ (M ↾ R).E)

State before:
case intro.intro
α : Type u_1
M M' : Matroid α
e f : α
I J R✝¹ B X Y Z K D D₁ D₂ R✝ R : Set α
hR : R ⊆ M.E
⊢ M ↾ R = M ＼ (M.E \ (M ↾ R).E)
Tactic:
rw [delete_compl, restrict_ground_eq]
State after:
no goals