∀ (α : Type u_1) (β : Type u_2) [inst : LinearOrderedCommGroupWithZero α] [inst_1 : LinearOrderedCommGroupWithZero β]
  (a : WithZero (Lex (αˣ × βˣ))),
  (LinearOrderedCommGroupWithZero.fst α β) a =
    (MonoidWithZeroHom.fst α β) ((WithZero.map' ↑(ofLexMulEquiv (αˣ × βˣ))) a)