Zulip Chat Archive

Stream: new members

Topic: logic manipulation


view this post on Zulip Michael Beeson (Oct 06 2020 at 03:38):

h93:  (y : M), y  b  y  z  ¬y  z
h94: (( (z_1 : M), z_1  z  z_1  b)   (x : M), x  b  x  z  b - z)  z  FINITE M
 z  FINITE M

So what is the "easy" way to substitute a new variable, say t, for z_1 and x and get on with it from there? as I would
do with 'cases' if it were a positive existential; here it's a negative universal and I do not know the right command.

view this post on Zulip Kyle Miller (Oct 06 2020 at 04:04):

It's a bit hard to understand your question -- it can be very helpful having a minimal working example (#mwe), for example as an example. Here's an approximation, since I'm not sure what all your types are, along with some tactics that might be helpful in this context:

example (M : Type*) (b z : set M) (FINITE : Type*  set (set M))
  (h93:  (y : M), y  b  y  z  ¬y  z)
  (h94: (( (z_1 : M), z_1  z  z_1  b)   (x : M), x  b  x  z  b \ z)  z  FINITE M)
  : (z  FINITE M) :=
begin
  apply h94,
  split,
  intros t ht,
  specialize h93 t,

end

view this post on Zulip Michael Beeson (Oct 06 2020 at 04:18):

Thank you, Kyle, "apply" was the thing I didn't know. I've written something like 14000 lines of Lean proofs and never once used "apply" because I don't know about it. Now I'll learn it. Also, thanks for demonstrating how I could have made a MWE out of this few lines. I didn't think it was possible.


Last updated: May 10 2021 at 00:31 UTC