English
If the product of cardinalities 1 < |A|·|B| holds, then there exist two distinct representations p1 and p2 in A×ˢB such that each has UniqueMul A B p1.1 p1.2 and UniqueMul A B p2.1 p2.2.
Русский
Если 1 < |A|·|B|, то существуют две различные представления p1, p2 в A×ˢB, каждое из которых удовлетворяет UniqueMul A B p1.1 p1.2 и UniqueMul A B p2.1 p2.2.
LaTeX
$$$1 < |A| \\cdot |B| \\Rightarrow \\exists p_1 \\in A \\timesˢ B, \\exists p_2 \\in A \\timesˢ B, p_1 \\neq p_2 \\land UniqueMul A B p_1.1 p_1.2 \\land UniqueMul A B p_2.1 p_2.2$$$
Lean4
@[to_additive]
theorem uniqueMul_of_twoUniqueMul {G} [Mul G] {A B : Finset G}
(h : 1 < #A * #B → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2)
(hA : A.Nonempty) (hB : B.Nonempty) : ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b :=
by
by_cases hc : #A ≤ 1 ∧ #B ≤ 1
· exact UniqueMul.of_card_le_one hA hB hc.1 hc.2
simp_rw [not_and_or, not_le] at hc
rw [← Finset.card_pos] at hA hB
obtain ⟨p, hp, _, _, _, hu, _⟩ := h (Nat.one_lt_mul_iff.mpr ⟨hA, hB, hc⟩)
rw [Finset.mem_product] at hp
exact ⟨p.1, hp.1, p.2, hp.2, hu⟩
