# Zulip Chat Archive

## 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