stable_matching_of_all_women_top_choice

Read back from the Lean

For any two types $M$ and $W$, any market : MarriageMarket M W (providing preference relations pref_m : M → W → W → Prop and pref_w : W → M → M → Prop), and any bijection $\mu : M \simeq W$: If for every woman $w : W$ and every man $m : M$, it is not the case that $w$ prefers $m$ over her assigned partner $\mu^{-1}(w)$ (¬ market.pref_w w m (μ.symm w)), then for every man $m : M$ and woman $w : W$, it is not the case that both: 1. $m$ prefers $w$ over his assigned partner $\mu(m)$ (market.pref_m m w (μ m)), and 2. $w$ prefers $m$ over her assigned partner $\mu^{-1}(w)$ (market.pref_w w m (μ.symm w)).

Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.