Commit 2026-08-21 01:13 67c055d7

chore: deduplicate Set.pairwise_iff_of_refl and add aliases (#42807) Std.Refl.set_pairwise_iff was a duplicate (albeit in an earlier file), but this is better in the Set namespace rather than Std.Refl. There was an alias for Set.pairwise_iff_of_refl in the forward direction called Set.Pairwise.of_refl. which I thought was a terrible name, because it sounds like it's proving Set.Pairwise (i.e., the reverse direction), but instead it was actually using that for dot notation. I renamed the forward direction to forall₂, and the reverse to of_forall₂ (but do it manually to remove the Std.Refl hypothesis).