English
Let (f_i) be a family of monoids and H a submonoid of the product ∏_i f_i. For a finite index set I ⊆ η, and x ∈ ∏_i f_i such that x_i = 1 for i ∉ I, and for every i ∈ I we have Pi.mulSingle i (x_i) ∈ H, then x ∈ H.
Русский
Пусть {f_i} — семейство моноидов, H — подпmoноид произведения ∏_i f_i. Пусть I ⊆ η конечно и x ∈ ∏_i f_i удовлетворяет x_i = 1 для i ∉ I, и для каждого i ∈ I выполняется Pi.mulSingle i (x_i) ∈ H. Тогда x ∈ H.
LaTeX
$$$\exists I \subseteq \eta\text{ finite},\ x \in \prod_i f_i\ ∧\ (\forall i \notin I\, x_i = 1) \ ∧\ (\forall i \in I\, \Pi.mulSingle i (x_i) \in H) \Rightarrow x \in H$$$
Lean4
@[to_additive]
theorem pi_mem_of_mulSingle_mem_aux [DecidableEq η] (I : Finset η) {H : S} (x : Π i, f i) (h1 : ∀ i, i ∉ I → x i = 1)
(h2 : ∀ i, i ∈ I → Pi.mulSingle i (x i) ∈ H) : x ∈ H := by
induction I using Finset.induction_on generalizing x with
| empty =>
have : x = 1 := funext fun i => h1 i (Finset.notMem_empty i)
exact this ▸ one_mem H
| insert i I hnotMem
ih =>
have : x = Function.update x i 1 * Pi.mulSingle i (x i) :=
by
ext j
by_cases heq : j = i
· subst heq
simp
· simp [heq]
rw [this]
clear this
apply mul_mem (ih _ _ _) (by simp [h2]) <;> clear ih <;> intro j hj
· by_cases heq : j = i
· subst heq
simp
· simpa [heq] using h1 j (by simpa [heq] using hj)
· have : j ≠ i := fun h => h ▸ hnotMem <| hj
simp only [ne_eq, this, not_false_eq_true, Function.update_of_ne]
exact h2 _ (Finset.mem_insert_of_mem hj)
