mathlib3

84066cbf - feat(logic/equiv, topology/homeomorph): split a product at a coordinate (#16210)

feat(logic/equiv, topology/homeomorph): split a product at a coordinate (#16210) + Add `equiv.pi_split_at` and `homeomorph.pi_split_at`: for every "coordinate" `i : α`, the bijection/homeomorphism between a product `Π j : α, β j` of types/topological spaces and the binary product of the type/space `β i` at that coordinate and the product `Π j : {j // j ≠ i}, β j` over all other coordinates. + Specialize to get the non-dependent versions, which concerns a product of copies of the same type/topological space, in which case non-dependent versions are friendlier to unification. Moreover, separate definitions allow the use of `@[simps]` to generate lemmas in which type casts are automatically removed. Prerequisite of #15681, where we deal with cubes, which are products of copies of the unit interval, for the purpose of showing commutativity of homotopy groups.