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

Proof state:
case intro
α : Type u_3
a c : α
inst✝³ : MulZeroClass α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
c0 : 0 < c
hab : a ≤ a
b0 : 0 < a
hcd : c ≤ 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
b0 : 0 < b
c0 : 0 < c
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
b0 : 0 < b
c0 : 0 < c
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
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
hcd : c < d
⊢ a * c < b * d

Proof state:
α : Type u_3
a b c d : α
inst✝³ : MulZeroClass α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab : a ≤ b
hcd : c ≤ d
b0 : 0 < b
c0 : 0 < c
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
b0 : 0 < b
c0 : 0 < c
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
b0 : 0 < b
c0 : 0 < c
⊢ 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 α
c0 : 0 < c
hab : a ≤ a
b0 : 0 < a
hcd : c ≤ c
⊢ a * c = a * c

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
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
hab : a < b
⊢ a * c < b * d

Tactic:
exact (mul_lt_mul_of_pos_right hab c0).trans_le (mul_le_mul_of_nonneg_left hcd b0.le)

Result:
no goals

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
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
hcd : c < d
⊢ a * c < b * d

Tactic:
exact (mul_le_mul_of_nonneg_right hab c0.le).trans_lt (mul_lt_mul_of_pos_left hcd b0)

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
b0 : 0 < b
c0 : 0 < c
⊢ 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
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
⊢ a = b ∧ c = d