English
Let f' be a three-argument family f' i x y with f'i 1 1 = 1. Then f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j for all i,x,y,j.
Русский
Пусть f' — тройное отображение f'i x y с условием f'i 1 1 = 1. Тогда для всех i, x, y, j выполняется f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j.
LaTeX
$$$\forall (f' : \forall i, M i \to N i \to O i), (\forall i, f' i 1 1 = 1) \to \forall i (x : M i) (y : N i) (j : ι),\; f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j$$$
Lean4
@[to_additive apply_single₂]
theorem apply_mulSingle₂ (f' : ∀ i, M i → N i → O i) (hf' : ∀ i, f' i 1 1 = 1) (i : ι) (x : M i) (y : N i) (j : ι) :
f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j :=
by
by_cases h : j = i
· subst h
simp only [mulSingle_eq_same]
· simp only [mulSingle_eq_of_ne h, hf']
