use タクティクを紹介する

[Seasawher]

exists では通らず、use が通るようなコード例を探したい

[Seasawher]

Zulip: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60use.60.20vs.20.60exists.60

[Seasawher]

Zulip で教えてもらえた．

inductive Exists3 {α β : Sort*} (p : α → β → Prop) : Prop
  | mk (x : α) (y : β) (h : p x y)

example : Exists3 (fun (x1 x2 : String) => x1 = x2) := by
  exists "hello" -- failure, insufficient number of arguments

example : Exists3 (fun (x1 x2 : String) => x1 = x2) := by
  use "hello"

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.E2.9C.94.20.60use.60.20vs.20.60exists.60/near/446414572