The rank-selection consequence of cor:indecomposable-chain, obtained by literally repeating the downward step. This is the chain interface needed below.

theorem TutteFormalization.exists_indecomposable_of_rank {α : Type u_1} {M : Matroid α} [M.Finite] {S T : Set α} (hS : Indecomposable M S) (hT : Indecomposable M T) (hTS : T ⊆ S) (k : ℕ) (hTk : natRank M T ≤ k) (hkS : k ≤ natRank M S) : ∃ (U : Set α), Indecomposable M U ∧ T ⊆ U ∧ U ⊆ S ∧ natRank M U = k