# Zulip Chat Archive

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

#### Patrick Massot (Aug 16 2021 at 08:23):

`tauto`

#### Patrick Massot (Aug 16 2021 at 08:23):

`hint`

#### Patrick Massot (Aug 16 2021 at 08:23):

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

Thanks!

Last updated: Dec 20 2023 at 11:08 UTC