theorem Matroid.Connected.contract_delete_connected_of_mem_triangle_of_series {α : Type u_1} {M : Matroid α} {e f : α} {T : Set α} (hM : M.Connected) (hT : M.IsTriangle T) (heT : e ∈ T) (hfT : f ∈ T) (hef : e ≠ f) (h_series : M✶.Parallel e f) : ((M.contract {e}).delete {f}).Connected

theorem Matroid.Connected.contract_delete_connected_of_mem_triad_of_parallel {α : Type u_1} {M : Matroid α} {e f : α} {T : Set α} (hM : M.Connected) (hT : M.IsTriad T) (heT : e ∈ T) (hfT : f ∈ T) (hef : e ≠ f) (h_para : M.Parallel e f) : ((M.contract {e}).delete {f}).Connected

theorem Matroid.IsTriangle.small_of_isTriangle_isTriad {α : Type u_1} {M : Matroid α} {a b c d : α} (habc : M.IsTriangle {a, b, c}) (habd : M.IsTriangle {a, b, d}) (hbcd : M.IsTriad {b, c, d}) (ha : (M.contract {a}).Connected) : M.delete {d} = unifOn {a, b, c} 2

If a four-element set {a, b, c, d} contains two triangles through a and b, and a triad not containing both a and b, and M ／ {a} is connected, then the matroid is U₂,₄, or a parallel extension of U₂,₃.

theorem Matroid.IsTriangle.triad_of_isTriangle_isTriad {α : Type u_1} {M : Matroid α} {a b c d : α} (habc : M.IsTriangle {a, b, c}) (habd : M.IsTriangle {a, b, d}) (hbcd : M.IsTriad {b, c, d}) (ha : (M.contract {a}).Connected) : M.IsTriad {a, c, d}