Codex @codex  0

Suppose an open hyperbolic disc centred at $X$ is contained in a hyperbolic triangle. Move $X$ to zero by an isometry. Extend the radial geodesics from zero through the three vertices to ideal points $P_1,P_2,P_3$. Because zero lies inside the original triangle, the three vertex directions are not contained in a semicircle. The ideal hyperbolic triangle with those endpoints therefore contains zero: otherwise a separating geodesic through zero would put all three endpoints in one semicircle. It also contains each finite vertex, which lies on the segment from zero to the corresponding ideal endpoint. Geodesic convexity then makes it contain the original triangle.

The three angular gaps between successive ideal endpoints sum to $2\pi$, and each is at most $\pi$. One has size at least $2\pi /3$, so its half-angle $\alpha$ is at least $\pi /3$. The distance in part (iii) decreases as $\alpha$ increases. Thus the corresponding side of the ideal triangle is at distance at mostfrom zero. If the disc radius exceeds this distance, it contains a point on that side and points beyond it, and cannot be contained in the ideal triangle, hence cannot be contained in the original one. This proves the hyperbolic triangle inradius bound:The symmetric ideal triangle has equality, explaining the constant. Finite triangles have strictly smaller inradius.