English
Final formulation of the auxiliary identity for iterated derivatives, parameterized by a set and a bijection e, showing equality of two nested update operations.
Русский
Финальная формулировка вспомогательного равенства для итеративной производной, параметризованная множеством и биекцией e, показывающая равенство двух вложенных операций обновления.
LaTeX
$$$$ \text{iteratedFDeriv_aux}(s,e,m,a,z) = \text{iterated update expression with } e $$$$
Lean4
theorem iteratedFDeriv_aux {ι} {M₁ : ι → Type*} {α : Type*} [DecidableEq α] (s : Set ι) [DecidableEq { x // x ∈ s }]
(e : α ≃ s) (m : α → ((i : ι) → M₁ i)) (a : α) (z : (i : ι) → M₁ i) :
(fun i ↦ update m a z (e.symm i) i) = (fun i ↦ update (fun j ↦ m (e.symm j) j) (e a) (z (e a)) i) :=
by
ext i
rcases eq_or_ne a (e.symm i) with rfl | hne
· rw [Equiv.apply_symm_apply e i, update_self, update_self]
· rw [update_of_ne hne.symm, update_of_ne fun h ↦ (Equiv.symm_apply_apply .. ▸ h ▸ hne) rfl]
