α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
h : a * b < c * d
hc : 0 < c
hh : c ≤ a
ha : a ≠ 0
⊢ b < d
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
h : a * b < c * d
hc : 0 < c
hh : c ≤ a
⊢ b < d
have ha : a ≠ 0 := ne_of_gt (lt_of_lt_of_le hc hh)
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
h : a * b < c * d
hc : 0 < c
ha : a ≠ 0
hh : a⁻¹ ≤ c⁻¹
⊢ b < d
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
h : a * b < c * d
hc : 0 < c
hh : c ≤ a
ha : a ≠ 0
⊢ b < d
simp_rw [← inv_le_inv₀ ha (ne_of_gt hc)] at hh
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
h : a * b < c * d
hc : 0 < c
ha : a ≠ 0
hh : a⁻¹ ≤ c⁻¹
this : a⁻¹ * (a * b) < c⁻¹ * (c * d)
⊢ b < d
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
h : a * b < c * d
hc : 0 < c
ha : a ≠ 0
hh : a⁻¹ ≤ c⁻¹
⊢ b < d
have := mul_lt_mul_of_lt_of_le₀ hh (inv_ne_zero (ne_of_gt hc)) h
no goals
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
h : a * b < c * d
hc : 0 < c
ha : a ≠ 0
hh : a⁻¹ ≤ c⁻¹
this : a⁻¹ * (a * b) < c⁻¹ * (c * d)
⊢ b < d
simpa [inv_mul_cancel_left₀ ha, inv_mul_cancel_left₀ (ne_of_gt hc)] using this