[GOAL]
α : Type u
β✝ : Type u_1
inst✝³ : OrderedCommMonoid α
β : Type u_2
inst✝² : One β
inst✝¹ : Mul β
inst✝ : Pow β ℕ
f : β → α
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : β), f (x * y) = f x * f y
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
src✝¹ : PartialOrder β := PartialOrder.lift f hf
src✝ : CommMonoid β := Injective.commMonoid f hf one mul npow
a b : β
ab : a ≤ b
c : β
⊢ f (c * a) ≤ f (c * b)
[PROOFSTEP]
rw [mul, mul]
[GOAL]
α : Type u
β✝ : Type u_1
inst✝³ : OrderedCommMonoid α
β : Type u_2
inst✝² : One β
inst✝¹ : Mul β
inst✝ : Pow β ℕ
f : β → α
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : β), f (x * y) = f x * f y
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
src✝¹ : PartialOrder β := PartialOrder.lift f hf
src✝ : CommMonoid β := Injective.commMonoid f hf one mul npow
a b : β
ab : a ≤ b
c : β
⊢ f c * f a ≤ f c * f b
[PROOFSTEP]
apply mul_le_mul_left'
[GOAL]
case bc
α : Type u
β✝ : Type u_1
inst✝³ : OrderedCommMonoid α
β : Type u_2
inst✝² : One β
inst✝¹ : Mul β
inst✝ : Pow β ℕ
f : β → α
hf : Injective f
one : f 1 = 1
mul : ∀ (x y : β), f (x * y) = f x * f y
npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n
src✝¹ : PartialOrder β := PartialOrder.lift f hf
src✝ : CommMonoid β := Injective.commMonoid f hf one mul npow
a b : β
ab : a ≤ b
c : β
⊢ f a ≤ f b
[PROOFSTEP]
exact ab
[GOAL]
α : Type u
β : Type u_1
inst✝⁴ : Mul α
inst✝³ : LinearOrder α
inst✝² : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b a0 b0 : α
ha : a0 ≤ a
hb : b0 ≤ b
ab : a * b ≤ a0 * b0
⊢ a = a0 ∧ b = b0
[PROOFSTEP]
haveI := Mul.to_covariantClass_right α
[GOAL]
α : Type u
β : Type u_1
inst✝⁴ : Mul α
inst✝³ : LinearOrder α
inst✝² : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b a0 b0 : α
ha : a0 ≤ a
hb : b0 ≤ b
ab : a * b ≤ a0 * b0
this : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
⊢ a = a0 ∧ b = b0
[PROOFSTEP]
have ha' : ¬a0 * b0 < a * b → ¬a0 < a := mt (mul_lt_mul_of_lt_of_le · hb)
[GOAL]
α : Type u
β : Type u_1
inst✝⁴ : Mul α
inst✝³ : LinearOrder α
inst✝² : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b a0 b0 : α
ha : a0 ≤ a
hb : b0 ≤ b
ab : a * b ≤ a0 * b0
this : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
ha' : ¬a0 * b0 < a * b → ¬a0 < a
⊢ a = a0 ∧ b = b0
[PROOFSTEP]
have hb' : ¬a0 * b0 < a * b → ¬b0 < b := mt (mul_lt_mul_of_le_of_lt ha ·)
[GOAL]
α : Type u
β : Type u_1
inst✝⁴ : Mul α
inst✝³ : LinearOrder α
inst✝² : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b a0 b0 : α
ha : a0 ≤ a
hb : b0 ≤ b
ab : a * b ≤ a0 * b0
this : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
ha' : ¬a0 * b0 < a * b → ¬a0 < a
hb' : ¬a0 * b0 < a * b → ¬b0 < b
⊢ a = a0 ∧ b = b0
[PROOFSTEP]
push_neg at ha' hb' 
[GOAL]
α : Type u
β : Type u_1
inst✝⁴ : Mul α
inst✝³ : LinearOrder α
inst✝² : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b a0 b0 : α
ha : a0 ≤ a
hb : b0 ≤ b
ab : a * b ≤ a0 * b0
this : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
ha' : a * b ≤ a0 * b0 → a ≤ a0
hb' : a * b ≤ a0 * b0 → b ≤ b0
⊢ a = a0 ∧ b = b0
[PROOFSTEP]
exact ⟨ha.antisymm' (ha' ab), hb.antisymm' (hb' ab)⟩
