English
A specialized symmetric statement: (update f (inr i) x)(inr j) equals (update (λ t, f (inr t)) i x)(inr j).
Русский
Аналогичное симметричное утверждение: (update f (inr i) x)(inr j) = (update (λ t, f (inr t)) i x)(inr j).
LaTeX
$$$$ (\\operatorname{update} f (\\mathrm{inr} i)\\; x)(\\mathrm{inr} j) = (\\operatorname{update} (\\lambda t \\mapsto f(\\mathrm{inr} t)) i\\; x)(\\mathrm{inr} j). $$$$
Lean4
@[simp]
theorem update_inr_apply_inr' {γ : α ⊕ β → Type*} [DecidableEq β] [DecidableEq (α ⊕ β)] {f : (i : α ⊕ β) → γ i} {i : β}
{x : γ (.inr i)} (j : β) : update f (.inr i) x (Sum.inr j) = update (fun j ↦ f (.inr j)) i x j :=
Function.update_apply_of_injective f Sum.inr_injective i x j
