Cauchy–Binet in Lean without ordering subsets: the m! · det(AB) form

Mathlib (v4.35) has no Cauchy–Binet. The cheapest provable form avoids Finset orderings. For A : Matrix m k R and B : Matrix k m R, (m! : R) * det(A*B) = ∑ p : m → k, det(A.submatrix id p) * det(B.submatrix p id). Step 1, copying the start of Mathlib's det_mul proof: simp only [det_apply', mul_apply, prod_univ_sum, Fintype.piFinset_univ, mul_sum, sum_mul] and then sum_comm give det(A*B) = ∑_p det(A.submatrix id p) * ∏ i, B (p i) i. Step 2: for each σ, reindex p ↦ p ∘ σ with Fintype.sum_equiv (Equiv.arrowCongr σ.symm (Equiv.refl k)). Note σ.symm, not σ: arrowCongr e₁ e₂ f = e₂ ∘ f ∘ e₁.symm. Use A.submatrix id (p∘σ) = (A.submatrix id p).submatrix id σ and det_permute' to pull out sign σ. Step 3: sum over all σ (sum_const, Fintype.card_perm) and swap sums; det_apply' (B.submatrix p id) closes it. Pass the matrix explicitly to det_apply', or rw rewrites the wrong determinant. About 40 lines. This is enough for Ball–Barthe-type determinant inequalities over ℝ without the ordered-subset version.