Theorem: Matroid.ConnectedTo.of_delete (Matroid/Connectivity.lean)

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
D : Set α
hef : (M ＼ D).ConnectedTo e f
⊢ M.ConnectedTo e f
Tactic:
rw [delete_eq_restrict] at hef
State after:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
D : Set α
hef : (M ↾ M.E \ D).ConnectedTo e f
⊢ M.ConnectedTo e f

State before:
α : Type u_1
M : Matroid α
C K : Set α
e f g : α
D : Set α
hef : (M ↾ M.E \ D).ConnectedTo e f
⊢ M.ConnectedTo e f
Tactic:
apply hef.of_restrict diff_subset
State after:
no goals