English
Same structure as PowerSet DiffElem for another instance.
Русский
Та же структура, что и ранее, для другого примера.
LaTeX
$$$\\dots$$$
Lean4
@[to_additive]
theorem mul_finprod_cond_ne (a : α) (hf : (mulSupport f).Finite) : (f a * ∏ᶠ (i) (_ : i ≠ a), f i) = ∏ᶠ i, f i := by
classical
rw [finprod_eq_prod _ hf]
have h : ∀ x : α, f x ≠ 1 → (x ≠ a ↔ x ∈ hf.toFinset \ { a }) :=
by
intro x hx
rw [Finset.mem_sdiff, Finset.mem_singleton, Finite.mem_toFinset, mem_mulSupport]
grind
rw [finprod_cond_eq_prod_of_cond_iff f (fun hx => h _ hx), Finset.sdiff_singleton_eq_erase]
by_cases ha : a ∈ mulSupport f
· apply Finset.mul_prod_erase _ _ ((Finite.mem_toFinset _).mpr ha)
· rw [mem_mulSupport, not_not] at ha
rw [ha, one_mul]
apply Finset.prod_erase _ ha
