## Stream: new members

### Topic: Arbitrary reordering under universal quantifier

#### Rish Vaishnav (Jan 31 2022 at 16:17):

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 (Jan 31 2022 at 16:39):

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]


Last updated: Dec 20 2023 at 11:08 UTC