English
If G has IsRightCancelMul, LinearOrder, and MulLeftStrictMono, then TwoUniqueProds G.
Русский
Если G удовлетворяет IsRightCancelMul, линейному порядку и левостроительному монотонному слева, тогда TwoUniqueProds G.
LaTeX
$$$ [\\text{IsRightCancelMul }G][\\text{LinearOrder }G][\\text{MulLeftStrictMono }G] \\Rightarrow \\mathrm{TwoUniqueProds} G. $$$
Lean4
/-- This instance asserts that if `G` has a right-cancellative multiplication, a linear order, and
multiplication is strictly monotone w.r.t. the second argument, then `G` has `TwoUniqueProds`. -/
@[to_additive /-- This instance asserts that if `G` has a right-cancellative addition, a linear order,
and addition is strictly monotone w.r.t. the second argument, then `G` has `TwoUniqueSums`. -/
]
instance (priority := 100) of_covariant_right [IsRightCancelMul G] [LinearOrder G] [MulLeftStrictMono G] :
TwoUniqueProds G where
uniqueMul_of_one_lt_card {A B}
hc := by
obtain ⟨hA, hB, -⟩ := Nat.one_lt_mul_iff.mp hc
rw [card_pos] at hA hB
rw [← card_product] at hc
obtain ⟨a0, ha0, b0, hb0, he0⟩ := mem_mul.mp (max'_mem _ <| hA.mul hB)
obtain ⟨a1, ha1, b1, hb1, he1⟩ := mem_mul.mp (min'_mem _ <| hA.mul hB)
have : UniqueMul A B a0 b0 := by
intro a b ha hb he
obtain hl | rfl | hl := lt_trichotomy b b0
· exact ((he0 ▸ he ▸ mul_lt_mul_left' hl a).not_ge <| le_max' _ _ <| mul_mem_mul ha hb0).elim
· exact ⟨mul_right_cancel he, rfl⟩
· exact ((he0 ▸ mul_lt_mul_left' hl a0).not_ge <| le_max' _ _ <| mul_mem_mul ha0 hb).elim
refine ⟨_, mk_mem_product ha0 hb0, _, mk_mem_product ha1 hb1, fun he ↦ ?_, this, ?_⟩
· rw [Prod.mk_inj] at he; rw [he.1, he.2, he1] at he0
obtain ⟨⟨a2, b2⟩, h2, hne⟩ := exists_mem_ne hc (a0, b0)
rw [mem_product] at h2
refine (min'_lt_max' _ (mul_mem_mul ha0 hb0) (mul_mem_mul h2.1 h2.2) fun he ↦ hne ?_).ne he0
exact Prod.ext_iff.mpr (this h2.1 h2.2 he.symm)
· intro a b ha hb he
obtain hl | rfl | hl := lt_trichotomy b b1
· exact ((he1 ▸ mul_lt_mul_left' hl a1).not_ge <| min'_le _ _ <| mul_mem_mul ha1 hb).elim
· exact ⟨mul_right_cancel he, rfl⟩
· exact ((he1 ▸ he ▸ mul_lt_mul_left' hl a).not_ge <| min'_le _ _ <| mul_mem_mul ha hb1).elim
