Rewriting under the scope of a series of quantifiers

Stream: new members

[Stuart Presnell]

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]

Try simp_rw only [L] at h

[Stuart Presnell]

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

[Stuart Presnell]

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

[Stuart Presnell]

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]

tauto

[Patrick Massot]

hint

[Patrick Massot]

#backticks

[Stuart Presnell]

Thanks!