@[simp]

theorem Matroid.delete_ground_self {α : Type u_1} (M : Matroid α) : M.delete M.E = emptyOn α

theorem Matroid.Loopless.delete {α : Type u_1} {M : Matroid α} (h : M.Loopless) (D : Set α) : (M.delete D).Loopless

instance Matroid.instLooplessDelete_matroid {α : Type u_1} {M : Matroid α} [h : M.Loopless] {D : Set α} : (M.delete D).Loopless

theorem Matroid.removeLoops_eq_delete {α : Type u_1} (M : Matroid α) : M.removeLoops = M.delete M.loops

theorem Matroid.removeLoops_del_eq_removeLoops {α : Type u_1} {M : Matroid α} {X : Set α} (h : X ⊆ M.loops) : (M.delete X).removeLoops = M.removeLoops

@[simp]

theorem Matroid.sum_delete {α : Type u_2} {β : Type u_3} (M : Matroid α) (N : Matroid β) (D : Set (α ⊕ β)) : (M.sum N).delete D = (M.delete (Sum.inl ⁻¹' D)).sum (N.delete (Sum.inr ⁻¹' D))

theorem Matroid.disjointSigma_delete {α : Type u_1} {ι : Type u_2} (M : ι → Matroid α) (h : Pairwise (Function.onFun Disjoint fun (i : ι) => (M i).E)) (D : Set α) : (Matroid.disjointSigma M h).delete D = Matroid.disjointSigma (fun (i : ι) => (M i).delete D) ⋯

theorem Matroid.disjointSum_delete {α : Type u_1} {D : Set α} {M N : Matroid α} (hMN : Disjoint M.E N.E) : (M.disjointSum N hMN).delete D = (M.delete D).disjointSum (N.delete D) ⋯

theorem Matroid.disjointSum_delete_left {α : Type u_1} {D : Set α} {M N : Matroid α} (hMN : Disjoint M.E N.E) (hD : D ⊆ M.E) : (M.disjointSum N hMN).delete D = (M.delete D).disjointSum N ⋯

theorem Matroid.disjointSum_delete_right {α : Type u_1} {D : Set α} {M N : Matroid α} (hMN : Disjoint M.E N.E) (hD : D ⊆ N.E) : (M.disjointSum N hMN).delete D = M.disjointSum (N.delete D) ⋯

theorem Matroid.Dep.delete_of_disjoint {α : Type u_1} {M : Matroid α} {X D : Set α} (hX : M.Dep X) (hXD : Disjoint X D) : (M.delete D).Dep X

theorem Matroid.Dep.of_delete {α : Type u_1} {M : Matroid α} {X D : Set α} (h : (M.delete D).Dep X) : M.Dep X

theorem Matroid.removeLoops_disjointSum {α : Type u_1} (M : Matroid α) : M = M.removeLoops.disjointSum (loopyOn M.loops) ⋯

@[simp]

theorem Matroid.loopyOn_delete {α : Type u_1} (E X : Set α) : (loopyOn E).delete X = loopyOn (E \ X)

@[simp]

theorem Matroid.freeOn_delete {α : Type u_1} (E X : Set α) : (freeOn E).delete X = freeOn (E \ X)

theorem Matroid.delete_restrict_eq_restrict {α : Type u_1} (M : Matroid α) {D R : Set α} (hDR : Disjoint D R) : (M.delete D).restrict R = M.restrict R

theorem Matroid.delete_restrict_ground_of_subset_loops {α : Type u_1} {M : Matroid α} {L : Set α} (hL : L ⊆ M.loops) : (M.delete L).restrict M.E = M

theorem Matroid.IsRestriction.delete {α : Type u_1} {M N : Matroid α} (h : N.IsRestriction M) (D : Set α) : (N.delete D).IsRestriction (M.delete D)

theorem Matroid.restrict_comap {α : Type u_1} {β : Type u_2} (M : Matroid β) (f : α → β) (R : Set β) : (M.restrict R).comap f = (M.comap f).restrict (f ⁻¹' R)

theorem Matroid.delete_comap {α : Type u_1} {β : Type u_2} (M : Matroid β) (f : α → β) (D : Set β) : (M.delete D).comap f = (M.comap f).delete (f ⁻¹' D)

theorem Matroid.restrict_map {α : Type u_1} {M : Matroid α} {R : Set α} {β : Type u_2} {f : α → β} (hf : Set.InjOn f M.E) (hR : R ⊆ M.E) : (M.restrict R).map f ⋯ = (M.map f hf).restrict (f '' R)

theorem Matroid.delete_map {α : Type u_1} {M : Matroid α} {D : Set α} {β : Type u_2} {f : α → β} (hf : Set.InjOn f M.E) (hD : D ⊆ M.E) : (M.delete D).map f ⋯ = (M.map f hf).delete (f '' D)

theorem Matroid.indep_iff_restrict_eq_freeOn {α : Type u_1} {M : Matroid α} {I : Set α} : M.Indep I ↔ M.restrict I = freeOn I

theorem Matroid.restrict_eq_delete_disjointSum_loopyOn {α : Type u_1} (M : Matroid α) (R : Set α) : M.restrict R = (M.delete (M.E \ R)).disjointSum (loopyOn (R \ M.E)) ⋯

theorem Matroid.restrict_eq_restrict_inter_ground_disjointSum_loopyOn {α : Type u_1} (M : Matroid α) (R : Set α) : M.restrict R = (M.restrict (R ∩ M.E)).disjointSum (loopyOn (R \ M.E)) ⋯

theorem Matroid.deleteElem_of_notMem_ground {α : Type u_1} {M : Matroid α} {e : α} (h : e ∉ M.E) : M.delete {e} = M

@[simp]

theorem Matroid.emptyOn_isRestriction {α : Type u_1} (M : Matroid α) : (emptyOn α).IsRestriction M

@[simp]

theorem Matroid.isRestriction_emptyOn_iff {α : Type u_1} {M : Matroid α} : M.IsRestriction (emptyOn α) ↔ M = emptyOn α

theorem Matroid.Coindep.delete_nonspanning_iff {α : Type u_1} {M : Matroid α} {X D : Set α} (hD : M.Coindep D) : (M.delete D).Nonspanning X ↔ M.Nonspanning X ∧ Disjoint X D

theorem Matroid.Coindep.delete_coindep_iff {α : Type u_1} {M : Matroid α} {X D : Set α} (hD : M.Coindep D) : (M.delete D).Coindep X ↔ M.Coindep (X ∪ D) ∧ Disjoint X D

theorem Matroid.Coindep.delete_codep_iff {α : Type u_1} {M : Matroid α} {X D : Set α} (hD : M.Coindep D) : (M.delete D).Codep X ↔ M.Codep (X ∪ D) ∧ Disjoint X D

theorem Matroid.girth_le_girth_delete {α : Type u_1} (M : Matroid α) (D : Set α) : M.girth ≤ (M.delete D).girth

theorem Matroid.Nonspanning.of_delete {α : Type u_1} {M : Matroid α} {X D : Set α} (h : (M.delete D).Nonspanning X) : M.Nonspanning X

theorem Matroid.Nonspanning.of_isRestriction {α : Type u_1} {M N : Matroid α} {X : Set α} (h : N.Nonspanning X) (hNM : N.IsRestriction M) : M.Nonspanning X

theorem Matroid.Coindep.delete_isSpanningRestriction {α : Type u_1} {M : Matroid α} {X : Set α} (hX : M.Coindep X) : (M.delete X).IsSpanningRestriction M

theorem Matroid.delete_isSpanningRestriction_iff {α : Type u_1} {M : Matroid α} {X : Set α} (hX : X ⊆ M.E := by aesop_mat) : (M.delete X).IsSpanningRestriction M ↔ M.Coindep X

theorem Matroid.IsRestriction.eq_delete {α : Type u_1} {M N : Matroid α} (h : N.IsRestriction M) : N = M.delete (M.E \ N.E)

theorem Matroid.IsRestriction.eq_of_isRestriction_of_ground_eq {α : Type u_1} {M N N' : Matroid α} (h : N.IsRestriction M) (h' : N'.IsRestriction M) (hE : N.E = N'.E) : N = N'

theorem Matroid.delete_restrict_ground_eq_disjointSum {α : Type u_1} {M : Matroid α} {D : Set α} (hD : D ⊆ M.E) : (M.delete D).restrict M.E = (M.delete D).disjointSum (loopyOn D) ⋯

theorem Matroid.IsSpanningRestriction.exists_eq_delete {α : Type u_1} {M N : Matroid α} (h : N.IsSpanningRestriction M) : ∃ (D : Set α), M.Coindep D ∧ N = M.delete D