Arbitrary reordering under universal quantifier

Stream: new members

[Rish Vaishnav]

Is there an easy way to prove the following?

lemma test1 (X Y : Type*) (XS : set X) (YS : set Y) (f : Y → X)
  (h : ∀ (P : X → Prop), (∀ x ∈ XS, P x) ↔ (∀ y ∈ YS, P (f y))) (P : X → X → Prop)
  : (∀ x1 x2 (ha : x1 ∈ XS) (hb : x2 ∈ XS), P x1 x2) ↔ (∀ y1 y2 (ha : y1 ∈ YS) (hb : y2 ∈ YS), P (f y1) (f y2)) :=
  by sorry

If I simply reorder the hypotheses on both sides of the goal, simp_rw handles it:

lemma test2 (X Y : Type*) (XS : set X) (YS : set Y) (f : Y → X)
  (h : ∀ (P : X → Prop), (∀ x ∈ XS, P x) ↔ (∀ y ∈ YS, P (f y))) (P : X → X → Prop)
  : (∀ x1 (ha: x1 ∈ XS) x2 (hb : x2 ∈ XS), P x1 x2) ↔ (∀ y1 (ha : y1 ∈ YS) y2 (hb : y2 ∈ YS), P (f y1) (f y2)) :=
  by simp_rw h

[Patrick Johnson]

docs#ball_mem_comm

lemma test1 (X Y : Type*) (XS : set X) (YS : set Y) (f : Y → X)
  (h : ∀ (P : X → Prop), (∀ x ∈ XS, P x) ↔ (∀ y ∈ YS, P (f y))) (P : X → X → Prop)
  : (∀ x1 x2 (ha : x1 ∈ XS) (hb : x2 ∈ XS), P x1 x2) ↔ (∀ y1 y2 (ha : y1 ∈ YS) (hb : y2 ∈ YS), P (f y1) (f y2)) :=
by simp [ball_mem_comm.symm, h]