[GOAL]
α : Type u_1
a b c d x y z : α
inst✝⁶ : LinearOrderedCommMonoidWithZero α
β : Type u_2
inst✝⁵ : Zero β
inst✝⁴ : One β
inst✝³ : Mul β
inst✝² : Pow β ℕ
inst✝¹ : Sup β
inst✝ : Inf β
f : β → α
hf : Injective f
zero : f 0 = 0
one : f 1 = 1
mul : ∀ (x y : β), f (x * y) = f x * f y
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
hsup : ∀ (x y : β), f (x ⊔ y) = max (f x) (f y)
hinf : ∀ (x y : β), f (x ⊓ y) = min (f x) (f y)
src✝² : LinearOrder β := LinearOrder.lift f hf hsup hinf
src✝¹ : OrderedCommMonoid β := orderedCommMonoid f hf one mul npow
src✝ : CommMonoidWithZero β := Injective.commMonoidWithZero f hf zero one mul npow
⊢ f 0 ≤ f 1
[PROOFSTEP]
simp only [zero, one, LinearOrderedCommMonoidWithZero.zero_le_one]
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommMonoidWithZero α
⊢ 0 ≤ a
[PROOFSTEP]
simpa only [mul_zero, mul_one] using mul_le_mul_left' zero_le_one a
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
h : c ≠ 0
hab : a * c ≤ b * c
⊢ a ≤ b
[PROOFSTEP]
simpa only [mul_inv_cancel_right₀ h] using mul_le_mul_right' hab c⁻¹
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
h : c ≠ 0
hab : a * c ≤ b
⊢ a * c ≤ b * c⁻¹ * c
[PROOFSTEP]
simpa [h] using hab
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b * c
⊢ a * c⁻¹ ≤ b
[PROOFSTEP]
by_cases h : c = 0
[GOAL]
case pos
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b * c
h : c = 0
⊢ a * c⁻¹ ≤ b
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b * c
h : ¬c = 0
⊢ a * c⁻¹ ≤ b
[PROOFSTEP]
exact le_of_le_mul_right h (by simpa [h] using hab)
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b * c
h : ¬c = 0
⊢ a * c⁻¹ * c ≤ b * c
[PROOFSTEP]
simpa [h] using hab
[GOAL]
α : Type u_1
a✝ b✝ c✝ d✝ x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
a b c d : α
hb : b ≠ 0
hd : d ≠ 0
⊢ a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b
[PROOFSTEP]
rw [mul_inv_le_iff₀ hb, mul_right_comm, le_mul_inv_iff₀ hd]
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b
hb : b ≠ 0
hcd : c < d
hd : d ≠ 0
ha : a = 0
⊢ a * c < b * d
[PROOFSTEP]
rw [ha, zero_mul, zero_lt_iff]
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b
hb : b ≠ 0
hcd : c < d
hd : d ≠ 0
ha : a = 0
⊢ b * d ≠ 0
[PROOFSTEP]
exact mul_ne_zero hb hd
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b
hb : b ≠ 0
hcd : c < d
hd : d ≠ 0
ha : ¬a = 0
hc : c = 0
⊢ a * c < b * d
[PROOFSTEP]
rw [hc, mul_zero, zero_lt_iff]
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hab : a ≤ b
hb : b ≠ 0
hcd : c < d
hd : d ≠ 0
ha : ¬a = 0
hc : c = 0
⊢ b * d ≠ 0
[PROOFSTEP]
exact mul_ne_zero hb hd
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
h : x < y * z
⊢ x * z⁻¹ < y
[PROOFSTEP]
contrapose! h
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
h : y ≤ x * z⁻¹
⊢ y * z ≤ x
[PROOFSTEP]
simpa only [inv_inv] using mul_inv_le_of_le_mul h
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
h : x < y * z
⊢ y⁻¹ * x < z
[PROOFSTEP]
rw [mul_comm] at *
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
h : x < z * y
⊢ x * y⁻¹ < z
[PROOFSTEP]
exact mul_inv_lt_of_lt_mul₀ h
[GOAL]
α : Type u_1
a b c✝ d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
c : α
h : a < b
hc : c ≠ 0
⊢ a * c < b * c
[PROOFSTEP]
contrapose! h
[GOAL]
α : Type u_1
a b c✝ d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
c : α
hc : c ≠ 0
h : b * c ≤ a * c
⊢ b ≤ a
[PROOFSTEP]
exact le_of_le_mul_right hc h
[GOAL]
α : 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
[PROOFSTEP]
have ha : a ≠ 0 := ne_of_gt (lt_of_lt_of_le hc hh)
[GOAL]
α : 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
[PROOFSTEP]
simp_rw [← inv_le_inv₀ ha (ne_of_gt hc)] at hh 
[GOAL]
α : 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
[PROOFSTEP]
have := mul_lt_mul_of_lt_of_le₀ hh (inv_ne_zero (ne_of_gt hc)) h
[GOAL]
α : 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
[PROOFSTEP]
simpa [inv_mul_cancel_left₀ ha, inv_mul_cancel_left₀ (ne_of_gt hc)] using this
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
ha : a ≠ 0
⊢ a * b ≤ a * c ↔ b ≤ c
[PROOFSTEP]
simp only [mul_comm a]
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
ha : a ≠ 0
⊢ b * a ≤ c * a ↔ b ≤ c
[PROOFSTEP]
exact mul_le_mul_right₀ ha
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hc : c ≠ 0
⊢ a / c ≤ b / c ↔ a ≤ b
[PROOFSTEP]
rw [div_eq_mul_inv, div_eq_mul_inv, mul_le_mul_right₀ (inv_ne_zero hc)]
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ a / b ≤ a / c ↔ c ≤ b
[PROOFSTEP]
simp only [div_eq_mul_inv, mul_le_mul_left₀ ha, inv_le_inv₀ hb hc]
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hc : c ≠ 0
⊢ a ≤ b / c ↔ a * c ≤ b
[PROOFSTEP]
rw [div_eq_mul_inv, le_mul_inv_iff₀ hc]
[GOAL]
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
hc : c ≠ 0
⊢ a / c ≤ b ↔ a ≤ b * c
[PROOFSTEP]
rw [div_eq_mul_inv, mul_inv_le_iff₀ hc]
[GOAL]
α : Type u_1
a✝ b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
a : α
ha : a ≠ 0
⊢ symm (mulLeft₀' ha) = mulLeft₀' (_ : a⁻¹ ≠ 0)
[PROOFSTEP]
ext
[GOAL]
case h.h
α : Type u_1
a✝ b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
a : α
ha : a ≠ 0
x✝ : α
⊢ ↑(symm (mulLeft₀' ha)) x✝ = ↑(mulLeft₀' (_ : a⁻¹ ≠ 0)) x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
a✝ b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
a : α
ha : a ≠ 0
⊢ symm (mulRight₀' ha) = mulRight₀' (_ : a⁻¹ ≠ 0)
[PROOFSTEP]
ext
[GOAL]
case h.h
α : Type u_1
a✝ b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
a : α
ha : a ≠ 0
x✝ : α
⊢ ↑(symm (mulRight₀' ha)) x✝ = ↑(mulRight₀' (_ : a⁻¹ ≠ 0)) x✝
[PROOFSTEP]
rfl
