Syntax or built-in for negation introduction?

Stream: lean4

[Mark Wilhelm]

Is there any "rfl" type of statement or mathlib4 function that would finish this?

import Mathlib.Logic.Basic

inductive Sandwich where
  | egg : Sandwich
  | roast_beef : Sandwich
  | vegetable : Sandwich

open Sandwich

def f (a: Sandwich) : Sandwich :=
  match a with
  | egg => roast_beef
  | roast_beef => roast_beef
  | vegetable => egg

theorem one_f_is_not_beef :
  ¬ (
    ∀ (a: Sandwich),
    f a = roast_beef
  )
:=
  have h0: ¬ f vegetable = roast_beef :=
    sorry
  have h1: ∃ (z: Sandwich), ¬ f z = roast_beef :=
    Exists.intro vegetable h0
  not_forall_of_exists_not h1

[Arthur Paulino]

by simp only [f] can replace your sorry (not sure if this is what you asked for)

[Mark Wilhelm]

That works, thanks. Is there a short non-tactic way of doing this?