Proving that two strings are different in Lean

As I was carrying out my normal course of lean theorem proving, I realized my current file was taking an awfully long time to compile. I then narrowed down the issue to the part where I was attempting to prove that two strings were distinct:

lemma L0 : "x" ≠ "y" :=
begin
  intros H, cases H
end

This little lemma alone will take 15 seconds to compile on my (albeit) slow machine. something is seriously wrong.

I am not a fluent Lean user so guessing I should not be using the cases tactic for string. What else can I do?

The corresponding lemma in Coq works fine without any timing issue:

Require Import String.

Open Scope string_scope.

Lemma L0 : "x" <> "y".
Proof.
    intros H. inversion H.
Qed.