[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : a ≤ b
⊢ a + (b - a) = b
[PROOFSTEP]
refine' le_antisymm _ le_add_tsub
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : a ≤ b
⊢ a + (b - a) ≤ b
[PROOFSTEP]
obtain ⟨c, rfl⟩ := exists_add_of_le h
[GOAL]
case intro
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c✝ d c : α
h : a ≤ a + c
⊢ a + (a + c - a) ≤ a + c
[PROOFSTEP]
exact add_le_add_left add_tsub_le_left a
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : a ≤ b
⊢ b - a + a = b
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : a ≤ b
⊢ a + (b - a) = b
[PROOFSTEP]
exact add_tsub_cancel_of_le h
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : c ≤ b
⊢ a - c ≤ b - c ↔ a ≤ b
[PROOFSTEP]
rw [tsub_le_iff_right, tsub_add_cancel_of_le h]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h1 : c ≤ a
h2 : c ≤ b
⊢ a - c = b - c ↔ a = b
[PROOFSTEP]
simp_rw [le_antisymm_iff, tsub_le_tsub_iff_right h1, tsub_le_tsub_iff_right h2]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : c ≤ b
h2 : a - c < b - c
⊢ a < b
[PROOFSTEP]
refine' ((tsub_le_tsub_iff_right h).mp h2.le).lt_of_ne _
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : c ≤ b
h2 : a - c < b - c
⊢ a ≠ b
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c d : α
h : c ≤ a
h2 : a - c < a - c
⊢ False
[PROOFSTEP]
exact h2.false
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hab : b ≤ a
hcb : c ≤ b
⊢ a - b + (b - c) = a - c
[PROOFSTEP]
convert tsub_add_cancel_of_le (tsub_le_tsub_right hab c) using 2
[GOAL]
case h.e'_2.h.e'_5
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hab : b ≤ a
hcb : c ≤ b
⊢ a - b = a - c - (b - c)
[PROOFSTEP]
rw [tsub_tsub, add_tsub_cancel_of_le hcb]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : c ≤ b
⊢ a - c - (b - c) = a - b
[PROOFSTEP]
rw [tsub_tsub, add_tsub_cancel_of_le h]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : c ≤ b
⊢ a = b - c → a + c = b
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c d : α
hc : AddLECancellable c
h : c ≤ b
⊢ b - c + c = b
[PROOFSTEP]
exact tsub_add_cancel_of_le h
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
h : b ≤ a
⊢ a - b = c ↔ a = c + b
[PROOFSTEP]
rw [eq_comm, hb.eq_tsub_iff_add_eq_of_le h, eq_comm]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b c d : α
hc : AddLECancellable c
h : c ≤ b
a : α
⊢ a + b - c = a + (b - c)
[PROOFSTEP]
conv_lhs => rw [← add_tsub_cancel_of_le h, add_comm c, ← add_assoc, hc.add_tsub_cancel_right]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b c d : α
hc : AddLECancellable c
h : c ≤ b
a : α
| a + b - c
[PROOFSTEP]
rw [← add_tsub_cancel_of_le h, add_comm c, ← add_assoc, hc.add_tsub_cancel_right]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b c d : α
hc : AddLECancellable c
h : c ≤ b
a : α
| a + b - c
[PROOFSTEP]
rw [← add_tsub_cancel_of_le h, add_comm c, ← add_assoc, hc.add_tsub_cancel_right]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b c d : α
hc : AddLECancellable c
h : c ≤ b
a : α
| a + b - c
[PROOFSTEP]
rw [← add_tsub_cancel_of_le h, add_comm c, ← add_assoc, hc.add_tsub_cancel_right]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
h : b ≤ a
⊢ a - b + c = a + c - b
[PROOFSTEP]
rw [add_comm a, hb.add_tsub_assoc_of_le h, add_comm]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hbc : AddLECancellable (b - c)
h₁ : b ≤ a
h₂ : c ≤ b
⊢ a = a - b + c + (b - c)
[PROOFSTEP]
rw [add_assoc, add_tsub_cancel_of_le h₂, tsub_add_cancel_of_le h₁]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
hd : AddLECancellable d
hba : b ≤ a
hdc : d ≤ c
⊢ a - b + (c - d) = a + c - (b + d)
[PROOFSTEP]
rw [hb.tsub_add_eq_add_tsub hba, ← hd.add_tsub_assoc_of_le hdc, tsub_tsub, add_comm d]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
h : a ≤ c
⊢ b ≤ c - a ↔ b + a ≤ c
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
h : a ≤ c
⊢ b ≤ c - a ↔ a + b ≤ c
[PROOFSTEP]
exact ha.le_tsub_iff_left h
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a - b < c ↔ a < b + c
[PROOFSTEP]
refine' ⟨hb.lt_add_of_tsub_lt_left, _⟩
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a < b + c → a - b < c
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + c
⊢ a - b < c
[PROOFSTEP]
refine' (tsub_le_iff_left.mpr h.le).lt_of_ne _
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + c
⊢ a - b ≠ c
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b d : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + (a - b)
⊢ False
[PROOFSTEP]
exact h.ne' (add_tsub_cancel_of_le hba)
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a - b < c ↔ a < c + b
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a - b < c ↔ a < b + c
[PROOFSTEP]
exact hb.tsub_lt_iff_left hba
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hb : AddLECancellable b
hc : AddLECancellable c
h₁ : b ≤ a
h₂ : c ≤ a
⊢ a - b < c ↔ a - c < b
[PROOFSTEP]
rw [hb.tsub_lt_iff_left h₁, hc.tsub_lt_iff_right h₂]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
hc : AddLECancellable c
h₁ : a ≤ b
h₂ : c ≤ b
⊢ a ≤ b - c ↔ c ≤ b - a
[PROOFSTEP]
rw [ha.le_tsub_iff_left h₁, hc.le_tsub_iff_right h₂]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : c ≤ b
⊢ a < b - c ↔ a + c < b
[PROOFSTEP]
refine' ⟨fun h' => (add_le_of_le_tsub_right_of_le h h'.le).lt_of_ne _, hc.lt_tsub_of_add_lt_right⟩
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : c ≤ b
h' : a < b - c
⊢ a + c ≠ b
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c d : α
hc : AddLECancellable c
h : c ≤ a + c
h' : a < a + c - c
⊢ False
[PROOFSTEP]
exact h'.ne' hc.add_tsub_cancel_right
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : c ≤ b
⊢ a < b - c ↔ c + a < b
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : c ≤ b
⊢ a < b - c ↔ a + c < b
[PROOFSTEP]
exact hc.lt_tsub_iff_right_of_le h
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hab : AddLECancellable (a - b)
h₁ : b ≤ a
h₂ : c ≤ a
h₃ : a - b = a - c
⊢ b = c
[PROOFSTEP]
rw [← hab.inj]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hab : AddLECancellable (a - b)
h₁ : b ≤ a
h₂ : c ≤ a
h₃ : a - b = a - c
⊢ a - b + b = a - b + c
[PROOFSTEP]
rw [tsub_add_cancel_of_le h₁, h₃, tsub_add_cancel_of_le h₂]
[GOAL]
α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
hb : AddLECancellable b
hca : c ≤ a
h : a - b < a - c
⊢ c < b
[PROOFSTEP]
conv_lhs at h => rw [← tsub_add_cancel_of_le hca]
[GOAL]
α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
hb : AddLECancellable b
hca : c ≤ a
h : a - b < a - c
| a - b
[PROOFSTEP]
rw [← tsub_add_cancel_of_le hca]
[GOAL]
α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
hb : AddLECancellable b
hca : c ≤ a
h : a - b < a - c
| a - b
[PROOFSTEP]
rw [← tsub_add_cancel_of_le hca]
[GOAL]
α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
hb : AddLECancellable b
hca : c ≤ a
h : a - b < a - c
| a - b
[PROOFSTEP]
rw [← tsub_add_cancel_of_le hca]
[GOAL]
α : Type u_1
inst✝⁶ : AddCommSemigroup α
inst✝⁵ : PartialOrder α
inst✝⁴ : ExistsAddOfLE α
inst✝³ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1
hb : AddLECancellable b
hca : c ≤ a
h : a - c + c - b < a - c
⊢ c < b
[PROOFSTEP]
exact lt_of_add_lt_add_left (hb.lt_add_of_tsub_lt_right h)
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : c ≤ a
h2 : a < b
⊢ a - c < b - c
[PROOFSTEP]
apply hc.lt_tsub_of_add_lt_left
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : c ≤ a
h2 : a < b
⊢ c + (a - c) < b
[PROOFSTEP]
rwa [add_tsub_cancel_of_le h]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hac : AddLECancellable (a - c)
h : c ≤ a
⊢ a + b = b + c + (a - c)
[PROOFSTEP]
rw [add_assoc, add_tsub_cancel_of_le h, add_comm]
[GOAL]
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hab : AddLECancellable (a - b)
h : b ≤ a
⊢ a - c - (a - b) = b - c
[PROOFSTEP]
rw [tsub_right_comm, hab.tsub_tsub_cancel_of_le h]
[GOAL]
α : Type u_1
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ b - a + a = b ↔ a ≤ b
[PROOFSTEP]
rw [add_comm]
[GOAL]
α : Type u_1
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ a + (b - a) = b ↔ a ≤ b
[PROOFSTEP]
exact add_tsub_cancel_iff_le
[GOAL]
α : Type u_1
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ a - b = 0 ↔ a ≤ b
[PROOFSTEP]
rw [← nonpos_iff_eq_zero, tsub_le_iff_left, add_zero]
[GOAL]
α : Type u_1
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ 0 < a - b ↔ ¬a ≤ b
[PROOFSTEP]
rw [pos_iff_ne_zero, Ne.def, tsub_eq_zero_iff_le]
[GOAL]
α : Type u_1
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
hc : AddLECancellable c
h : c ≤ a
⊢ a - b ≤ a - c ↔ c ≤ b
[PROOFSTEP]
refine' ⟨_, fun h => tsub_le_tsub_left h a⟩
[GOAL]
α : Type u_1
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
hc : AddLECancellable c
h : c ≤ a
⊢ a - b ≤ a - c → c ≤ b
[PROOFSTEP]
rw [tsub_le_iff_left, ← hc.add_tsub_assoc_of_le h, hc.le_tsub_iff_right (h.trans le_add_self), add_comm b]
[GOAL]
α : Type u_1
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
hc : AddLECancellable c
h : c ≤ a
⊢ a + c ≤ a + b → c ≤ b
[PROOFSTEP]
apply ha
[GOAL]
α : Type u_1
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
hb : AddLECancellable b
hc : AddLECancellable c
hba : b ≤ a
hca : c ≤ a
⊢ a - b = a - c ↔ b = c
[PROOFSTEP]
simp_rw [le_antisymm_iff, ha.tsub_le_tsub_iff_left hb hba, ha.tsub_le_tsub_iff_left hc hca, and_comm]
[GOAL]
α : Type u_1
inst✝³ : CanonicallyOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a b c d : α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
⊢ AddCommMonoid α
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝³ : CanonicallyOrderedAddMonoid α
inst✝² : Sub α
inst✝¹ : OrderedSub α
a✝ b✝ c✝ d : α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
src✝ : AddCommMonoid α := inferInstance
a b c : α
h : a + b = a + c
⊢ b = c
[PROOFSTEP]
simpa only [add_tsub_cancel_left] using congr_arg (fun x => x - a) h
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ 0 < a - b ↔ b < a
[PROOFSTEP]
rw [tsub_pos_iff_not_le, not_le]
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b✝ c d a b : α
⊢ a - b = a - min a b
[PROOFSTEP]
cases' le_total a b with h h
[GOAL]
case inl
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b✝ c d a b : α
h : a ≤ b
⊢ a - b = a - min a b
[PROOFSTEP]
rw [min_eq_left h, tsub_self, tsub_eq_zero_of_le h]
[GOAL]
case inr
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a✝ b✝ c d a b : α
h : b ≤ a
⊢ a - b = a - min a b
[PROOFSTEP]
rw [min_eq_right h]
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
hc : AddLECancellable c
h : c ≤ a
⊢ a - c < b - c ↔ a < b
[PROOFSTEP]
rw [hc.lt_tsub_iff_left, add_tsub_cancel_of_le h]
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
h₁ : 0 < a
h₂ : 0 < b
⊢ a - b < a
[PROOFSTEP]
refine' tsub_le_self.lt_of_ne fun h => _
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
h₁ : 0 < a
h₂ : 0 < b
h : a - b = a
⊢ False
[PROOFSTEP]
rw [← h, tsub_pos_iff_lt] at h₁ 
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
h₁ : b < a
h₂ : 0 < b
h : a - b = a
⊢ False
[PROOFSTEP]
exact h₂.not_le (ha.add_le_iff_nonpos_left.1 <| add_le_of_le_tsub_left_of_le h₁.le h.ge)
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
⊢ a - b < a ↔ 0 < a ∧ 0 < b
[PROOFSTEP]
refine' ⟨fun h => ⟨(zero_le _).trans_lt h, (zero_le b).lt_of_ne _⟩, fun h => ha.tsub_lt_self h.1 h.2⟩
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
ha : AddLECancellable a
h : a - b < a
⊢ 0 ≠ b
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c d : α
ha : AddLECancellable a
h : a - 0 < a
⊢ False
[PROOFSTEP]
rw [tsub_zero] at h 
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a c d : α
ha : AddLECancellable a
h : a < a
⊢ False
[PROOFSTEP]
exact h.false
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ a - b + b = max a b
[PROOFSTEP]
cases' le_total a b with h h
[GOAL]
case inl
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : a ≤ b
⊢ a - b + b = max a b
[PROOFSTEP]
rw [max_eq_right h, tsub_eq_zero_of_le h, zero_add]
[GOAL]
case inr
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : b ≤ a
⊢ a - b + b = max a b
[PROOFSTEP]
rw [max_eq_left h, tsub_add_cancel_of_le h]
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ a + (b - a) = max a b
[PROOFSTEP]
rw [add_comm, max_comm, tsub_add_eq_max]
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ a - min a b = a - b
[PROOFSTEP]
cases' le_total a b with h h
[GOAL]
case inl
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : a ≤ b
⊢ a - min a b = a - b
[PROOFSTEP]
rw [min_eq_left h, tsub_self, tsub_eq_zero_of_le h]
[GOAL]
case inr
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
h : b ≤ a
⊢ a - min a b = a - b
[PROOFSTEP]
rw [min_eq_right h]
[GOAL]
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ a - b + min a b = a
[PROOFSTEP]
rw [← tsub_min, @tsub_add_cancel_of_le]
[GOAL]
case h
α : Type u_1
inst✝² : CanonicallyLinearOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c d : α
⊢ min a b ≤ a
[PROOFSTEP]
apply min_le_left
