[GOAL]
α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : Add α
inst✝⁵ : Sub α
inst✝⁴ : OrderedSub α
a✝ b✝ c d : α
inst✝³ : Preorder β
inst✝² : Add β
inst✝¹ : Sub β
inst✝ : OrderedSub β
f : AddHom α β
hf : Monotone ↑f
a b : α
⊢ ↑f a - ↑f b ≤ ↑f (a - b)
[PROOFSTEP]
rw [tsub_le_iff_right, ← f.map_add]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : Add α
inst✝⁵ : Sub α
inst✝⁴ : OrderedSub α
a✝ b✝ c d : α
inst✝³ : Preorder β
inst✝² : Add β
inst✝¹ : Sub β
inst✝ : OrderedSub β
f : AddHom α β
hf : Monotone ↑f
a b : α
⊢ ↑f a ≤ ↑f (a - b + b)
[PROOFSTEP]
exact hf le_tsub_add
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁸ : Preorder α
inst✝⁷ : Add α
inst✝⁶ : Sub α
inst✝⁵ : OrderedSub α
a✝ b✝ c✝ d : α
R : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Preorder R
inst✝² : Sub R
inst✝¹ : OrderedSub R
inst✝ : CovariantClass R R (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : R
⊢ a * c - b * c ≤ (a - b) * c
[PROOFSTEP]
simpa only [mul_comm _ c] using le_mul_tsub
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Preorder M
inst✝⁶ : Add M
inst✝⁵ : Sub M
inst✝⁴ : OrderedSub M
inst✝³ : PartialOrder N
inst✝² : Add N
inst✝¹ : Sub N
inst✝ : OrderedSub N
e : M ≃o N
h_add : ∀ (a b : M), ↑e (a + b) = ↑e a + ↑e b
a b : M
⊢ ↑e (a - b) = ↑e a - ↑e b
[PROOFSTEP]
let e_add : M ≃+ N := { e with map_add' := h_add }
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Preorder M
inst✝⁶ : Add M
inst✝⁵ : Sub M
inst✝⁴ : OrderedSub M
inst✝³ : PartialOrder N
inst✝² : Add N
inst✝¹ : Sub N
inst✝ : OrderedSub N
e : M ≃o N
h_add : ∀ (a b : M), ↑e (a + b) = ↑e a + ↑e b
a b : M
e_add : M ≃+ N := { toEquiv := e.toEquiv, map_add' := h_add }
⊢ ↑e (a - b) = ↑e a - ↑e b
[PROOFSTEP]
refine' le_antisymm _ (e_add.toAddHom.le_map_tsub e.monotone a b)
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Preorder M
inst✝⁶ : Add M
inst✝⁵ : Sub M
inst✝⁴ : OrderedSub M
inst✝³ : PartialOrder N
inst✝² : Add N
inst✝¹ : Sub N
inst✝ : OrderedSub N
e : M ≃o N
h_add : ∀ (a b : M), ↑e (a + b) = ↑e a + ↑e b
a b : M
e_add : M ≃+ N := { toEquiv := e.toEquiv, map_add' := h_add }
⊢ ↑e (a - b) ≤ ↑e a - ↑e b
[PROOFSTEP]
suffices e (e.symm (e a) - e.symm (e b)) ≤ e (e.symm (e a - e b)) by simpa
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Preorder M
inst✝⁶ : Add M
inst✝⁵ : Sub M
inst✝⁴ : OrderedSub M
inst✝³ : PartialOrder N
inst✝² : Add N
inst✝¹ : Sub N
inst✝ : OrderedSub N
e : M ≃o N
h_add : ∀ (a b : M), ↑e (a + b) = ↑e a + ↑e b
a b : M
e_add : M ≃+ N := { toEquiv := e.toEquiv, map_add' := h_add }
this : ↑e (↑(symm e) (↑e a) - ↑(symm e) (↑e b)) ≤ ↑e (↑(symm e) (↑e a - ↑e b))
⊢ ↑e (a - b) ≤ ↑e a - ↑e b
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
M : Type u_3
N : Type u_4
inst✝⁷ : Preorder M
inst✝⁶ : Add M
inst✝⁵ : Sub M
inst✝⁴ : OrderedSub M
inst✝³ : PartialOrder N
inst✝² : Add N
inst✝¹ : Sub N
inst✝ : OrderedSub N
e : M ≃o N
h_add : ∀ (a b : M), ↑e (a + b) = ↑e a + ↑e b
a b : M
e_add : M ≃+ N := { toEquiv := e.toEquiv, map_add' := h_add }
⊢ ↑e (↑(symm e) (↑e a) - ↑(symm e) (↑e b)) ≤ ↑e (↑(symm e) (↑e a - ↑e b))
[PROOFSTEP]
exact e.monotone (e_add.symm.toAddHom.le_map_tsub e.symm.monotone _ _)
