[GOAL]
α : Type u
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
⊢ ContravariantClass (WithZero α) (WithZero α) (fun x x_1 => x * x_1) fun x x_1 => x < x_1
[PROOFSTEP]
refine ⟨fun a b c h => ?_⟩
[GOAL]
α : Type u
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : WithZero α
h : a * b < a * c
⊢ b < c
[PROOFSTEP]
have := ((zero_le _).trans_lt h).ne'
[GOAL]
α : Type u
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c : WithZero α
h : a * b < a * c
this : a * c ≠ 0
⊢ b < c
[PROOFSTEP]
induction a using WithZero.recZeroCoe
[GOAL]
case h₁
α : Type u
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
b c : WithZero α
h : 0 * b < 0 * c
this : 0 * c ≠ 0
⊢ b < c
[PROOFSTEP]
exfalso
[GOAL]
case h₁.h
α : Type u
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
b c : WithZero α
h : 0 * b < 0 * c
this : 0 * c ≠ 0
⊢ False
[PROOFSTEP]
exact left_ne_zero_of_mul this rfl
[GOAL]
case h₂
α : Type u
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
b c : WithZero α
a✝ : α
h : ↑a✝ * b < ↑a✝ * c
this : ↑a✝ * c ≠ 0
⊢ b < c
[PROOFSTEP]
induction c using WithZero.recZeroCoe
[GOAL]
case h₂.h₁
α : Type u
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
b : WithZero α
a✝ : α
h : ↑a✝ * b < ↑a✝ * 0
this : ↑a✝ * 0 ≠ 0
⊢ b < 0
[PROOFSTEP]
exfalso
[GOAL]
case h₂.h₁.h
α : Type u
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
b : WithZero α
a✝ : α
h : ↑a✝ * b < ↑a✝ * 0
this : ↑a✝ * 0 ≠ 0
⊢ False
[PROOFSTEP]
exact right_ne_zero_of_mul this rfl
[GOAL]
case h₂.h₂
α : Type u
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
b : WithZero α
a✝¹ a✝ : α
h : ↑a✝¹ * b < ↑a✝¹ * ↑a✝
this : ↑a✝¹ * ↑a✝ ≠ 0
⊢ b < ↑a✝
[PROOFSTEP]
induction b using WithZero.recZeroCoe
[GOAL]
case h₂.h₂.h₁
α : Type u
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a✝¹ a✝ : α
this : ↑a✝¹ * ↑a✝ ≠ 0
h : ↑a✝¹ * 0 < ↑a✝¹ * ↑a✝
⊢ 0 < ↑a✝
case h₂.h₂.h₂
α : Type u
inst✝² : Mul α
inst✝¹ : PartialOrder α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a✝² a✝¹ : α
this : ↑a✝² * ↑a✝¹ ≠ 0
a✝ : α
h : ↑a✝² * ↑a✝ < ↑a✝² * ↑a✝¹
⊢ ↑a✝ < ↑a✝¹
[PROOFSTEP]
exacts [zero_lt_coe _, coe_lt_coe.mpr (lt_of_mul_lt_mul_left' <| coe_lt_coe.mp h)]
