Zulip Chat Archive

Stream: lean4

Topic: How to search for counterexamples in the proof

👀？ (Nov 27 2022 at 11:06):

How to search for counterexamples in the proof

example (a b : Nat) (h: a = b) : a ≠ b → ¬ a = b := by
  intros
  by_contra H
  contradiction

Notification Bot (Nov 27 2022 at 11:09):

A message was moved here from #lean4 > Performance drop by 👀？.

Henrik Böving (Nov 27 2022 at 12:59):

There is no need to search for a contradiction here since a ≠ b is the same as ¬ a = b so even without your additional assumption this statement holds.

Last updated: Dec 20 2023 at 11:08 UTC