[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
inst✝² : OrderedCommMonoid α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : OrderedCommMonoid β
x y : Lex (α × β)
hxy✝ : x ≤ y
z : Lex (α × β)
hxy : x.fst = y.fst ∧ x.snd ≤ y.snd
⊢ (z.fst * x.fst, z.snd * x.snd).fst = (z.fst * y.fst, z.snd * y.snd).fst
[PROOFSTEP]
rw [hxy.1]
