[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ a - b ≤ c ↔ a ≤ b + c
[PROOFSTEP]
rw [tsub_le_iff_right, add_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ a - b ≤ c ↔ a - c ≤ b
[PROOFSTEP]
rw [tsub_le_iff_left, tsub_le_iff_right]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + b - c ≤ a + (b - c)
[PROOFSTEP]
rw [tsub_le_iff_left, add_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + b ≤ a + (c + (b - c))
[PROOFSTEP]
exact add_le_add_left le_add_tsub a
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + b - c ≤ a - c + b
[PROOFSTEP]
rw [add_comm, add_comm _ b]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ b + a - c ≤ b + (a - c)
[PROOFSTEP]
exact add_tsub_le_assoc
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + b ≤ a + c + (b - c)
[PROOFSTEP]
rw [add_assoc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + b ≤ a + (c + (b - c))
[PROOFSTEP]
exact add_le_add_left le_add_tsub a
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + b ≤ a - c + (b + c)
[PROOFSTEP]
rw [add_comm a, add_comm (a - c)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ b + a ≤ b + c + (a - c)
[PROOFSTEP]
exact add_le_add_add_tsub
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a - c ≤ a - b + (b - c)
[PROOFSTEP]
rw [tsub_le_iff_left, ← add_assoc, add_right_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a ≤ c + (b - c) + (a - b)
[PROOFSTEP]
exact le_add_tsub.trans (add_le_add_right le_add_tsub _)
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ c - a - (c - b) ≤ b - a
[PROOFSTEP]
rw [tsub_le_iff_left, tsub_le_iff_left, add_left_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ c ≤ c - b + (a + (b - a))
[PROOFSTEP]
exact le_tsub_add.trans (add_le_add_left le_add_tsub _)
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + b - (c + d) ≤ a - c + (b - d)
[PROOFSTEP]
rw [add_comm c, tsub_le_iff_left, add_assoc, ← tsub_le_iff_left, ← tsub_le_iff_left]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + b - d - c ≤ a - c + (b - d)
[PROOFSTEP]
refine' (tsub_le_tsub_right add_tsub_le_assoc c).trans _
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + (b - d) - c ≤ a - c + (b - d)
[PROOFSTEP]
rw [add_comm a, add_comm (a - c)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ b - d + a - c ≤ b - d + (a - c)
[PROOFSTEP]
exact add_tsub_le_assoc
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + b - (a + c) ≤ b - c
[PROOFSTEP]
rw [tsub_le_iff_left, add_assoc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + b ≤ a + (c + (b - c))
[PROOFSTEP]
exact add_le_add_left le_add_tsub _
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + c - (b + c) ≤ a - b
[PROOFSTEP]
rw [tsub_le_iff_left, add_right_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : AddCommSemigroup α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ a + c ≤ b + (a - b) + c
[PROOFSTEP]
exact add_le_add_right le_add_tsub c
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
⊢ a ≤ a + b - b
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
⊢ a ≤ b + a - b
[PROOFSTEP]
exact hb.le_add_tsub_swap
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
h : a + b ≤ c
⊢ b + a ≤ c
[PROOFSTEP]
rwa [add_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : AddCommMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ a - b ≤ 0 ↔ a ≤ b
[PROOFSTEP]
rw [tsub_le_iff_left, add_zero]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b✝ c✝ d b a c : α
⊢ b - a - c = b - (a + c)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b✝ c✝ d b a c : α
⊢ b - a - c ≤ b - (a + c)
[PROOFSTEP]
rw [tsub_le_iff_left, tsub_le_iff_left, ← add_assoc, ← tsub_le_iff_left]
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b✝ c✝ d b a c : α
⊢ b - (a + c) ≤ b - a - c
[PROOFSTEP]
rw [tsub_le_iff_left, add_assoc, ← tsub_le_iff_left, ← tsub_le_iff_left]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b✝ c✝ d a b c : α
⊢ a - (b + c) = a - c - b
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b✝ c✝ d a b c : α
⊢ a - (c + b) = a - c - b
[PROOFSTEP]
apply tsub_add_eq_tsub_tsub
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ a - b - c = a - c - b
[PROOFSTEP]
rw [← tsub_add_eq_tsub_tsub, tsub_add_eq_tsub_tsub_swap]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
h : a = c + b
⊢ c ≤ a - b
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
h : a = c + b
⊢ c ≤ c + b - b
[PROOFSTEP]
exact hb.le_add_tsub
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
h : a = b + c
⊢ a = c + b
[PROOFSTEP]
rw [add_comm, h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
⊢ a + b = a + b
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
h : a - b < c
⊢ a < b + c
[PROOFSTEP]
rw [lt_iff_le_and_ne, ← tsub_le_iff_left]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
h : a - b < c
⊢ a - b ≤ c ∧ a ≠ b + c
[PROOFSTEP]
refine' ⟨h.le, _⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
h : a - b < c
⊢ a ≠ b + c
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c d : α
hb : AddLECancellable b
h : b + c - b < c
⊢ False
[PROOFSTEP]
simp [hb] at h 
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : a - c < b
⊢ a < b + c
[PROOFSTEP]
rw [lt_iff_le_and_ne, ← tsub_le_iff_right]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : a - c < b
⊢ a - c ≤ b ∧ a ≠ b + c
[PROOFSTEP]
refine' ⟨h.le, _⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : a - c < b
⊢ a ≠ b + c
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c d : α
hc : AddLECancellable c
h : b + c - c < b
⊢ False
[PROOFSTEP]
simp [hc] at h 
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : a + c < b
⊢ a ≠ b - c
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c d : α
hc : AddLECancellable c
h : b - c + c < b
⊢ False
[PROOFSTEP]
exact h.not_le le_tsub_add
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
h : a + c < b
⊢ c + a < b
[PROOFSTEP]
rwa [add_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
a✝ b✝ c✝ d : α
inst✝¹ : CovariantClass α α (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 c b : α
⊢ a + c - (b + c) = a - b
[PROOFSTEP]
refine' add_tsub_add_le_tsub_right.antisymm (tsub_le_iff_right.2 <| le_of_add_le_add_right _)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
a✝ b✝ c✝ d : α
inst✝¹ : CovariantClass α α (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 c b : α
⊢ α
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
a✝ b✝ c✝ d : α
inst✝¹ : CovariantClass α α (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 c b : α
⊢ a + ?refine'_1 ≤ a + c - (b + c) + b + ?refine'_1
[PROOFSTEP]
exact c
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
a✝ b✝ c✝ d : α
inst✝¹ : CovariantClass α α (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 c b : α
⊢ a + c ≤ a + c - (b + c) + b + c
[PROOFSTEP]
rw [add_assoc]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
a✝ b✝ c✝ d : α
inst✝¹ : CovariantClass α α (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 c b : α
⊢ a + c ≤ a + c - (b + c) + (b + c)
[PROOFSTEP]
exact le_tsub_add
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : AddCommSemigroup α
inst✝³ : Sub α
inst✝² : OrderedSub α
a✝ b✝ c✝ d : α
inst✝¹ : CovariantClass α α (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 c : α
⊢ a + b - (a + c) = b - c
[PROOFSTEP]
rw [add_comm a b, add_comm a c, add_tsub_add_eq_tsub_right]
