Theorem: Matroid.flat_of_deleteElem_flat (Matroid/Old/ModularCut.lean)

State before:
α : Type u_1
e : α
F : Set α
M : Matroid α
e_nF : e ∉ F
hF : M.Flat (insert e F)
⊢ (M ＼ e).Flat F
Tactic:
rw [flat_iff_cl_self, deleteElem, delete_cl_eq, diff_singleton_eq_self e_nF]
State after:
α : Type u_1
e : α
F : Set α
M : Matroid α
e_nF : e ∉ F
hF : M.Flat (insert e F)
⊢ M.cl F \ {e} = F

State before:
α : Type u_1
e : α
F : Set α
M : Matroid α
e_nF : e ∉ F
hF : M.Flat (insert e F)
⊢ M.cl F \ {e} = F
Tactic:
apply subset_antisymm _ (subset_diff_singleton (M.subset_cl _ ((subset_insert _ _).trans
 hF.subset_ground)) e_nF)
State after:
α : Type u_1
e : α
F : Set α
M : Matroid α
e_nF : e ∉ F
hF : M.Flat (insert e F)
⊢ M.cl F \ {e} ⊆ F

State before:
α : Type u_1
e : α
F : Set α
M : Matroid α
e_nF : e ∉ F
hF : M.Flat (insert e F)
⊢ M.cl F \ {e} ⊆ F
Tactic:
rw [diff_singleton_subset_iff]
State after:
α : Type u_1
e : α
F : Set α
M : Matroid α
e_nF : e ∉ F
hF : M.Flat (insert e F)
⊢ M.cl F ⊆ insert e F

State before:
α : Type u_1
e : α
F : Set α
M : Matroid α
e_nF : e ∉ F
hF : M.Flat (insert e F)
⊢ M.cl F ⊆ insert e F
Tactic:
apply (hF.cl_subset_of_subset (subset_insert _ _))
State after:
no goals