English
For any c, with Decidable, and a,b in Ordering, the equality (if c then a else b) = Ordering.eq is equivalent to (if c then a = Ordering.eq else b = Ordering.eq).
Русский
Для любого c с разрешимостью, и a,b из Ordering, равенство (if c then a else b) = Ordering.eq эквивалентно (if c then a = Ordering.eq else b = Ordering.eq).
LaTeX
$$$\\forall c\\ (\\text{Decidable } c)\\ (a,b:\\text{Ordering}),\\ ((\\text{if } c\\text{ then } a\\text{ else } b) = \\text{Ordering.eq}) = \\text{if } c\\ then a = \\text{Ordering.eq} \\text{ else } b = \\text{Ordering.eq}$$$
Lean4
@[simp]
theorem ite_eq_eq_distrib (c : Prop) [Decidable c] (a b : Ordering) :
((if c then a else b) = Ordering.eq) = if c then a = Ordering.eq else b = Ordering.eq := by by_cases c <;> simp [*]
