English
For f : Fin n → M, the product of the first i elements of List.ofFn f equals the product over all j with j.val < i of f j.
Русский
Для f : Fin n → M произведение первых i элементов List.ofFn f равно произведению по всем j, таких что j.val < i, от f j.
LaTeX
$$$\\big(\\mathrm{List.ofFn} f\\big).take i .\\mathrm{prod} = \\prod_{j:\\mathrm{Fin} n, j.\\mathrm{val} < i} f(j)$$$
Lean4
@[to_additive]
theorem prod_take_ofFn {n : ℕ} (f : Fin n → M) (i : ℕ) : ((ofFn f).take i).prod = ∏ j with j.val < i, f j := by
induction i with
| zero => simp
| succ i IH =>
by_cases h : i < n
· have : i < length (ofFn f) := by rwa [length_ofFn]
rw [prod_take_succ _ _ this]
have A : ({j | j.val < i + 1} : Finset (Fin n)) = insert ⟨i, h⟩ ({j | Fin.val j < i} : Finset (Fin n)) :=
by
ext ⟨_, _⟩
simp [Nat.lt_succ_iff_lt_or_eq, or_comm]
rw [A, prod_insert (by simp), IH, mul_comm]
simp
· have A : (ofFn f).take i = (ofFn f).take i.succ :=
by
rw [← length_ofFn (f := f)] at h
have : length (ofFn f) ≤ i := not_lt.mp h
rw [take_of_length_le this, take_of_length_le (le_trans this (Nat.le_succ _))]
have B : ∀ j : Fin n, ((j : ℕ) < i.succ) = ((j : ℕ) < i) :=
by
intro j
have : (j : ℕ) < i := lt_of_lt_of_le j.2 (not_lt.mp h)
simp [this, lt_trans this (Nat.lt_succ_self _)]
simp [← A, B, IH]
