English
A simplified variant of the previous contraction identity in a group setting; expresses the same relationship in a form suitable for simp-based proofs.
Русский
Упрощённый вариант предшествующей тождественности свёртки в группе; выражает ту же зависимость в форме, удобной для доказательств через simp.
LaTeX
$$$$\\text{(same contraction relation in a simplified form).}$$$$
Lean4
@[to_additive]
theorem partialProd_contractNth {G : Type*} [Monoid G] {n : ℕ} (g : Fin (n + 1) → G) (a : Fin (n + 1)) :
partialProd (contractNth a (· * ·) g) = partialProd g ∘ a.succ.succAbove :=
by
ext i
refine inductionOn i ?_ ?_
· simp only [partialProd_zero, Function.comp_apply, succ_succAbove_zero]
· intro i hi
simp only [Function.comp_apply, succ_succAbove_succ] at *
rw [partialProd_succ, partialProd_succ, hi]
rcases lt_trichotomy (i : ℕ) a with (h | h | h)
·
rw [succAbove_of_castSucc_lt, contractNth_apply_of_lt _ _ _ _ h, succAbove_of_castSucc_lt] <;>
simp only [lt_def, coe_castSucc, val_succ] <;>
omega
·
rw [succAbove_of_castSucc_lt, contractNth_apply_of_eq _ _ _ _ h, succAbove_of_le_castSucc, castSucc_fin_succ,
partialProd_succ, mul_assoc] <;>
simp only [castSucc_lt_succ_iff, le_def, coe_castSucc] <;>
omega
·
rw [succAbove_of_le_castSucc, succAbove_of_le_castSucc, contractNth_apply_of_gt _ _ _ _ h, castSucc_fin_succ] <;>
simp only [le_def, val_succ, coe_castSucc] <;>
omega
