case inl
α : Type u_1
a c d : α
inst✝⁵ : MulZeroClass α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : PosMulMonoRev α
inst✝ : MulPosMonoRev α
hbd : c ≤ d
c0 : 0 < c
hac : a ≤ a
b0 : 0 < a
h : a * c = a * d
⊢ a = a ∧ c = d

case inr
α : Type u_1
a b c d : α
inst✝⁵ : MulZeroClass α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : PosMulMonoRev α
inst✝ : MulPosMonoRev α
hac✝ : a ≤ b
hbd : c ≤ d
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
hac : a < b
⊢ a = b ∧ c = d
α : Type u_1
a b c d : α
inst✝⁵ : MulZeroClass α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : PosMulMonoRev α
inst✝ : MulPosMonoRev α
hac : a ≤ b
hbd : c ≤ d
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
⊢ a = b ∧ c = d
rcases hac.eq_or_lt with (rfl | hac)
case inr.inl
α : Type u_1
a b c : α
inst✝⁵ : MulZeroClass α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : PosMulMonoRev α
inst✝ : MulPosMonoRev α
hac✝ : a ≤ b
b0 : 0 < b
c0 : 0 < c
hac : a < b
hbd : c ≤ c
h : a * c = b * c
⊢ a = b ∧ c = c

case inr.inr
α : Type u_1
a b c d : α
inst✝⁵ : MulZeroClass α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : PosMulMonoRev α
inst✝ : MulPosMonoRev α
hac✝ : a ≤ b
hbd✝ : c ≤ d
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
hac : a < b
hbd : c < d
⊢ a = b ∧ c = d
case inr
α : Type u_1
a b c d : α
inst✝⁵ : MulZeroClass α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : PosMulMonoRev α
inst✝ : MulPosMonoRev α
hac✝ : a ≤ b
hbd : c ≤ d
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
hac : a < b
⊢ a = b ∧ c = d
rcases eq_or_lt_of_le hbd with (rfl | hbd)
no goals
case inr.inr
α : Type u_1
a b c d : α
inst✝⁵ : MulZeroClass α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : PosMulMonoRev α
inst✝ : MulPosMonoRev α
hac✝ : a ≤ b
hbd✝ : c ≤ d
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
hac : a < b
hbd : c < d
⊢ a = b ∧ c = d
exact ((mul_lt_mul_of_lt_of_lt' hac hbd b0 c0).ne h).elim
no goals
case inl
α : Type u_1
a c d : α
inst✝⁵ : MulZeroClass α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : PosMulMonoRev α
inst✝ : MulPosMonoRev α
hbd : c ≤ d
c0 : 0 < c
hac : a ≤ a
b0 : 0 < a
h : a * c = a * d
⊢ a = a ∧ c = d
exact ⟨rfl, (mul_left_cancel_iff_of_pos b0).mp h⟩
no goals
case inr.inl
α : Type u_1
a b c : α
inst✝⁵ : MulZeroClass α
inst✝⁴ : PartialOrder α
inst✝³ : PosMulStrictMono α
inst✝² : MulPosStrictMono α
inst✝¹ : PosMulMonoRev α
inst✝ : MulPosMonoRev α
hac✝ : a ≤ b
b0 : 0 < b
c0 : 0 < c
hac : a < b
hbd : c ≤ c
h : a * c = b * c
⊢ a = b ∧ c = c
exact ⟨(mul_right_cancel_iff_of_pos c0).mp h, rfl⟩