Lean4
/-- If a group has `UniqueProds`, then it actually has `TwoUniqueProds`.
For an example of a semigroup `G` embeddable into a group that has `UniqueProds`
but not `TwoUniqueProds`, see Example 10.13 in
[J. Okniński, *Semigroup Algebras*][Okninski1991]. -/
@[to_additive]
theorem toTwoUniqueProds_of_group {G} [Group G] [UniqueProds G] : TwoUniqueProds G where
uniqueMul_of_one_lt_card {A B}
hc := by
simp_rw [Nat.one_lt_mul_iff, card_pos] at hc
obtain ⟨a, ha, b, hb, hu⟩ := uniqueMul_of_nonempty hc.1 hc.2.1
let C :=
A.map
⟨_, mul_right_injective a⁻¹⟩ -- C = a⁻¹A
let D :=
B.map
⟨_, mul_left_injective b⁻¹⟩ -- D = Bb⁻¹
have hcard : 1 < #C ∨ 1 < #D := by simp_rw [C, D, card_map]; exact hc.2.2
have hC : 1 ∈ C := mem_map.mpr ⟨a, ha, inv_mul_cancel a⟩
have hD : 1 ∈ D := mem_map.mpr ⟨b, hb, mul_inv_cancel b⟩
suffices ∃ c ∈ C, ∃ d ∈ D, (c ≠ 1 ∨ d ≠ 1) ∧ UniqueMul C D c d
by
simp_rw [mem_product]
obtain ⟨c, hc, d, hd, hne, hu'⟩ := this
obtain ⟨a0, ha0, rfl⟩ := mem_map.mp hc
obtain ⟨b0, hb0, rfl⟩ := mem_map.mp hd
refine ⟨(_, _), ⟨ha0, hb0⟩, (a, b), ⟨ha, hb⟩, ?_, fun a' b' ha' hb' he => ?_, hu⟩
· simp_rw [Function.Embedding.coeFn_mk, Ne, inv_mul_eq_one, mul_inv_eq_one] at hne
rwa [Ne, Prod.mk_inj, not_and_or, eq_comm]
specialize hu' (mem_map_of_mem _ ha') (mem_map_of_mem _ hb')
simp_rw [Function.Embedding.coeFn_mk, mul_left_cancel_iff, mul_right_cancel_iff] at hu'
rw [mul_assoc, ← mul_assoc a', he, mul_assoc, mul_assoc] at hu'
exact hu' rfl
classical
let _ :=
Finset.mul (α := G) -- E = D⁻¹C, F = DC⁻¹
have := uniqueMul_of_nonempty (A := D.image (·⁻¹) * C) (B := D * C.image (·⁻¹)) ?_ ?_
· obtain ⟨e, he, f, hf, hu⟩ := this
clear_value C D
simp only [UniqueMul, mem_mul, mem_image] at he hf hu
obtain ⟨_, ⟨d1, hd1, rfl⟩, c1, hc1, rfl⟩ := he
obtain ⟨d2, hd2, _, ⟨c2, hc2, rfl⟩, rfl⟩ := hf
by_cases h12 : c1 ≠ 1 ∨ d2 ≠ 1
· refine ⟨c1, hc1, d2, hd2, h12, fun c3 d3 hc3 hd3 he => ?_⟩
specialize hu ⟨_, ⟨_, hd1, rfl⟩, _, hc3, rfl⟩ ⟨_, hd3, _, ⟨_, hc2, rfl⟩, rfl⟩
rw [mul_left_cancel_iff, mul_right_cancel_iff, mul_assoc, ← mul_assoc c3, he, mul_assoc, mul_assoc] at hu;
exact hu rfl
push_neg at h12; obtain ⟨rfl, rfl⟩ := h12
by_cases h21 : c2 ≠ 1 ∨ d1 ≠ 1
· refine ⟨c2, hc2, d1, hd1, h21, fun c4 d4 hc4 hd4 he => ?_⟩
specialize hu ⟨_, ⟨_, hd4, rfl⟩, _, hC, rfl⟩ ⟨_, hD, _, ⟨_, hc4, rfl⟩, rfl⟩
simpa only [mul_one, one_mul, ← mul_inv_rev, he, true_imp_iff, inv_inj, and_comm] using hu
push_neg at h21; obtain ⟨rfl, rfl⟩ := h21
rcases hcard with hC | hD
· obtain ⟨c, hc, hc1⟩ := exists_mem_ne hC 1
refine (hc1 ?_).elim
simpa using hu ⟨_, ⟨_, hD, rfl⟩, _, hc, rfl⟩ ⟨_, hD, _, ⟨_, hc, rfl⟩, rfl⟩
· obtain ⟨d, hd, hd1⟩ := exists_mem_ne hD 1
refine (hd1 ?_).elim
simpa using hu ⟨_, ⟨_, hd, rfl⟩, _, hC, rfl⟩ ⟨_, hd, _, ⟨_, hC, rfl⟩, rfl⟩
all_goals apply_rules [Nonempty.mul, Nonempty.image, Finset.Nonempty.map, hc.1, hc.2.1]
