English
If two lists l1 and l2 have equal products and all their elements are prime, then l1 and l2 are permutations of each other.
Русский
Если два списка l1 и l2 имеют равные произведения и все их элементы — простые, то эти списки — перестановки друг друга.
LaTeX
$$$\forall {l_1 l_2 : List M}, l_1.prod = l_2.prod \rightarrow (\forall p \in l_1, Prime p) \rightarrow (\forall p \in l_2, Prime p) \rightarrow l_1.Perm l_2$$$
Lean4
theorem perm_of_prod_eq_prod :
∀ {l₁ l₂ : List M}, l₁.prod = l₂.prod → (∀ p ∈ l₁, Prime p) → (∀ p ∈ l₂, Prime p) → Perm l₁ l₂
| [], [], _, _, _ => Perm.nil
| [], a :: l, h₁, _, h₃ =>
have ha : a ∣ 1 := prod_nil (M := M) ▸ h₁.symm ▸ (prod_cons (l := l)).symm ▸ dvd_mul_right _ _
absurd ha (Prime.not_dvd_one (h₃ a mem_cons_self))
| a :: l, [], h₁, h₂, _ =>
have ha : a ∣ 1 := prod_nil (M := M) ▸ h₁ ▸ (prod_cons (l := l)).symm ▸ dvd_mul_right _ _
absurd ha (Prime.not_dvd_one (h₂ a mem_cons_self))
| a :: l₁, b :: l₂, h, hl₁, hl₂ => by
classical
have hl₁' : ∀ p ∈ l₁, Prime p := fun p hp => hl₁ p (mem_cons_of_mem _ hp)
have hl₂' : ∀ p ∈ (b :: l₂).erase a, Prime p := fun p hp => hl₂ p (mem_of_mem_erase hp)
have ha : a ∈ b :: l₂ :=
mem_list_primes_of_dvd_prod (hl₁ a mem_cons_self) hl₂ (h ▸ by rw [prod_cons]; exact dvd_mul_right _ _)
have hb : b :: l₂ ~ a :: (b :: l₂).erase a := perm_cons_erase ha
have hl : prod l₁ = prod ((b :: l₂).erase a) :=
(mul_right_inj' (hl₁ a mem_cons_self).ne_zero).1 <| by rwa [← prod_cons, ← prod_cons, ← hb.prod_eq]
exact Perm.trans ((perm_of_prod_eq_prod hl hl₁' hl₂').cons _) hb.symm
