English
Let a ≤ b and c ≤ d with a>0 and d>0. If a·c = b·d, then a=b and c=d, provided PosMulStrictMono and MulPosStrictMono hold.
Русский
Пусть a ≤ b и c ≤ d, причём a>0, d>0. Если a·c = b·d, тогда a=b и c=d, при условии PosMulStrictMono и MulPosStrictMono.
LaTeX
$$$a \le b\; \wedge\; c \le d\; \wedge\; a>0\; \wedge\; d>0 \Rightarrow (a\cdot c = b\cdot 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)
(a0 : 0 < a) (d0 : 0 < d) : 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_le_mul_of_nonneg_left hcd a0.le).trans_lt (mul_lt_mul_of_pos_right hab d0)
· exact (mul_lt_mul_of_pos_left hcd a0).trans_le (mul_le_mul_of_nonneg_right hab d0.le)
