English
If a ≤ a2 and b ≤ b2 with left/right strict mono, then a2*b2 ≤ a*b implies a2=a and b2=b.
Русский
При условии строгой монотонности слева и справа, если a2*b2 ≤ a*b, тогда a2=a и b2=b.
LaTeX
$$$$ \\forall a1,a2,b1,b2 \\in \\alpha,\; a1 \\le a2 \\land b1 \\le b2 \\Rightarrow a2 \\cdot b2 \\le a1 \\cdot b1 \\iff a1=a2 \\land b1=b2 $$$$
Lean4
@[to_additive]
theorem mul_le_mul_iff_of_ge [MulLeftStrictMono α] [MulRightStrictMono α] {a₁ a₂ b₁ b₂ : α} (ha : a₁ ≤ a₂)
(hb : b₁ ≤ b₂) : a₂ * b₂ ≤ a₁ * b₁ ↔ a₁ = a₂ ∧ b₁ = b₂ :=
by
haveI := mulLeftMono_of_mulLeftStrictMono α
haveI := mulRightMono_of_mulRightStrictMono α
refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
simp only [eq_iff_le_not_lt, ha, hb, true_and]
refine ⟨fun ha ↦ h.not_gt ?_, fun hb ↦ h.not_gt ?_⟩
exacts [mul_lt_mul_of_lt_of_le ha hb, mul_lt_mul_of_le_of_lt ha hb]
