α : Type u_1
β : Type ?u.17481
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)
α : Type u_1
β : Type ?u.17481
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)
rw [add_comm c, tsub_le_iff_left, add_assoc, ← tsub_le_iff_left, ← tsub_le_iff_left]
α : Type u_1
β : Type ?u.17481
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)
α : Type u_1
β : Type ?u.17481
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)
refine' (tsub_le_tsub_right add_tsub_le_assoc c).trans _
α : Type u_1
β : Type ?u.17481
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)
α : Type u_1
β : Type ?u.17481
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)
rw [add_comm a, add_comm (a - c)]
no goals
α : Type u_1
β : Type ?u.17481
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)
exact add_tsub_le_assoc