ST-05: the relative complement construction in lem:flat-complement. The recursion is the paper's simultaneous adjoining of an element to S and T; it terminates because the corank of S decreases strictly at each step.

theorem TutteFormalization.natRank_closure_insert {α : Type u_1} {M : Matroid α} [M.Finite] {S : Set α} (hS : M.IsFlat S) {e : α} (he : e ∈ M.E) (heS : e ∉ S) : natRank M (M.closure (insert e S)) = natRank M S + 1

theorem TutteFormalization.exists_relative_complement_data {α : Type u_1} {M : Matroid α} [M.Finite] (S T : Set α) (hS : M.IsFlat S) (hT : M.IsFlat T) (hTS : T ⊆ S) : ∃ (U : Set α), M.IsFlat U ∧ T ⊆ U ∧ M.closure (U ∪ S) = M.E ∧ natRank M U + natRank M S = natRank M T + natRank M M.E

ST-05: recursive construction before the final intersection calculation. The additive rank equation avoids truncated subtraction in the invariant.

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

ST-05: full relative complement, with the source corank formula.