no goals
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
x y : P
h : Injective bit0
⊢ ↑(pointReflection x) y = y ↔ y = x
rw [pointReflection_apply, eq_comm, eq_vadd_iff_vsub_eq, ← neg_vsub_eq_vsub_rev,
  neg_eq_iff_add_eq_zero, ← bit0, ← bit0_zero, h.eq_iff, vsub_eq_zero_iff_eq, eq_comm]