The source prop:indecomposable-diamond construction.

theorem TutteFormalization.exists_indecomposable_diamond {α : Type u_1} {M : Matroid α} [M.Finite] {S T : Set α} (hS : Indecomposable M S) (hT : Indecomposable M T) (hTS : T ⊆ S) (hSr : natRank M S = natRank M T + 2) : ∃ (U : Set α) (V : Set α), Indecomposable M U ∧ Indecomposable M V ∧ T ⊆ U ∧ T ⊆ V ∧ U ⊆ S ∧ V ⊆ S ∧ U ≠ V ∧ natRank M U = natRank M T + 1 ∧ natRank M V = natRank M T + 1