Explicit rank calculations used in the source Diamond construction.

theorem TutteFormalization.corankTwo_iff_natRank {α : Type u_1} {M : Matroid α} [M.Finite] {T : Set α} (hF : M.IsFlat T) : CorankTwo M T ↔ natRank M T + 2 = natRank M M.E

theorem TutteFormalization.union_ne_ground_of_indecomposable_inter {α : Type u_1} {M : Matroid α} [M.Finite] {T X Y : Set α} (hT : Indecomposable M T) (hX : M.IsFlat X) (hY : M.IsFlat Y) (hi : X ∩ Y = T) (hnX : X ≠ T) (hnY : Y ≠ T) (hr : natRank M X + natRank M Y = natRank M T + natRank M M.E) : X ∪ Y ≠ M.E

theorem TutteFormalization.diamond_join_inter {α : Type u_1} {M : Matroid α} [M.Finite] {S T L P : Set α} (hS : M.IsFlat S) (hL : CorankTwo M L) (hP : M.IsFlat P) (hi : L ∩ S = T) (hTP : T ⊂ P) (hPS : P ⊆ S) (hSr : natRank M S = natRank M T + 2) (hPr : natRank M P = natRank M T + 1) (hj : M.closure (L ∪ S) = M.E) : IsHyperplane M (M.closure (L ∪ P)) ∧ S ∩ M.closure (L ∪ P) = P

theorem TutteFormalization.cover_flats_inter_eq {α : Type u_1} {M : Matroid α} [M.Finite] {F P Q : Set α} (hF : M.IsFlat F) (hP : M.IsFlat P) (hQ : M.IsFlat Q) (hFP : F ⊆ P) (hFQ : F ⊆ Q) (hrP : natRank M P = natRank M F + 1) (hrQ : natRank M Q = natRank M F + 1) (hne : P ≠ Q) : P ∩ Q = F

theorem TutteFormalization.cover_flats_join_eq {α : Type u_1} {M : Matroid α} [M.Finite] {F P Q S : Set α} (hS : M.IsFlat S) (hP : M.IsFlat P) (hQ : M.IsFlat Q) (hPS : P ⊆ S) (hQS : Q ⊆ S) (hrP : natRank M P = natRank M F + 1) (hrQ : natRank M Q = natRank M F + 1) (hrS : natRank M S = natRank M F + 2) (hne : P ≠ Q) : M.closure (P ∪ Q) = S