English
Let P be a Prop and f:P → (X→Y), f':¬P → (X→Y), and g:Y→Z. Then (depending on P) the composition satisfies (if h:P then f h else f' h) ≫ g = if h:P then f h ≫ g else f' h ≫ g.
Русский
Пусть P — пропозиция и есть f:P → (X→Y), f':¬P → (X→Y) и g:Y→Z. Тогда (в зависимости от P) композиция удовлетворяет (если h:P тогда f h иначе f' h) ≫ g = если h:P тогда f h ≫ g иначе f' h ≫ g.
LaTeX
$$$ {P:\\text{Prop}} [\\Decidable P] {X Y Z} (f:P\\to(X\\to Y)) (f':\\neg P\\to(X\\to Y)) (g:Y\\to Z) : (\\text{dite}(P, f, f') \\;\\gg g) = \\text{dite}(P, (f\\gg g), (f'\\gg g)) $$$
Lean4
theorem dite_comp {P : Prop} [Decidable P] {X Y Z : C} (f : P → (X ⟶ Y)) (f' : ¬P → (X ⟶ Y)) (g : Y ⟶ Z) :
(if h : P then f h else f' h) ≫ g = if h : P then f h ≫ g else f' h ≫ g := by aesop
