English
Applying the update to the inl branch and then evaluating at inl is the same as updating f after composing with inl and evaluating at inl: update f (inl i) x (inl j) = update (f ∘ inl) i x (inl j).
Русский
Применение обновления к ветке inl и последующая оценка в inl эквивалентны обновлению после композиции: update f (inl i) x (inl j) = update (f ∘ inl) i x (inl j).
LaTeX
$$$\operatorname{update} f (\mathrm{Sum.inl} i) x (\mathrm{Sum.inl} j) = \operatorname{update} (f \circ \mathrm{inl}) i x (\mathrm{Sum.inl} j)$$$
Lean4
@[simp]
theorem update_elim_inr [DecidableEq β] [DecidableEq (α ⊕ β)] {f : α → γ} {g : β → γ} {i : β} {x : γ} :
update (Sum.elim f g) (inr i) x = Sum.elim f (update g i x) :=
update_eq_iff.2 ⟨by simp, by simp +contextual⟩
