rw [Prod.mk_one_mul_mk_one] at h
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
x y : M
hxy : x * y ∈ s.toSubsemigroup
h :
  (x, 1) * (y, 1) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (x, 1) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (y, 1) z
⊢ (∃ z ∈ s.toSubsemigroup, Associated x z) ∧ ∃ z ∈ s.toSubsemigroup, Associated y z
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
s : Submonoid M
t : Submonoid N
x y : M
hxy : x * y ∈ s.toSubsemigroup
h :
  (x * y, 1) ∈ (prod s t).toSubsemigroup →
    (∃ z ∈ (prod s t).toSubsemigroup, Associated (x, 1) z) ∧ ∃ z ∈ (prod s t).toSubsemigroup, Associated (y, 1) z
⊢ (∃ z ∈ s.toSubsemigroup, Associated x z) ∧ ∃ z ∈ s.toSubsemigroup, Associated y z