English
Given a triangle t and a point p with two vertices i1, i3 fixed, if twice the angle between t.points i1, p, t.points i3 equals twice the angle at t.points i1, i2, i3, then p lies on the circumsphere of t.
Русский
Для треугольника t и точки p, если удвоенный угол между точками t.points_{i1}, p, t.points_{i3} равен удвоенному углу между t.points_{i1}, t.points_{i2}, t.points_{i3}, то p лежит на circumsphere треугольника t.
LaTeX
$$$\\exists i_1,i_2,i_3 \\; (i_1,i_2,i_3\\text{ попарно различны}) \; \\text{и} \\ (2:ℤ)\\angle (t.points_{i_1}, p, t.points_{i_3}) = (2:ℤ)\\angle (t.points_{i_1}, t.points_{i_2}, t.points_{i_3}) \\Rightarrow p \\in t.circumsphere$$$
Lean4
/-- Given a triangle, and a fourth point such that twice the angle between two points of the
triangle at that fourth point equals twice the third angle of the triangle, the fourth point
lies in the circumsphere of the triangle. -/
theorem mem_circumsphere_of_two_zsmul_oangle_eq {t : Triangle ℝ P} {p : P} {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂)
(h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃)
(h : (2 : ℤ) • ∡ (t.points i₁) p (t.points i₃) = (2 : ℤ) • ∡ (t.points i₁) (t.points i₂) (t.points i₃)) :
p ∈ t.circumsphere := by
let t'p : Fin 3 → P := Function.update t.points i₂ p
have h₁ : t'p i₁ = t.points i₁ := by simp [t'p, h₁₂]
have h₂ : t'p i₂ = p := by simp [t'p]
have h₃ : t'p i₃ = t.points i₃ := by simp [t'p, h₂₃.symm]
have ha : AffineIndependent ℝ t'p :=
by
rw [affineIndependent_iff_not_collinear_of_ne h₁₂ h₁₃ h₂₃, h₁, h₂, h₃, collinear_iff_of_two_zsmul_oangle_eq h, ←
affineIndependent_iff_not_collinear_of_ne h₁₂ h₁₃ h₂₃]
exact t.independent
let t' : Triangle ℝ P := ⟨t'p, ha⟩
have h₁' : t'.points i₁ = t.points i₁ := h₁
have h₂' : t'.points i₂ = p := h₂
have h₃' : t'.points i₃ = t.points i₃ := h₃
have h' :
(2 : ℤ) • ∡ (t'.points i₁) (t'.points i₂) (t'.points i₃) = (2 : ℤ) • ∡ (t.points i₁) (t.points i₂) (t.points i₃) :=
by rwa [h₁', h₂', h₃']
rw [← circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq h₁₂ h₁₃ h₂₃ h₁' h₃' h', ← h₂']
exact Simplex.mem_circumsphere _ _
