[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hx : x ≠ c
hy : y ≠ c
⊢ inversion c R x ∈ perpBisector c (inversion c R y) ↔ dist x y = dist y c
[PROOFSTEP]
rw [mem_perpBisector_iff_dist_eq, dist_inversion_inversion hx hy, dist_inversion_center]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hx : x ≠ c
hy : y ≠ c
⊢ R ^ 2 / dist x c = R ^ 2 / (dist x c * dist y c) * dist x y ↔ dist x y = dist y c
[PROOFSTEP]
have hx' := dist_ne_zero.2 hx
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hx : x ≠ c
hy : y ≠ c
hx' : dist x c ≠ 0
⊢ R ^ 2 / dist x c = R ^ 2 / (dist x c * dist y c) * dist x y ↔ dist x y = dist y c
[PROOFSTEP]
have hy' := dist_ne_zero.2 hy
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hx : x ≠ c
hy : y ≠ c
hx' : dist x c ≠ 0
hy' : dist y c ≠ 0
⊢ R ^ 2 / dist x c = R ^ 2 / (dist x c * dist y c) * dist x y ↔ dist x y = dist y c
[PROOFSTEP]
field_simp [mul_assoc, mul_comm, hx, hx.symm, eq_comm]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ inversion c R x ∈ perpBisector c (inversion c R y) ↔ dist x y = dist y c ∧ x ≠ c
[PROOFSTEP]
rcases eq_or_ne x c with rfl | hx
[GOAL]
case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ x
⊢ inversion x R x ∈ perpBisector x (inversion x R y) ↔ dist x y = dist y x ∧ x ≠ x
[PROOFSTEP]
simp [*]
[GOAL]
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
hx : x ≠ c
⊢ inversion c R x ∈ perpBisector c (inversion c R y) ↔ dist x y = dist y c ∧ x ≠ c
[PROOFSTEP]
simp [inversion_mem_perpBisector_inversion_iff hR hx hy, hx]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ inversion c R ⁻¹' ↑(perpBisector c y) = sphere (inversion c R y) (R ^ 2 / dist y c) \ {c}
[PROOFSTEP]
rw [← dist_inversion_center, ← preimage_inversion_perpBisector_inversion hR, inversion_inversion]
[GOAL]
case hR
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ R ≠ 0
[PROOFSTEP]
simp [*]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ inversion c R y ≠ c
[PROOFSTEP]
simp [*]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ inversion c R '' ↑(perpBisector c y) = sphere (inversion c R y) (R ^ 2 / dist y c) \ {c}
[PROOFSTEP]
rw [image_eq_preimage_of_inverse (inversion_involutive _ hR) (inversion_involutive _ hR),
  preimage_inversion_perpBisector hR hy]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ inversion c R ⁻¹' sphere y (dist y c) = insert c ↑(perpBisector c (inversion c R y))
[PROOFSTEP]
ext x
[GOAL]
case h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x✝ y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
x : P
⊢ x ∈ inversion c R ⁻¹' sphere y (dist y c) ↔ x ∈ insert c ↑(perpBisector c (inversion c R y))
[PROOFSTEP]
rcases eq_or_ne x c with rfl | hx
[GOAL]
case h.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
x✝ y : P
R : ℝ
hR : R ≠ 0
x : P
hy : y ≠ x
⊢ x ∈ inversion x R ⁻¹' sphere y (dist y x) ↔ x ∈ insert x ↑(perpBisector x (inversion x R y))
[PROOFSTEP]
simp [dist_comm]
[GOAL]
case h.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x✝ y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
x : P
hx : x ≠ c
⊢ x ∈ inversion c R ⁻¹' sphere y (dist y c) ↔ x ∈ insert c ↑(perpBisector c (inversion c R y))
[PROOFSTEP]
rw [mem_preimage, mem_sphere, ← inversion_mem_perpBisector_inversion_iff hR]
[GOAL]
case h.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x✝ y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
x : P
hx : x ≠ c
⊢ inversion c R (inversion c R x) ∈ perpBisector c (inversion c R y) ↔ x ∈ insert c ↑(perpBisector c (inversion c R y))
[PROOFSTEP]
simp [*]
[GOAL]
case h.inr.hx
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x✝ y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
x : P
hx : x ≠ c
⊢ inversion c R x ≠ c
[PROOFSTEP]
simp [*]
[GOAL]
case h.inr.hy
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x✝ y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
x : P
hx : x ≠ c
⊢ y ≠ c
[PROOFSTEP]
simp [*]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hR : R ≠ 0
hy : y ≠ c
⊢ inversion c R '' sphere y (dist y c) = insert c ↑(perpBisector c (inversion c R y))
[PROOFSTEP]
rw [image_eq_preimage_of_inverse (inversion_involutive _ hR) (inversion_involutive _ hR),
  preimage_inversion_sphere_dist_center hR hy]
