English
In a lawful monad, mapping pure values through mOfFn is equivalent to pure ofFn: mOfFn (fun i => pure (f i)) = pure (ofFn f).
Русский
В правильной монадe отображение чистых значений через mOfFn эквивалентно чистому ofFn: mOfFn (λ i, pure (f i)) = pure (ofFn f).
LaTeX
$$$\\forall {m}\\ [\\mathrm{Monad}\\ m]\\ [\\mathrm{LawfulMonad}\\ m] {\\alpha} {n}, (\\forall f:\\mathrm{Fin} n \\to \\alpha),\\; \\mathrm{mOfFn}(\\lambda i. \\mathrm{pure}(f i)) = \\mathrm{pure}(\\mathrm{ofFn}(f))$$$
Lean4
theorem mOfFn_pure {m} [Monad m] [LawfulMonad m] {α} :
∀ {n} (f : Fin n → α), (@mOfFn m _ _ _ fun i => pure (f i)) = pure (ofFn f)
| 0, _ => rfl
| n + 1, f => by
rw [mOfFn, @mOfFn_pure m _ _ _ n _, ofFn]
simp
