no goals
G✝ : Type ?u.56742
P✝ : Type ?u.56745
inst✝³ : AddGroup G✝
inst✝² : AddTorsor G✝ P✝
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
h : Injective bit0
y x₁ x₂ : P
hy : ↑(pointReflection x₁) y = ↑(pointReflection x₂) y
⊢ x₁ = x₂
rwa [pointReflection_apply, pointReflection_apply, vadd_eq_vadd_iff_sub_eq_vsub,
  vsub_sub_vsub_cancel_right, ← neg_vsub_eq_vsub_rev, neg_eq_iff_add_eq_zero, ← bit0, ← bit0_zero,
  h.eq_iff, vsub_eq_zero_iff_eq] at hy