case inl
α : Type u_1
a✝ b✝ c✝ d : α
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x x_1 => x < x_1
a : { x // 0 ≤ x }
b c : α
h : b * ↑a < c * ↑a
ha : 0 = ↑a
⊢ b < c

case inr
α : Type u_1
a✝ b✝ c✝ d : α
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x x_1 => x < x_1
a : { x // 0 ≤ x }
b c : α
h : b * ↑a < c * ↑a
ha : 0 < ↑a
⊢ b < c
α : Type u_1
a✝ b✝ c✝ d : α
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x x_1 => x < x_1
a : { x // 0 ≤ x }
b c : α
h : b * ↑a < c * ↑a
⊢ b < c
obtain ha | ha := a.prop.eq_or_lt
no goals
case inl
α : Type u_1
a✝ b✝ c✝ d : α
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h✝ : ContravariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x x_1 => x < x_1
a : { x // 0 ≤ x }
b c : α
h : b * ↑a < c * ↑a
ha : 0 = ↑a
⊢ b < c
simp [←ha] at h