logic manipulation

Stream: new members

[Michael Beeson]

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]

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]

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.