English
Under a setup with a bijection between the non-unit positions of sums/products, matching non-unit factors, the total products are equal: ∏_{x∈s} f x = ∏_{x∈t} g x, given the non-unit correspondence via i.
Русский
При условии биекции между позициями без единицы, согласование ненулевых факторов даёт равенство произведений: ∏_{x∈s} f x = ∏_{x∈t} g x при соответствующей биекции.
LaTeX
$$$\displaystyle \prod_{x \in s} f(x) = \prod_{x \in t} g(x)$ under the stated non-unit correspondence$$
Lean4
@[to_additive]
theorem prod_bij_ne_one {s : Finset ι} {t : Finset κ} {f : ι → M} {g : κ → M} (i : ∀ a ∈ s, f a ≠ 1 → κ)
(hi : ∀ a h₁ h₂, i a h₁ h₂ ∈ t) (i_inj : ∀ a₁ h₁₁ h₁₂ a₂ h₂₁ h₂₂, i a₁ h₁₁ h₁₂ = i a₂ h₂₁ h₂₂ → a₁ = a₂)
(i_surj : ∀ b ∈ t, g b ≠ 1 → ∃ a h₁ h₂, i a h₁ h₂ = b) (h : ∀ a h₁ h₂, f a = g (i a h₁ h₂)) :
∏ x ∈ s, f x = ∏ x ∈ t, g x := by
classical
calc
∏ x ∈ s, f x = ∏ x ∈ s with f x ≠ 1, f x := by rw [prod_filter_ne_one]
_ = ∏ x ∈ t with g x ≠ 1, g x :=
(prod_bij (fun a ha => i a (mem_filter.mp ha).1 <| by simpa using (mem_filter.mp ha).2) ?_ ?_ ?_ ?_)
_ = ∏ x ∈ t, g x := prod_filter_ne_one _
· grind
· solve_by_elim
· intro b hb
refine (mem_filter.mp hb).elim fun h₁ h₂ ↦ ?_
obtain ⟨a, ha₁, ha₂, eq⟩ := i_surj b h₁ fun H ↦ by rw [H] at h₂; simp at h₂
exact ⟨a, mem_filter.mpr ⟨ha₁, ha₂⟩, eq⟩
· solve_by_elim
