Proving a "not for all" with an "exists" with Classical

Stream: lean4

[Mark Wilhelm]

I think I'm missing something obvious here, but what would be the cleanest way to finish this?

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

open Classical

theorem one_f_is_not_beef :
  ¬ (
    ∀ (a: Sandwich),
    f a = roast_beef
  )
:=
byContradiction (
  fun h0: ¬¬∀ (a : Sandwich), f a = roast_beef => sorry
)

[Chris B]

One way:

byContradiction (
  fun h0 =>
    have h1 : ¬∀ a, f a = roast_beef := fun hAll => Sandwich.noConfusion (hAll vegetable)
    absurd h1 h0
)

[Mark Wilhelm]

thanks, wrapping my head around this for a moment....

[Kevin Buzzard]

Just do it in tactic mode, do intro a and then cases a and then follow your nose

[Arthur Paulino]

This is kind of #xy, but this exercise has helped me many times in the past (thanks Kyle MIller!)

inductive Sandwich where
  | egg
  | roast_beef
  | vegetable
  deriving DecidableEq

open Sandwich

def f : Sandwich → Sandwich
  | egg        => roast_beef
  | roast_beef => roast_beef
  | vegetable  => egg

theorem not_forall_iff {α : Type} {p : α → Prop} :
  ¬(∀ i : α, p i) ↔ ∃ i : α, ¬ (p i) := sorry

theorem not_eq_iff {α : Type} {a a' : α} : ¬ (a = a') ↔ a ≠ a' := sorry

theorem one_f_is_not_beef : ¬ ( ∀ (a: Sandwich), f a = roast_beef ) := by
  rw [not_forall_iff]
  exact ⟨vegetable, by rw [not_eq_iff]; simp only [f]⟩