Stream: new members

Topic: logic manipulation

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.

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


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