-- Mathlib/Geometry/Euclidean/Sphere/Power.lean
theorem mul_dist_eq_abs_sub_sq_dist {a b p q : P} (hp : ∃ k : ℝ, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p))
    (hq : dist a q = dist b q) : dist a p * dist b p = |dist b q ^ 2 - dist p q ^ 2|

Proof state:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ ‖a -ᵥ p‖ * ‖b -ᵥ p‖ = |‖b -ᵥ q‖ ^ 2 - ‖p -ᵥ q‖ ^ 2|

Tactic:
rw [← h1, ← h2, h, h]

Result:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ ‖m -ᵥ p - (m -ᵥ a)‖ * ‖m -ᵥ p + (m -ᵥ a)‖ = |‖m -ᵥ q + (m -ᵥ a)‖ ^ 2 - ‖m -ᵥ q - (m -ᵥ p)‖ ^ 2|

Proof state:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ ‖m -ᵥ p - (m -ᵥ a)‖ * ‖m -ᵥ p + (m -ᵥ a)‖ = |‖m -ᵥ q + (m -ᵥ a)‖ ^ 2 - ‖m -ᵥ q - (m -ᵥ p)‖ ^ 2|

Tactic:
rw [← h1, h] at hp

Result:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
hq : dist a q = dist b q
m : P := midpoint ℝ a b
hp : ∃ k, k ≠ 1 ∧ m -ᵥ p + (m -ᵥ a) = k • (m -ᵥ p - (m -ᵥ a))
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ ‖m -ᵥ p - (m -ᵥ a)‖ * ‖m -ᵥ p + (m -ᵥ a)‖ = |‖m -ᵥ q + (m -ᵥ a)‖ ^ 2 - ‖m -ᵥ q - (m -ᵥ p)‖ ^ 2|

Proof state:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)
hq : dist a q = dist b q
⊢ dist a p * dist b p = |dist b q ^ 2 - dist p q ^ 2|

Tactic:
let m : P := midpoint ℝ a b

Result:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)
hq : dist a q = dist b q
m : P := midpoint ℝ a b
⊢ dist a p * dist b p = |dist b q ^ 2 - dist p q ^ 2|

Proof state:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ dist a p * dist b p = |dist b q ^ 2 - dist p q ^ 2|

Tactic:
iterate 4 rw [dist_eq_norm_vsub V]

Result:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ ‖a -ᵥ p‖ * ‖b -ᵥ p‖ = |‖b -ᵥ q‖ ^ 2 - ‖p -ᵥ q‖ ^ 2|

Proof state:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
m : P := midpoint ℝ a b
hq : ‖m -ᵥ q - (m -ᵥ a)‖ = ‖m -ᵥ q + (m -ᵥ a)‖
hp : ∃ k, k ≠ 1 ∧ m -ᵥ p + (m -ᵥ a) = k • (m -ᵥ p - (m -ᵥ a))
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ ‖m -ᵥ p - (m -ᵥ a)‖ * ‖m -ᵥ p + (m -ᵥ a)‖ = |‖m -ᵥ q + (m -ᵥ a)‖ ^ 2 - ‖m -ᵥ q - (m -ᵥ p)‖ ^ 2|

Tactic:
exact mul_norm_eq_abs_sub_sq_norm hp hq

Result:
no goals

Proof state:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ ‖a -ᵥ p‖ * ‖b -ᵥ p‖ = |‖b -ᵥ q‖ ^ 2 - dist p q ^ 2|

Tactic:
rw [dist_eq_norm_vsub V]

Result:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ ‖a -ᵥ p‖ * ‖b -ᵥ p‖ = |‖b -ᵥ q‖ ^ 2 - ‖p -ᵥ q‖ ^ 2|

Proof state:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
hq : dist a q = dist b q
m : P := midpoint ℝ a b
hp : ∃ k, k ≠ 1 ∧ m -ᵥ p + (m -ᵥ a) = k • (m -ᵥ p - (m -ᵥ a))
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ ‖m -ᵥ p - (m -ᵥ a)‖ * ‖m -ᵥ p + (m -ᵥ a)‖ = |‖m -ᵥ q + (m -ᵥ a)‖ ^ 2 - ‖m -ᵥ q - (m -ᵥ p)‖ ^ 2|

Tactic:
rw [dist_eq_norm_vsub V a q, dist_eq_norm_vsub V b q, ← h3, h] at hq

Result:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
m : P := midpoint ℝ a b
hq : ‖m -ᵥ q - (m -ᵥ a)‖ = ‖m -ᵥ q + (m -ᵥ a)‖
hp : ∃ k, k ≠ 1 ∧ m -ᵥ p + (m -ᵥ a) = k • (m -ᵥ p - (m -ᵥ a))
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ ‖m -ᵥ p - (m -ᵥ a)‖ * ‖m -ᵥ p + (m -ᵥ a)‖ = |‖m -ᵥ q + (m -ᵥ a)‖ ^ 2 - ‖m -ᵥ q - (m -ᵥ p)‖ ^ 2|

Proof state:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
⊢ dist a p * dist b p = |dist b q ^ 2 - dist p q ^ 2|

Tactic:
have h : ∀ r, b -ᵥ r = m -ᵥ r + (m -ᵥ a) := fun r => by
  rw [midpoint_vsub_left, ← right_vsub_midpoint, add_comm, vsub_add_vsub_cancel]

Result:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
h : ∀ (r : P), b -ᵥ r = m -ᵥ r + (m -ᵥ a)
⊢ dist a p * dist b p = |dist b q ^ 2 - dist p q ^ 2|

Proof state:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b p q : P
hp : ∃ k, k ≠ 1 ∧ b -ᵥ p = k • (a -ᵥ p)
hq : dist a q = dist b q
m : P := midpoint ℝ a b
h1 : m -ᵥ p - (m -ᵥ a) = a -ᵥ p
h2 : m -ᵥ q - (m -ᵥ p) = p -ᵥ q
h3 : m -ᵥ q - (m -ᵥ a) = a -ᵥ q
r : P
⊢ b -ᵥ r = m -ᵥ r + (m -ᵥ a)

Tactic:
rw [midpoint_vsub_left, ← right_vsub_midpoint, add_comm, vsub_add_vsub_cancel]

Result:
no goals