∀ (m_2 : ℕ) (n_2 : Fin m_2.succ → ℕ),
  finSigmaFinEquiv =
    Trans.trans
      (Trans.trans
        (Trans.trans
          (Trans.trans finSumFinEquiv.sigmaCongrLeft.symm (Equiv.sumSigmaDistrib fun a => Fin (n_2 (finSumFinEquiv a))))
          (finSigmaFinEquiv.sumCongr (Equiv.uniqueSigma fun i => Fin (n_2 (finSumFinEquiv (Sum.inr i))))))
        finSumFinEquiv)
      (finCongr ⋯)