[lozenge]

It is lean-verified, so it can be trusted unless the Lean statement of the hypothesis is not an accurate description of the hypothesis.