English
In a Monoid with partial order and positivity, if a ≤ b, c ≤ d and b>0, c>0, then a c = b d if and only if a=b and c=d.
Русский
В моноиде с частичным порядком и положительностью, если a ≤ b, c ≤ d и b>0, c>0, то a c = b d эквивалентно a=b и c=d.
LaTeX
$$$a \le b \land c \le d \land 0 < b \land 0 < c \Rightarrow a c = b d \iff a = b \land c = d$$$
Lean4
theorem mul_eq_mul_iff_eq_and_eq_of_pos' [PosMulStrictMono α] [MulPosStrictMono α] (hab : a ≤ b) (hcd : c ≤ d)
(b0 : 0 < b) (c0 : 0 < c) : a * c = b * d ↔ a = b ∧ c = d :=
by
refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
simp only [eq_iff_le_not_lt, hab, hcd, true_and]
refine ⟨fun hab ↦ h.not_lt ?_, fun hcd ↦ h.not_lt ?_⟩
· exact (mul_lt_mul_of_pos_right hab c0).trans_le (mul_le_mul_of_nonneg_left hcd b0.le)
· exact (mul_le_mul_of_nonneg_right hab c0.le).trans_lt (mul_lt_mul_of_pos_left hcd b0)
