@[simp]

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

@[simp]

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

theorem Matroid.contract_eq_loopyOn_of_spanning {α : Type u_1} {M : Matroid α} {C : Set α} (h : M.Spanning C) : M.contract C = loopyOn (M.E \ C)

@[simp]

theorem Matroid.contract_ground_self {α : Type u_1} (M : Matroid α) : M.contract M.E = emptyOn α

theorem Matroid.contract_map {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : α → β} (hf : Set.InjOn f M.E) {C : Set α} (hC : C ⊆ M.E) : (M.contract C).map f ⋯ = (M.map f hf).contract (f '' C)

theorem Matroid.contract_comap {α : Type u_1} {β : Type u_2} (M : Matroid β) (f : α → β) {C : Set β} (hC : C ⊆ Set.range f) : (M.contract C).comap f = (M.comap f).contract (f ⁻¹' C)

@[simp]

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

theorem Matroid.contract_closure_congr {α : Type u_1} {M : Matroid α} {X Y : Set α} (h : M.closure X = M.closure Y) (C : Set α) : (M.contract C).closure X = (M.contract C).closure Y

theorem Matroid.contract_codep_iff {α : Type u_1} {M : Matroid α} {C X : Set α} : (M.contract C).Codep X ↔ M.Codep X ∧ Disjoint X C

theorem Matroid.contractElem_of_notMem_ground {α : Type u_1} {M : Matroid α} {e : α} (he : e ∉ M.E) : M.contract {e} = M

theorem Matroid.contract_nonspanning_iff {α : Type u_1} {M : Matroid α} {C X : Set α} (hC : C ⊆ M.E := by aesop_mat) : (M.contract C).Nonspanning X ↔ M.Nonspanning (X ∪ C) ∧ Disjoint X C

theorem Matroid.contract_rankPos_iff {α : Type u_1} {M : Matroid α} {C : Set α} (hC : C ⊆ M.E := by aesop_mat) : (M.contract C).RankPos ↔ M.Nonspanning C

theorem Matroid.Nonspanning.contract_rankPos {α : Type u_1} {M : Matroid α} {C : Set α} (hC : M.Nonspanning C) : (M.contract C).RankPos

theorem Matroid.girth_le_girth_contract_add {α : Type u_1} (M : Matroid α) (C : Set α) : M.girth ≤ (M.contract C).girth + M.eRk C

theorem Matroid.Dep.contract_of_delete {α : Type u_1} {M : Matroid α} {X D : Set α} (hX : (M.delete X).Dep (D \ X)) : (M.contract X).Dep (D \ X)

theorem Matroid.Dep.contract_of_disjoint {α : Type u_1} {M : Matroid α} {C D : Set α} (hD : M.Dep D) (hDC : Disjoint D C) : (M.contract C).Dep D

theorem Matroid.contract_eq_contract_delete_of_subset_closure {α : Type u_1} {M : Matroid α} {X Y : Set α} (hXY : X ⊆ Y) (hYX : Y ⊆ M.closure X) : M.contract Y = (M.contract X).delete (Y \ X)

theorem Matroid.Dep.contract_of_indep {α : Type u_1} {M : Matroid α} {I D : Set α} (hD : M.Dep D) (hI : M.Indep (D ∩ I)) : (M.contract I).Dep (D \ I)

Contracting a set whose intersection with D is independent never turns a dependent set D into an independent set.

theorem Matroid.Codep.of_contract {α : Type u_1} {M : Matroid α} {C X : Set α} (h : (M.contract C).Codep X) : M.Codep X

theorem Matroid.Coindep.of_contract {α : Type u_1} {M : Matroid α} {I C : Set α} (h : (M.contract C).Coindep I) : M.Coindep I

theorem Matroid.Codep.of_delete {α : Type u_1} {M : Matroid α} {X D : Set α} (h : (M.delete D).Codep X) (hD : D ⊆ M.E := by aesop_mat) : M.Codep (X ∪ D)

theorem Matroid.Codep.restrict {α : Type u_1} {M : Matroid α} {R X : Set α} (hD : M.Codep X) (hXR : X ⊆ R) : (M.restrict R).Codep X

theorem Matroid.removeLoops_eq_contract {α : Type u_1} (M : Matroid α) : M.removeLoops = M.contract M.loops

theorem Matroid.removeColoops_eq_contract {α : Type u_1} (M : Matroid α) : M.removeColoops = M.contract M.coloops

theorem Matroid.removeColoops_eq_delete {α : Type u_1} (M : Matroid α) : M.removeColoops = M.delete M.coloops

theorem Matroid.removeLoops_removeColoops_comm {α : Type u_1} (M : Matroid α) : M.removeLoops.removeColoops = M.removeColoops.removeLoops

theorem Matroid.removeColoops_disjointSum {α : Type u_1} (M : Matroid α) : M = M.removeColoops.disjointSum (freeOn M.coloops) ⋯

theorem Matroid.IsRestriction.contract {α : Type u_1} {M N : Matroid α} {C : Set α} (h : N.IsRestriction M) (hC : C ⊆ N.E) : (N.contract C).IsRestriction (M.contract C)

theorem Matroid.IsSpanningRestriction.contract {α : Type u_1} {M N : Matroid α} {C : Set α} (h : N.IsSpanningRestriction M) (hC : C ⊆ N.E) : (N.contract C).IsSpanningRestriction (M.contract C)

theorem Matroid.Nonspanning.of_contract {α : Type u_1} {M : Matroid α} {C X : Set α} (h : (M.contract C).Nonspanning X) : M.Nonspanning X

theorem Matroid.Cyclic.contract {α : Type u_1} {M : Matroid α} {A : Set α} (hA : M.Cyclic A) (C : Set α) : (M.contract C).Cyclic (A \ C)

theorem Matroid.IsCircuit.isCircuit_or_isCircuit_insert_of_contractElem {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} (hC : (M.contract {e}).IsCircuit C) : M.IsCircuit C ∨ M.IsCircuit (insert e C)

theorem Matroid.IsCircuit.isCircuit_contract_of_union {α : Type u_1} {M : Matroid α} {X C : Set α} (h : M.IsCircuit (X ∪ C)) (hdj : Disjoint X C) (hne : C.Nonempty) : (M.contract X).IsCircuit C

theorem Matroid.IsCircuit.isCircuit_contractElem_of_insert {α : Type u_1} {M : Matroid α} {e : α} {C : Set α} (h : M.IsCircuit (insert e C)) (he : e ∉ C) (hC : C.Nonempty) : (M.contract {e}).IsCircuit C

theorem Matroid.ext_contractElem_deleteElem {α : Type u_1} {M N : Matroid α} {e : α} (heM : M.IsNonloop e) (heN : N.IsNonloop e) (hc : M.contract {e} = N.contract {e}) (hd : M.delete {e} = N.delete {e}) : M = N

If e is a nonloop of both M and N, and M and N agree after removing e in both ways, then M = N.

theorem Matroid.ext_contractElem_deleteElem' {α : Type u_1} {M N : Matroid α} {e : α} (heM : e ∈ M.E) (heN : e ∈ N.E) (heMl : M.IsLoop e → N.IsNonColoop e) (heNl : N.IsLoop e → M.IsNonColoop e) (hc : M.contract {e} = N.contract {e}) (hd : M.delete {e} = N.delete {e}) : M = N

A version of ext_contractElem_deleteElem with slightly weaker assumptions.