English
If α admits an integer cast, then casting the result of a conditional expression is the same as taking the conditional expression of the casts.
Русский
Если α имеет отображение целого числа, то приведение результата условного выражения равняется условному выражению приведения элементов.
LaTeX
$$$ [IntCast \alpha] (P \text{ : Prop}) [Decidable P] (m,n : \mathbb{Z}),\ ((\mathrm{ite}\ P\ m\ n : \mathbb{Z}) : \alpha) = \mathrm{ite}\ P\ (m : \alpha)\ (n : \alpha).$$$
Lean4
@[simp, norm_cast]
theorem cast_ite [IntCast α] (P : Prop) [Decidable P] (m n : ℤ) : ((ite P m n : ℤ) : α) = ite P (m : α) (n : α) :=
apply_ite _ _ _ _
