English
If two oriented triangles t1 and t2 share two corresponding vertices and twice the angle at the third vertex agrees between the two triangles, then their circumspheres coincide.
Русский
Если два треугольника t1 и t2 имеют по две вершины совпадающими соответственно и вторая пара углов на третьей вершине относится одинаково вдвое между двумя треугольниками, то их описанные сферы совпадают.
LaTeX
$$$\\text{If } t_1,t_2\\text{ are triangles and } i_1,i_2,i_3\\in\\{0,1,2\\}, \n(i_1\\neq i_2), (i_1\\neq i_3), (i_2\\neq i_3), \nt_1.\\text{points}_{i_1} = t_2.\\text{points}_{i_1}, \; t_1.\\text{points}_{i_3} = t_2.\\text{points}_{i_3}, \n2\\angle(t_1.\\text{points}_{i_1}, t_1.\\textpoints_{i_2}, t_1.\\textpoints_{i_3}) = 2\\angle(t_2.\\textpoints_{i_1}, t_2.\\textpoints_{i_2}, t_2.\\textpoints_{i_3}) \\Rightarrow t_1.circumsphere = t_2.circumsphere$$$
Lean4
/-- If two triangles have two points the same, and twice the angle at the third point the same,
they have the same circumsphere. -/
theorem circumsphere_eq_circumsphere_of_eq_of_eq_of_two_zsmul_oangle_eq {t₁ t₂ : Triangle ℝ P} {i₁ i₂ i₃ : Fin 3}
(h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) (h₁ : t₁.points i₁ = t₂.points i₁)
(h₃ : t₁.points i₃ = t₂.points i₃)
(h₂ :
(2 : ℤ) • ∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃) =
(2 : ℤ) • ∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)) :
t₁.circumsphere = t₂.circumsphere := by
rw [t₁.circumsphere_eq_of_dist_of_oangle h₁₂ h₁₃ h₂₃, t₂.circumsphere_eq_of_dist_of_oangle h₁₂ h₁₃ h₂₃,
Real.Angle.tan_eq_of_two_zsmul_eq h₂, Real.Angle.abs_sin_eq_of_two_zsmul_eq h₂, h₁, h₃]
