English
If a,b,c,d are cospherical and ∠a p b = π and ∠c p d = π, then dist(a,p)dist(b,p) = dist(c,p)dist(d,p).
Русский
Если кососферные точки a,b,c,d и углы ∠a p b = π, ∠c p d = π, то dist(a,p)dist(b,p) = dist(c,p)dist(d,p).
LaTeX
$$Cospherical({a,b,c,d}) ∧ ∠a p b = π ∧ ∠c p d = π ⇒ dist(a,p)dist(b,p) = dist(c,p)dist(d,p)$$
Lean4
/-- If `A`, `B`, `C`, `D` are cospherical and `P` is on both lines `AB` and `CD`, then
`AP * BP = CP * DP`. -/
theorem mul_dist_eq_mul_dist_of_cospherical {a b c d p : P} (h : Cospherical ({ a, b, c, d } : Set P))
(hapb : p ∈ line[ℝ, a, b]) (hcpd : p ∈ line[ℝ, c, d]) : dist a p * dist b p = dist c p * dist d p :=
by
obtain ⟨q, r, h'⟩ := (cospherical_def { a, b, c, d }).mp h
obtain ⟨ha, hb, hc, hd⟩ := h' a (by simp), h' b (by simp), h' c (by simp), h' d (by simp)
rw [← hd] at hc
rw [← hb] at ha
rw [mul_dist_eq_abs_sub_sq_dist hapb ha, hb, mul_dist_eq_abs_sub_sq_dist hcpd hc, hd]
