The two expressions

y >> pure x
liftM (const x) y

have the same type signature in Haskell.
I was curious whether they were equivalent, but I could neither produce a proof of the fact nor a counter example against it.

If we rewrite the two expressions so that we can eliminate the x and y then the question becomes whether the two following functions are equivalent

flip (>>) . pure
liftM . const

Note that both these functions have type Monad m => a -> m b -> m a.

I used the laws that Haskell gives for monad, applicatives, and functors to transform both statements into various equivalent forms, but I was not able to produce a sequence of equivalences between the two.

For instance I found that y >> pure x can be rewritten as follows

y >>= const (pure x)
y *> pure x
(id <$ y) <*> pure x
fmap (const id) y <*> pure x

and liftM (const x) y can be rewritten as follows

fmap (const x) y
pure (const x) <*> y

None of these spring out to me as necessarily equivalent, but I cannot think of any cases where they would not be equivalent.

Yes they are the same

Let's start with flip (>>) . pure, which is the pointfree version of x >> pure y you provide:

flip (>>) . pure

It is the case that flip (>>) is just (=<<) . const so we can rewrite this as:

((=<<) . const) . pure

Since function composition ((.)) is associative we can write this as:

(=<<) . (const . pure)

We can rewrite const . pure as fmap pure . const:

(=<<) . (fmap pure . const)

Now we associate again:

((=<<) . fmap pure) . const

Since (=<<) has type

(=<<) :: Monad m => (a -> m b) -> m a -> m b

we know fmap pure must be a subtype of Monad m => c -> (a -> m b). If we unify this with it's type of

fmap pure :: (Applicative f1, Functor f2) => f2 a -> f2 (f1 a)

We get Monad m => (a -> b) -> (a -> m b). Meaning our functor is (a ->). Since (.) is fmap over the functor (a ->) we can replace our fmap with (.).

((=<<) . (.) pure) . const

((=<<) . (.) pure) is the definition for liftM¹ so we can substitute:

liftM . const

And that is the goal. The two are the same.

^{1: The definition of liftM is liftM f m1 = do x1 <- m1; return (f x1) , we can desugar the do into liftM f m1 = m1 >>= return . f. We can flip the (>>=) for liftM f m1 = return . f =<< m1 and elide the m1 to get liftM f = (return . f =<<) a little pointfree magic and we get liftM = (=<<) . (.) return}

The other answer gets there eventually, but it takes a long-winded route. All that is actually needed are the definitions of liftM, const, and a single monad law: m1 >> m2 and m1 >>= _ -> m2 must be semantically identical. (Indeed, this is the default implementation of (>>), and it is rare to override it.) Then:

liftM (const x) y
= definition of liftM* 
y >>= z -> pure (const x z)
= definition of const 
y >>= z -> pure x
= monad law 
y >> pure x

* Okay, okay, so the actual definition of liftM uses return instead of pure. Whatever.

One more possible route:

For instance I found that y >> pure x can be rewritten as follows [...]

fmap (const id) y <*> pure x

That amounts to...

fmap (const id) y <*> pure x
pure ($ x) <*> fmap (const id) y -- interchange law of applicatives
($ x) <$> fmap (const id) y -- fmap in terms of <*>
fmap (($ x) . const id) y -- composition law of functors
fmap (const x) y

... which, as you noted, is the same as liftM (const x) y.