prop:indecomposable-complement: minimal-rank crossing cover and corank induction.

theorem TutteFormalization.exists_indecomposable_cover_not_subset {α : Type u_1} {M : Matroid α} [M.Finite] {S T U : Set α} (hS : Indecomposable M S) (hT : Indecomposable M T) (hU : M.IsFlat U) (hTS : T ⊆ S) (hTU : T ⊆ U) (hnSU : ¬S ⊆ U) : ∃ (W : Set α), Indecomposable M W ∧ T ⊆ W ∧ W ⊆ S ∧ ¬W ⊆ U ∧ natRank M W = natRank M T + 1

The minimal-rank argument in the source complement proof.

theorem TutteFormalization.exists_indecomposable_complement {α : Type u_1} {M : Matroid α} [M.Finite] {S T U : Set α} (hS : Indecomposable M S) (hT : Indecomposable M T) (hU : M.IsFlat U) (hTS : T ⊆ S) (hTU : T ⊆ U) (hjoin : M.closure (S ∪ U) = M.E) : ∃ (R : Set α), Indecomposable M R ∧ T ⊆ R ∧ R ⊆ S ∧ M.closure (R ∪ U) = M.E ∧ natRank M M.E - natRank M R = natRank M U - natRank M T

Source indecomposable complement, with the literal corank equation.