[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
g1 g2 : G
p : P
h : g1 +ᵥ p = g2 +ᵥ p
⊢ g1 = g2
[PROOFSTEP]
rw [← vadd_vsub g1 p, h, vadd_vsub]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
g : G
p1 p2 : P
⊢ g +ᵥ p1 -ᵥ p2 = g + (p1 -ᵥ p2)
[PROOFSTEP]
apply vadd_right_cancel p2
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
g : G
p1 p2 : P
⊢ g +ᵥ p1 -ᵥ p2 +ᵥ p2 = g + (p1 -ᵥ p2) +ᵥ p2
[PROOFSTEP]
rw [vsub_vadd, add_vadd, vsub_vadd]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p : P
⊢ p -ᵥ p = 0
[PROOFSTEP]
rw [← zero_add (p -ᵥ p), ← vadd_vsub_assoc, vadd_vsub]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 : P
h : p1 -ᵥ p2 = 0
⊢ p1 = p2
[PROOFSTEP]
rw [← vsub_vadd p1 p2, h, zero_vadd]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 p3 : P
⊢ p1 -ᵥ p2 + (p2 -ᵥ p3) = p1 -ᵥ p3
[PROOFSTEP]
apply vadd_right_cancel p3
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 p3 : P
⊢ p1 -ᵥ p2 + (p2 -ᵥ p3) +ᵥ p3 = p1 -ᵥ p3 +ᵥ p3
[PROOFSTEP]
rw [add_vadd, vsub_vadd, vsub_vadd, vsub_vadd]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 : P
⊢ -(p1 -ᵥ p2) = p2 -ᵥ p1
[PROOFSTEP]
refine' neg_eq_of_add_eq_zero_right (vadd_right_cancel p1 _)
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 : P
⊢ p1 -ᵥ p2 + (p2 -ᵥ p1) +ᵥ p1 = 0 +ᵥ p1
[PROOFSTEP]
rw [vsub_add_vsub_cancel, vsub_self]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
g : G
p q : P
⊢ g +ᵥ p -ᵥ q = g - (q -ᵥ p)
[PROOFSTEP]
rw [vadd_vsub_assoc, sub_eq_add_neg, neg_vsub_eq_vsub_rev]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 : P
g : G
⊢ p1 -ᵥ (g +ᵥ p2) = p1 -ᵥ p2 - g
[PROOFSTEP]
rw [← add_right_inj (p2 -ᵥ p1 : G), vsub_add_vsub_cancel, ← neg_vsub_eq_vsub_rev, vadd_vsub, ← add_sub_assoc, ←
  neg_vsub_eq_vsub_rev, neg_add_self, zero_sub]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 p3 : P
⊢ p1 -ᵥ p3 - (p2 -ᵥ p3) = p1 -ᵥ p2
[PROOFSTEP]
rw [← vsub_vadd_eq_vsub_sub, vsub_vadd]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ -v₁ + v₂ = p₁ -ᵥ p₂
[PROOFSTEP]
rw [eq_vadd_iff_vsub_eq, vadd_vsub_assoc, ← add_right_inj (-v₁), neg_add_cancel_left, eq_comm]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p : P
⊢ {p} -ᵥ {p} = {0}
[PROOFSTEP]
rw [Set.singleton_vsub_singleton, vsub_self]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
v₁ v₂ : G
p : P
⊢ v₁ +ᵥ p -ᵥ (v₂ +ᵥ p) = v₁ - v₂
[PROOFSTEP]
rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, vsub_self, add_zero]
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 p : P
h : p1 -ᵥ p = p2 -ᵥ p
⊢ p1 = p2
[PROOFSTEP]
rwa [← sub_eq_zero, vsub_sub_vsub_cancel_right, vsub_eq_zero_iff_eq] at h 
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 p : P
h : p -ᵥ p1 = p -ᵥ p2
⊢ p1 = p2
[PROOFSTEP]
refine' vadd_left_cancel (p -ᵥ p2) _
[GOAL]
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p1 p2 p : P
h : p -ᵥ p1 = p -ᵥ p2
⊢ p -ᵥ p2 +ᵥ p1 = p -ᵥ p2 +ᵥ p2
[PROOFSTEP]
rw [vsub_vadd, ← h, vsub_vadd]
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
p1 p2 p3 : P
⊢ p3 -ᵥ p2 - (p3 -ᵥ p1) = p1 -ᵥ p2
[PROOFSTEP]
rw [sub_eq_add_neg, neg_vsub_eq_vsub_rev, add_comm, vsub_add_vsub_cancel]
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
v : G
p1 p2 : P
⊢ v +ᵥ p1 -ᵥ (v +ᵥ p2) = p1 -ᵥ p2
[PROOFSTEP]
rw [vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_sub_cancel']
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
p1 p2 p3 : P
⊢ p1 -ᵥ p2 +ᵥ p3 = p3 -ᵥ p2 +ᵥ p1
[PROOFSTEP]
rw [← @vsub_eq_zero_iff_eq G, vadd_vsub_assoc, vsub_vadd_eq_vsub_sub]
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
p1 p2 p3 : P
⊢ p1 -ᵥ p2 + (p3 -ᵥ p1 - (p3 -ᵥ p2)) = 0
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
v₁ v₂ : G
p₁ p₂ : P
⊢ v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ v₂ - v₁ = p₁ -ᵥ p₂
[PROOFSTEP]
rw [vadd_eq_vadd_iff_neg_add_eq_vsub, neg_add_eq_sub]
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
p₁ p₂ p₃ p₄ : P
⊢ p₁ -ᵥ p₂ - (p₃ -ᵥ p₄) = p₁ -ᵥ p₃ - (p₂ -ᵥ p₄)
[PROOFSTEP]
rw [← vsub_vadd_eq_vsub_sub, vsub_vadd_comm, vsub_vadd_eq_vsub_sub]
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
p p' : P
⊢ (fun v => -v +ᵥ p) ((fun x x_1 => x -ᵥ x_1) p p') = p'
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
p : P
v : G
⊢ (fun x x_1 => x -ᵥ x_1) p ((fun v => -v +ᵥ p) v) = v
[PROOFSTEP]
simp [vsub_vadd_eq_vsub_sub]
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
v : G
p : P
⊢ (fun x x_1 => x +ᵥ x_1) (-v) ((fun x x_1 => x +ᵥ x_1) v p) = p
[PROOFSTEP]
simp [vadd_vadd]
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
v : G
p : P
⊢ (fun x x_1 => x +ᵥ x_1) v ((fun x x_1 => x +ᵥ x_1) (-v) p) = p
[PROOFSTEP]
simp [vadd_vadd]
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
x y : P
⊢ -(x -ᵥ ↑(pointReflection x) y) = -(y -ᵥ x)
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
x y : P
⊢ ↑(pointReflection x) y -ᵥ y = 2 • (x -ᵥ y)
[PROOFSTEP]
simp [pointReflection, two_nsmul, vadd_vsub_assoc]
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
x y : P
⊢ -(y -ᵥ ↑(pointReflection x) y) = -(2 • (y -ᵥ x))
[PROOFSTEP]
simp [← neg_nsmul]
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
x : P
⊢ ∀ (x_1 : P), ↑(pointReflection x).symm x_1 = ↑(pointReflection x) x_1
[PROOFSTEP]
simp [pointReflection]
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
x y : P
⊢ ↑(pointReflection x) y = ↑(pointReflection x).symm y
[PROOFSTEP]
rw [pointReflection_symm]
[GOAL]
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
[PROOFSTEP]
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]
[GOAL]
G✝ : Type u_1
P✝ : Type u_2
inst✝³ : AddGroup G✝
inst✝² : AddTorsor G✝ P✝
G : Type u_3
P : Type u_4
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
h : Injective bit0
y x₁ x₂ : P
hy : ↑(pointReflection x₁) y = ↑(pointReflection x₂) y
⊢ x₁ = x₂
[PROOFSTEP]
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 
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
⊢ Subsingleton G ↔ Subsingleton P
[PROOFSTEP]
inhabit P
[GOAL]
G : Type u_1
P : Type u_2
inst✝¹ : AddGroup G
inst✝ : AddTorsor G P
inhabited_h : Inhabited P
⊢ Subsingleton G ↔ Subsingleton P
[PROOFSTEP]
exact (Equiv.vaddConst default).subsingleton_congr
