Commit 2026-08-10 13:55 3f69b1ba

chore(Data/Finset/Prod): state singleton_product/product_singleton via sectR/sectL (#42418) The embeddings in the statements of Finset.singleton_product and Finset.product_singleton are Function.Embedding.sectR/sectL written out as anonymous constructors. Restate them via the named embeddings (the statements are definitionally unchanged), so call sites can rewrite with the sectR_apply/sectL_apply simp lemmas instead of Embedding.coeFn_mk. Update the two call sites that did the latter, and golf singleton_product_singleton, which is now rfl. Preparation for a follow-up PR replacing the aesop proofs of the {Icc,Ico,Ioc,Ioo,uIcc}_map_{sectL,sectR} lemmas in Order/Interval/Finset/Basic.