no goals
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s : Set α
t : Set β
h : Bounded (s ×ˢ t)
hs : Set.Nonempty s
⊢ Bounded t
simpa only [snd_image_prod hs t] using (@LipschitzWith.prod_snd α β _ _).bounded_image h