Stream: new members

Topic: Rewriting under the scope of a series of quantifiers

Stuart Presnell (Aug 12 2021 at 13:08):

If I have a hypothesis of the form h: ∀ a : X, ∃ b : X , P a b and a lemma L: ∀ a:X, ∀ b:X, P a b = Q a b, what's the quickest way to prove the goal ∀ a : X, ∃ b : X , Q a b? I know I can prove it by judicious use of intro, cases, use, and specialise, but is there a quicker way — for example, a version of rw?

Reid Barton (Aug 12 2021 at 13:10):

Try simp_rw only [L] at h

Stuart Presnell (Aug 12 2021 at 13:23):

Thanks! Lean wasn't happy with simp_rw only [L], but either of simp_rw [L] or simp only [L] work.

Stuart Presnell (Aug 12 2021 at 14:06):

Thanks again for this, you've saved me a lot of tedious work! :)

Stuart Presnell (Aug 16 2021 at 08:09):

As a follow-up to the above question: is there a quick way to prove the following?
example (X : Type*) (R : X → X → Prop) (P Q : X → Prop): (∀ x : X, P x → ∀ y : X, Q y → R x y) ↔ (∀ y : X, Q y → ∀ x : X, P x → R x y)

If the P x and Q y terms weren't there then forall_swap would work, but I couldn't find a theorem or a tactic that solves this (and library_search doesn't find anything).

tauto

hint

#backticks

Stuart Presnell (Aug 16 2021 at 08:39):

Thanks!

Last updated: Dec 20 2023 at 11:08 UTC