α : Type ?u.7326
β : Type ?u.7329
M : Type u_1
N : Type u_2
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
α : Type ?u.7326
β : Type ?u.7329
M : Type u_1
N : Type u_2
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
let e_add : M ≃+ N := { e with map_add' := h_add }
α : Type ?u.7326
β : Type ?u.7329
M : Type u_1
N : Type u_2
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
α : Type ?u.7326
β : Type ?u.7329
M : Type u_1
N : Type u_2
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
refine' le_antisymm _ (e_add.toAddHom.le_map_tsub e.monotone a b)
α : Type ?u.7326
β : Type ?u.7329
M : Type u_1
N : Type u_2
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))
α : Type ?u.7326
β : Type ?u.7329
M : Type u_1
N : Type u_2
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
suffices e (e.symm (e a) - e.symm (e b)) ≤ e (e.symm (e a - e b)) by simpa
no goals
α : Type ?u.7326
β : Type ?u.7329
M : Type u_1
N : Type u_2
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))
exact e.monotone (e_add.symm.toAddHom.le_map_tsub e.symm.monotone _ _)
no goals
α : Type ?u.7326
β : Type ?u.7329
M : Type u_1
N : Type u_2
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
simpa