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