@[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)