-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
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

Proof state:
case refine_2
α : Type u_3
a b c d : α
inst✝³ : MulZeroClass α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd✝ : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
hcd : c < d
⊢ a * c < b * d

Tactic:
exact (mul_lt_mul_of_pos_left hcd a0).trans_le (mul_le_mul_of_nonneg_right hab d0.le)

Result:
no goals

Proof state:
α : Type u_3
a b c d : α
inst✝³ : MulZeroClass α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
⊢ a = b ∧ c = d → a * c = b * d

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case intro
α : Type u_3
a c : α
inst✝³ : MulZeroClass α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
a0 : 0 < a
hab : a ≤ a
hcd : c ≤ c
d0 : 0 < c
⊢ a * c = a * c

Proof state:
α : Type u_3
a b c d : α
inst✝³ : MulZeroClass α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
⊢ a = b ∧ c = d

Tactic:
simp only [eq_iff_le_not_lt, hab, hcd, true_and]

Result:
α : Type u_3
a b c d : α
inst✝³ : MulZeroClass α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
⊢ ¬a < b ∧ ¬c < d

Proof state:
case intro
α : Type u_3
a c : α
inst✝³ : MulZeroClass α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
a0 : 0 < a
hab : a ≤ a
hcd : c ≤ c
d0 : 0 < c
⊢ a * c = a * c

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_3
a b c d : α
inst✝³ : MulZeroClass α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
⊢ a * c = b * d ↔ a = b ∧ c = d

Tactic:
refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩

Result:
α : Type u_3
a b c d : α
inst✝³ : MulZeroClass α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
⊢ a = b ∧ c = d

Proof state:
α : Type u_3
a b c d : α
inst✝³ : MulZeroClass α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
⊢ ¬a < b ∧ ¬c < d

Tactic:
refine ⟨fun hab ↦ h.not_lt ?_, fun hcd ↦ h.not_lt ?_⟩

Result:
case refine_1
α : Type u_3
a b c d : α
inst✝³ : MulZeroClass α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab✝ : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
hab : a < b
⊢ a * c < b * d

case refine_2
α : Type u_3
a b c d : α
inst✝³ : MulZeroClass α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd✝ : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
hcd : c < d
⊢ a * c < b * d

Proof state:
case refine_1
α : Type u_3
a b c d : α
inst✝³ : MulZeroClass α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab✝ : a ≤ b
hcd : c ≤ d
a0 : 0 < a
d0 : 0 < d
h : a * c = b * d
hab : a < b
⊢ a * c < b * d

Tactic:
exact (mul_le_mul_of_nonneg_left hcd a0.le).trans_lt (mul_lt_mul_of_pos_right hab d0)

Result:
no goals