To illustrate some trade-offs we did, consider the following two (equivalent)
definitions of converting the 3-sum matrix from the form of
a type-indexed nested block matrix to a matrix indexed by
elements of the standard representation of the resulting matroid.
\begin{leancode}
def Matrix.toMatrixDropUnionDrop {α : Type*}
    [DecidableEq α] {Xₗ Yₗ Xᵣ Yᵣ : Set α}
    {R : Type*}
    [∀ a, Decidable (a ∈ Xₗ)]
    [∀ a, Decidable (a ∈ Yₗ)]
    [∀ a, Decidable (a ∈ Xᵣ)]
    [∀ a, Decidable (a ∈ Yᵣ)]
    {x₀ₗ x₁ₗ x₂ₗ : Xₗ} {y₀ₗ y₁ₗ y₂ₗ : Yₗ}
    {x₀ᵣ x₁ᵣ x₂ᵣ : Xᵣ} {y₀ᵣ y₁ᵣ y₂ᵣ : Yᵣ}
    (A : Matrix
      ((Xₗ.drop3 x₀ₗ x₁ₗ x₂ₗ ⊕ Unit)
      ⊕ (Fin 2 ⊕ Xᵣ.drop3 x₀ᵣ x₁ᵣ x₂ᵣ))
      ((Yₗ.drop3 y₀ₗ y₁ₗ y₂ₗ ⊕ Fin 2)
      ⊕ (Unit ⊕ Yᵣ.drop3 y₀ᵣ y₁ᵣ y₂ᵣ))
      R) :
    Matrix
      (Xₗ.drop2 x₀ₗ x₁ₗ ∪ Xᵣ.drop1 x₂ᵣ).Elem
      (Yₗ.drop1 y₂ₗ ∪ Yᵣ.drop2 y₀ᵣ y₁ᵣ).Elem
      R :=
  A.submatrix
    (fun i : (Xₗ.drop2 x₀ₗ x₁ₗ ∪ Xᵣ.drop1 x₂ᵣ).Elem =>
      if hi₂ₗ : i.val = x₂ₗ then
        ◩◪0 else
      if hiXₗ : i.val ∈ Xₗ.drop3 x₀ₗ x₁ₗ x₂ₗ then
        ◩◩⟨i, hiXₗ⟩ else
      if hi₀ᵣ : i.val = x₀ᵣ then
        ◪◩0 else
      if hi₁ᵣ : i.val = x₁ᵣ then
        ◪◩1 else
      if hiXᵣ : i.val ∈ Xᵣ.drop3 x₀ᵣ x₁ᵣ x₂ᵣ then
        ◪◪⟨i, hiXᵣ⟩ else
      False.elim sorry)
    (fun j : (Yₗ.drop1 y₂ₗ ∪ Yᵣ.drop2 y₀ᵣ y₁ᵣ).Elem =>
      if hj₀ₗ : j.val = y₀ₗ then
        ◩◪0 else
      if hj₁ₗ : j.val = y₁ₗ then
        ◩◪1 else
      if hjYₗ : j.val ∈ Yₗ.drop3 y₀ₗ y₁ₗ y₂ₗ then
        ◩◩⟨j, hjYₗ⟩ else
      if hj₂ᵣ : j.val = y₂ᵣ then
        ◪◩0 else
      if hjYᵣ : j.val ∈ Yᵣ.drop3 y₀ᵣ y₁ᵣ y₂ᵣ then
        ◪◪⟨j, hjYᵣ⟩ else
      False.elim sorry)
\end{leancode}
The second definition starts by building two auxiliary bijections:
\begin{leancode}
private def equiv₃X {Xₗ Xᵣ : Set α}
    [∀ a, Decidable (a ∈ Xₗ)]
    [∀ a, Decidable (a ∈ Xᵣ)]
    {x₀ₗ x₁ₗ x₂ₗ : Xₗ} {x₀ᵣ x₁ᵣ x₂ᵣ : Xᵣ}
    (hx₀ₗ : x₁ₗ ≠ x₂ₗ) (hx₁ₗ : x₀ₗ ≠ x₂ₗ)
    (hx₀ᵣ : x₁ᵣ ≠ x₂ᵣ) (hx₁ᵣ : x₀ᵣ ≠ x₂ᵣ)
    (hx₂ᵣ : x₀ᵣ ≠ x₁ᵣ) :
    (Xₗ.drop3 x₀ₗ x₁ₗ x₂ₗ ⊕ Unit) ⊕
    (Fin 2 ⊕ Xᵣ.drop3 x₀ᵣ x₁ᵣ x₂ᵣ) ≃
    (Xₗ.drop2 x₀ₗ x₁ₗ).Elem ⊕ (Xᵣ.drop1 x₂ᵣ).Elem :=
  Equiv.sumCongr
    (((equivFin1 x₂ₗ).rightCongr.trans
      (Xₗ.drop3_disjoint₂ x₀ₗ x₁ₗ x₂ₗ
        ).equivSumUnion).trans
      (drop3_union_mem hx₁ₗ hx₀ₗ).≃)
    (((equivFin2 hx₂ᵣ).leftCongr.trans
      (Xᵣ.drop3_disjoint₀₁ x₀ᵣ x₁ᵣ x₂ᵣ
        ).symm.equivSumUnion).trans
      (pair_union_drop3 hx₁ᵣ hx₀ᵣ).≃)
\end{leancode}
Then \texttt{equiv₃Y} is defined similarly.
Afterwards, \texttt{Matrix.toIntermediate} is defined as
reindexing matrix by \texttt{equiv₃X} for the row index and
by \texttt{equiv₃Y} for the column index.
Finally, we can show the second definition of the
aforementioned conversion.
\begin{leancode}
private def Matrix.toMatrixDropUnionDropInternal
    {α : Type*} [DecidableEq α] {Xₗ Yₗ Xᵣ Yᵣ : Set α}
    {R : Type*}
    [∀ a, Decidable (a ∈ Xₗ)]
    [∀ a, Decidable (a ∈ Yₗ)]
    [∀ a, Decidable (a ∈ Xᵣ)]
    [∀ a, Decidable (a ∈ Yᵣ)]
    {x₀ₗ x₁ₗ x₂ₗ : Xₗ} {y₀ₗ y₁ₗ y₂ₗ : Yₗ}
    {x₀ᵣ x₁ᵣ x₂ᵣ : Xᵣ} {y₀ᵣ y₁ᵣ y₂ᵣ : Yᵣ}
    (A : Matrix
      ((Xₗ.drop3 x₀ₗ x₁ₗ x₂ₗ ⊕ Unit)
      ⊕ (Fin 2 ⊕ Xᵣ.drop3 x₀ᵣ x₁ᵣ x₂ᵣ))
      ((Yₗ.drop3 y₀ₗ y₁ₗ y₂ₗ ⊕ Fin 2)
      ⊕ (Unit ⊕ Yᵣ.drop3 y₀ᵣ y₁ᵣ y₂ᵣ))
      R)
    (hx₀ₗ : x₁ₗ ≠ x₂ₗ) (hx₁ₗ : x₀ₗ ≠ x₂ₗ)
    (hx₀ᵣ : x₁ᵣ ≠ x₂ᵣ) (hx₁ᵣ : x₀ᵣ ≠ x₂ᵣ)
    (hx₂ᵣ : x₀ᵣ ≠ x₁ᵣ) (hy₀ₗ : y₁ₗ ≠ y₂ₗ)
    (hy₁ₗ : y₀ₗ ≠ y₂ₗ) (hy₂ₗ : y₀ₗ ≠ y₁ₗ)
    (hy₀ᵣ : y₁ᵣ ≠ y₂ᵣ) (hy₁ᵣ : y₀ᵣ ≠ y₂ᵣ) :
    Matrix
      (Xₗ.drop2 x₀ₗ x₁ₗ ∪ Xᵣ.drop1 x₂ᵣ).Elem
      (Yₗ.drop1 y₂ₗ ∪ Yᵣ.drop2 y₀ᵣ y₁ᵣ).Elem
      R :=
  (A.toIntermediate
    hx₀ₗ hx₁ₗ hx₀ᵣ hx₁ᵣ hx₂ᵣ
    hy₀ₗ hy₁ₗ hy₂ₗ hy₀ᵣ hy₁ᵣ
  ).toMatrixUnionUnion
\end{leancode}
Understanding what \texttt{Matrix.toMatrixDropUnionDrop} does
is much easier than reading \texttt{Matrix.toMatrixDropUnionDropInternal}
with its dependencies and checking that it does
the thing it is supposed to do.
The extra conditions on elements being distinct are not
the main reason why \texttt{Matrix.toMatrixDropUnionDropInternal} was
excluded from the trusted code\,---\,these conditions would need
to be satisfied either way. The main reason against it is
the length of the definition (together with its dependencies)
and the difficulty of understanding what those intricate constructions
with \texttt{Equiv.sumCongr} and \texttt{Equiv.trans} actually do.
While \texttt{Matrix.toMatrixDropUnionDropInternal} was excluded from
the trusted code, it has been preserved in the 3-sum file as
a private definition because it is very useful for proving
\texttt{standardReprSum3\_hasTuSigning}.
The reason is compositionality.
By calling \texttt{Matrix.toMatrixUnionUnion} on the outermost layer,
we can use convenient lemmas such as
\texttt{Matrix.IsTotallyUnimodular.toMatrixElemElem} in
the subsequent proofs.
By implementing \texttt{equiv₃X} and \texttt{equiv₃Y} as
a composition of equivalences, we make it possible to inject
the swapping between \texttt{x₀} and \texttt{x₁} and/or
the swapping between \texttt{y₀} and \texttt{y₁} on the innermost layer.
The price of having both \texttt{Matrix.toMatrixDropUnionDrop}
and \texttt{Matrix.toMatrixDropUnionDropInternal} in the code is
that we needed to prove their equality (circa 100 lines) so that,
since \texttt{Matrix.toMatrixDropUnionDrop} is in the 3-sum definition
in the trusted code, we start the StandardRepr-level proof of regularity
of the 3-sum by collecting the necessary assumptions so that we can
rewrite \texttt{Matrix.toMatrixDropUnionDrop} to
\texttt{Matrix.toMatrixDropUnionDropInternal} and
continue the proof in the convenient way.
We believe that this is a reasonable price to pay for having the trusted
code cleaner and that our choice could guide future formalization projects
towards a code that is both believable and extensible.