Connectivity background in additive-partition form. This verifies the needed conclusions without claiming to audit the source's cocircuit proof.

theorem TutteFormalization.connected_iff_no_natRank_partition {α : Type u_1} {M : Matroid α} [M.Finite] : Connected M ↔ ¬∃ (A : Set α) (B : Set α), A.Nonempty ∧ B.Nonempty ∧ Disjoint A B ∧ A ∪ B = M.E ∧ natRank M A + natRank M B = natRank M M.E

theorem TutteFormalization.connected_contract_partition_side {α : Type u_1} {M : Matroid α} [M.Finite] {A B F : Set α} (hd : Disjoint A B) (hu : A ∪ B = M.E) (hr : natRank M A + natRank M B = natRank M M.E) (hF : F ⊆ M.E) (hc : Connected (M.contract F)) : A ⊆ F ∨ B ⊆ F

theorem TutteFormalization.indecomposable_inter {α : Type u_1} {M : Matroid α} [M.Finite] {F₁ F₂ : Set α} (h₁ : Indecomposable M F₁) (h₂ : Indecomposable M F₂) (hu : F₁ ∪ F₂ ≠ M.E) : Indecomposable M (F₁ ∩ F₂)

prop:connected-intersection, via the same direct-sum obstruction in rank form. The source's particular common-cocircuit argument is not claimed audited.