English
If two finite sets s1 and s2 are equal and two functions f,g coincide on s2, then the noncommutative product over s1 of f equals the noncommutative product over s2 of g, provided the commutativity condition holds for s1.
Русский
Если множества s1 и s2 совпадают, функции f и g совпадают на s2, и выполнено условие коммутативности, то некоммопрод по s1 от f равен некоммопродукту по s2 от g.
LaTeX
$$$ (s_1 = s_2) \to (\forall x \in s_2, f x = g x) \to (comm) \Rightarrow noncommProd s_1 f comm = noncommProd s_2 g (fun x hx y hy h => by ...)$$$
Lean4
@[to_additive (attr := congr)]
theorem noncommProd_congr {s₁ s₂ : Finset α} {f g : α → β} (h₁ : s₁ = s₂) (h₂ : ∀ x ∈ s₂, f x = g x) (comm) :
noncommProd s₁ f comm =
noncommProd s₂ g fun x hx y hy h => by
dsimp only [Function.onFun]
rw [← h₂ _ hx, ← h₂ _ hy]
subst h₁
exact comm hx hy h :=
by simp_rw [noncommProd, Multiset.map_congr (congr_arg _ h₁) h₂]
