awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a c : α
h : c ≤ a
h2 : a - c < a - c
⊢ False

Tactic:
h2.false

Premises used: LT.lt.false
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a c : α
h : c ≤ a
h2 : a - c < a - c
⊢ False

Tactic:
exact h2.false

Premises used: LT.lt.false
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hab : b ≤ a
hcb : c ≤ b
⊢ a - c - (b - c) + (b - c) = a - c

Tactic:
tsub_add_cancel_of_le (tsub_le_tsub_right hab c)

Premises used: tsub_add_cancel_of_le, tsub_le_tsub_right
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hab : b ≤ a
hcb : c ≤ b
h : a - b = a - c - (b - c)
⊢ a - b + (b - c) = a - c

Tactic:
convert! tsub_add_cancel_of_le (tsub_le_tsub_right hab c) using 2

Premises used: tsub_add_cancel_of_le, tsub_le_tsub_right
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hab : b ≤ a
hcb : c ≤ b
h : a - b = a - (c + (b - c))
h₁ h₂ : a - b = a - b
⊢ a - b = a - c - (b - c)

Tactic:
rw [tsub_tsub, add_tsub_cancel_of_le hcb]

Premises used: tsub_tsub, add_tsub_cancel_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
h : c ≤ b
rw : a - (c + (b - c)) = a - b
rw₁ rw₂ : a - b = a - b
⊢ a - c - (b - c) = a - b

Tactic:
rw [tsub_tsub, add_tsub_cancel_of_le h]

Premises used: tsub_tsub, add_tsub_cancel_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
b c : α
hc : AddLECancellable c
h : c ≤ b
⊢ b - c + c = b

Tactic:
tsub_add_cancel_of_le h

Premises used: tsub_add_cancel_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
b c : α
hc : AddLECancellable c
h : c ≤ b
⊢ b - c + c = b

Tactic:
exact tsub_add_cancel_of_le h

Premises used: tsub_add_cancel_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hb : AddLECancellable b
h : b ≤ a
rw : c = a - b ↔ a = c + b
rw₁ : c + b = a ↔ a = c + b
rw₂ rw₃ : a = c + b ↔ a = c + b
⊢ a - b = c ↔ a = c + b

Tactic:
rw [eq_comm, hb.eq_tsub_iff_add_eq_of_le h, eq_comm]

Premises used: AddLECancellable.eq_tsub_iff_add_eq_of_le, eq_comm
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
b c : α
hc : AddLECancellable c
h : c ≤ b
a : α
rw : a + (b - c)
| a + b - c

Tactic:
rw [← add_tsub_cancel_of_le h, add_comm c, ← add_assoc, hc.add_tsub_cancel_right]

Premises used: add_assoc, add_comm, AddLECancellable.add_tsub_cancel_right, add_tsub_cancel_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
b c : α
hc : AddLECancellable c
h : c ≤ b
a : α
conv_lhs : a + b - c = a + (b - c)
conv_lhs₁ : a + (b - c) = a + (b - c)
⊢ a + b - c = a + (b - c)

Tactic:
conv_lhs => rw [← add_tsub_cancel_of_le h, add_comm c, ← add_assoc, hc.add_tsub_cancel_right]

Premises used: add_assoc, add_comm, AddLECancellable.add_tsub_cancel_right, add_tsub_cancel_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hb : AddLECancellable b
h : b ≤ a
rw : a - b + c = c + a - b
rw₁ : a - b + c = c + (a - b)
rw₂ rw₃ : c + (a - b) = c + (a - b)
⊢ a - b + c = a + c - b

Tactic:
rw [add_comm a, hb.add_tsub_assoc_of_le h, add_comm]

Premises used: add_comm, AddLECancellable.add_tsub_assoc_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hbc : AddLECancellable (b - c)
h₁ : b ≤ a
h₂ : c ≤ b
rw : a = a - b + (c + (b - c))
rw₁ : a = a - b + b
rw₂ rw₃ : a = a
⊢ a = a - b + c + (b - c)

Tactic:
rw [add_assoc, add_tsub_cancel_of_le h₂, tsub_add_cancel_of_le h₁]

Premises used: add_assoc, tsub_add_cancel_of_le, add_tsub_cancel_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c d : α
hb : AddLECancellable b
hd : AddLECancellable d
hba : b ≤ a
hdc : d ≤ c
rw : a + (c - d) - b = a + c - (b + d)
rw₁ : a + c - d - b = a + c - (b + d)
rw₂ : a + c - (d + b) = a + c - (b + d)
rw₃ rw₄ : a + c - (b + d) = a + c - (b + d)
⊢ a - b + (c - d) = a + c - (b + d)

Tactic:
rw [hb.tsub_add_eq_add_tsub hba, ← hd.add_tsub_assoc_of_le hdc, tsub_tsub, add_comm d]

Premises used: AddLECancellable.tsub_add_eq_add_tsub, add_comm, tsub_tsub, AddLECancellable.add_tsub_assoc_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
ha : AddLECancellable a
h : a ≤ c
⊢ b ≤ c - a ↔ a + b ≤ c

Tactic:
⟨add_le_of_le_tsub_left_of_le h, ha.le_tsub_of_add_le_left⟩

Premises used: Iff.intro, add_le_of_le_tsub_left_of_le, AddLECancellable.le_tsub_of_add_le_left
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
ha : AddLECancellable a
h : a ≤ c
rw : b ≤ c - a ↔ a + b ≤ c
⊢ b ≤ c - a ↔ b + a ≤ c

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
ha : AddLECancellable a
h : a ≤ c
⊢ b ≤ c - a ↔ a + b ≤ c

Tactic:
ha.le_tsub_iff_left h

Premises used: AddLECancellable.le_tsub_iff_left
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
ha : AddLECancellable a
h : a ≤ c
⊢ b ≤ c - a ↔ a + b ≤ c

Tactic:
exact ha.le_tsub_iff_left h

Premises used: AddLECancellable.le_tsub_iff_left
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a - b < c ↔ a < b + c

Tactic:
⟨hb.lt_add_of_tsub_lt_left, ?_⟩

Premises used: Iff.intro, AddLECancellable.lt_add_of_tsub_lt_left
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hb : AddLECancellable b
hba : b ≤ a
refine : a < b + c → a - b < c
⊢ a - b < c ↔ a < b + c

Tactic:
refine ⟨hb.lt_add_of_tsub_lt_left, ?_⟩
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + c
⊢ a - b < c

Tactic:
(tsub_le_iff_left.mpr h.le).lt_of_ne ?_

Premises used: Iff.mpr, LT.lt.le, tsub_le_iff_left, LE.le.lt_of_ne
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + c
refine : a - b ≠ c
⊢ a - b < c

Tactic:
refine (tsub_le_iff_left.mpr h.le).lt_of_ne ?_

Premises used: Iff.mpr, LT.lt.le, tsub_le_iff_left, LE.le.lt_of_ne
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + (a - b)
⊢ False

Tactic:
h.ne' (add_tsub_cancel_of_le hba)

Premises used: LT.lt.ne', add_tsub_cancel_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + (a - b)
⊢ False

Tactic:
exact h.ne' (add_tsub_cancel_of_le hba)

Premises used: LT.lt.ne', add_tsub_cancel_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hb : AddLECancellable b
hba : b ≤ a
rw : a - b < c ↔ a < b + c
⊢ a - b < c ↔ a < c + b

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a - b < c ↔ a < b + c

Tactic:
hb.tsub_lt_iff_left hba

Premises used: AddLECancellable.tsub_lt_iff_left
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a - b < c ↔ a < b + c

Tactic:
exact hb.tsub_lt_iff_left hba

Premises used: AddLECancellable.tsub_lt_iff_left
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hb : AddLECancellable b
hc : AddLECancellable c
h₁ : b ≤ a
h₂ : c ≤ a
rw : a < b + c ↔ a - c < b
rw₁ rw₂ : a < b + c ↔ a < b + c
⊢ a - b < c ↔ a - c < b

Tactic:
rw [hb.tsub_lt_iff_left h₁, hc.tsub_lt_iff_right h₂]

Premises used: AddLECancellable.tsub_lt_iff_left, AddLECancellable.tsub_lt_iff_right
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
ha : AddLECancellable a
hc : AddLECancellable c
h₁ : a ≤ b
h₂ : c ≤ b
rw : a ≤ b - c ↔ a + c ≤ b
rw₁ rw₂ : a + c ≤ b ↔ a + c ≤ b
⊢ a ≤ b - c ↔ c ≤ b - a

Tactic:
rw [ha.le_tsub_iff_left h₁, hc.le_tsub_iff_right h₂]

Premises used: AddLECancellable.le_tsub_iff_right, AddLECancellable.le_tsub_iff_left
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ b
⊢ a < b - c ↔ a + c < b

Tactic:
⟨fun h' => (add_le_of_le_tsub_right_of_le h h'.le).lt_of_ne ?_, hc.lt_tsub_of_add_lt_right⟩

Premises used: LT.lt.le, LE.le.lt_of_ne, add_le_of_le_tsub_right_of_le, AddLECancellable.lt_tsub_of_add_lt_right, Iff.intro
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ b
refine : ∀ (h' : a < b - c), a + c ≠ b
⊢ a < b - c ↔ a + c < b

Tactic:
refine ⟨fun h' => (add_le_of_le_tsub_right_of_le h h'.le).lt_of_ne ?_, hc.lt_tsub_of_add_lt_right⟩
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a c : α
hc : AddLECancellable c
h : c ≤ a + c
h' : a < a + c - c
⊢ False

Tactic:
h'.ne' hc.add_tsub_cancel_right

Premises used: LT.lt.ne', AddLECancellable.add_tsub_cancel_right
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a c : α
hc : AddLECancellable c
h : c ≤ a + c
h' : a < a + c - c
⊢ False

Tactic:
exact h'.ne' hc.add_tsub_cancel_right

Premises used: LT.lt.ne', AddLECancellable.add_tsub_cancel_right
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ b
rw : a < b - c ↔ a + c < b
⊢ a < b - c ↔ c + a < b

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ b
⊢ a < b - c ↔ a + c < b

Tactic:
hc.lt_tsub_iff_right_of_le h

Premises used: AddLECancellable.lt_tsub_iff_right_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ b
⊢ a < b - c ↔ a + c < b

Tactic:
exact hc.lt_tsub_iff_right_of_le h

Premises used: AddLECancellable.lt_tsub_iff_right_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hab : AddLECancellable (a - b)
h₁ : b ≤ a
h₂ : c ≤ a
h₃ : a - b = a - c
rw : a - b + b = a - b + c
⊢ b = c

Tactic:
rw [← hab.inj]

Premises used: AddLECancellable.inj
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hab : AddLECancellable (a - b)
h₁ : b ≤ a
h₂ : c ≤ a
h₃ : a - b = a - c
rw : a = a - b + c
rw₁ : a = a - c + c
rw₂ rw₃ : a = a
⊢ a - b + b = a - b + c

Tactic:
rw [tsub_add_cancel_of_le h₁, h₃, tsub_add_cancel_of_le h₂]

Premises used: tsub_add_cancel_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLT α
hb : AddLECancellable b
hca : c ≤ a
h : a - b < a - c
rw : a - c + c - b
| a - b

Tactic:
rw [← tsub_add_cancel_of_le hca]

Premises used: tsub_add_cancel_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLT α
hb : AddLECancellable b
hca : c ≤ a
h : a - b < a - c
⊢ a - c + c - b < a - c

Tactic:
conv_lhs at h => rw [← tsub_add_cancel_of_le hca]

Premises used: tsub_add_cancel_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLT α
hb : AddLECancellable b
hca : c ≤ a
h : a - c + c - b < a - c
⊢ c < b

Tactic:
lt_of_add_lt_add_left (hb.lt_add_of_tsub_lt_right h)

Premises used: lt_of_add_lt_add_left, AddLECancellable.lt_add_of_tsub_lt_right
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLT α
hb : AddLECancellable b
hca : c ≤ a
h : a - c + c - b < a - c
⊢ c < b

Tactic:
exact lt_of_add_lt_add_left (hb.lt_add_of_tsub_lt_right h)

Premises used: lt_of_add_lt_add_left, AddLECancellable.lt_add_of_tsub_lt_right
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hab : AddLECancellable (a - b)
h₁ : b ≤ a
h : c < b
⊢ a - b < a - c

Tactic:
(tsub_le_tsub_left h.le _).lt_of_ne fun h' => h.ne' <| hab.tsub_inj_right h₁ (h.le.trans h₁) h'

Premises used: LT.lt.le, tsub_le_tsub_left, LE.le.lt_of_ne, LT.lt.ne', LE.le.trans, AddLECancellable.tsub_inj_right
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ a
h2 : a < b
apply : c + (a - c) < b
⊢ a - c < b - c

Tactic:
apply hc.lt_tsub_of_add_lt_left

Premises used: AddLECancellable.lt_tsub_of_add_lt_left
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ a
h2 rwa rwa₁ rwa₂ rwa₃ : a < b
⊢ c + (a - c) < b

Tactic:
rwa [add_tsub_cancel_of_le h]

Premises used: add_tsub_cancel_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLT α
hb : AddLECancellable b
hab : AddLECancellable (a - b)
h₁ : b ≤ a
h₂ : c ≤ a
⊢ a - b < a - c ↔ c < b

Tactic:
⟨hb.lt_of_tsub_lt_tsub_left_of_le h₂, hab.tsub_lt_tsub_left_of_le h₁⟩

Premises used: AddLECancellable.tsub_lt_tsub_left_of_le, AddLECancellable.lt_of_tsub_lt_tsub_left_of_le, Iff.intro
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hc : AddLECancellable c
hcb : c ≤ b
rw : a + c + b - c = a + b
rw₁ : a + b + c - c = a + b
rw₂ rw₃ : a + b = a + b
⊢ a + c + (b - c) = a + b

Tactic:
rw [← hc.add_tsub_assoc_of_le hcb, add_right_comm, hc.add_tsub_cancel_right]

Premises used: add_right_comm, AddLECancellable.add_tsub_cancel_right, AddLECancellable.add_tsub_assoc_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hac : AddLECancellable (a - c)
h : c ≤ a
rw : a + b = b + (c + (a - c))
rw₁ : a + b = b + a
rw₂ rw₃ : b + a = b + a
⊢ a + b = b + c + (a - c)

Tactic:
rw [add_assoc, add_tsub_cancel_of_le h, add_comm]

Premises used: add_assoc, add_comm, add_tsub_cancel_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b : α
hba : AddLECancellable (b - a)
h : a ≤ b
⊢ b - (b - a) = a

Tactic:
hba.tsub_eq_of_eq_add (add_tsub_cancel_of_le h).symm

Premises used: AddLECancellable.tsub_eq_of_eq_add, Eq.symm, add_tsub_cancel_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
hab : AddLECancellable (a - b)
h : b ≤ a
rw : a - (a - b) - c = b - c
rw₁ rw₂ : b - c = b - c
⊢ a - c - (a - b) = b - c

Tactic:
rw [tsub_right_comm, hab.tsub_tsub_cancel_of_le h]

Premises used: tsub_right_comm, AddLECancellable.tsub_tsub_cancel_of_le
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLE α
h : c ≤ b
⊢ a = b - c ↔ a + c = b

Tactic:
Contravariant.AddLECancellable.eq_tsub_iff_add_eq_of_le h

Premises used: AddLECancellable.eq_tsub_iff_add_eq_of_le, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLE α
h : b ≤ a
⊢ a - b = c ↔ a = c + b

Tactic:
Contravariant.AddLECancellable.tsub_eq_iff_eq_add_of_le h

Premises used: AddLECancellable.tsub_eq_iff_eq_add_of_le, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
b c : α
inst_6 : AddLeftReflectLE α
h : c ≤ b
a : α
⊢ a + b - c = a + (b - c)

Tactic:
Contravariant.AddLECancellable.add_tsub_assoc_of_le h a

Premises used: AddLECancellable.add_tsub_assoc_of_le, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLE α
h : b ≤ a
⊢ a - b + c = a + c - b

Tactic:
Contravariant.AddLECancellable.tsub_add_eq_add_tsub h

Premises used: AddLECancellable.tsub_add_eq_add_tsub, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLE α
h₁ : b ≤ a
h₂ : c ≤ b
⊢ a - (b - c) = a - b + c

Tactic:
Contravariant.AddLECancellable.tsub_tsub_assoc h₁ h₂

Premises used: AddLECancellable.tsub_tsub_assoc, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c d : α
inst_6 : AddLeftReflectLE α
hba : b ≤ a
hdc : d ≤ c
⊢ a - b + (c - d) = a + c - (b + d)

Tactic:
Contravariant.AddLECancellable.tsub_add_tsub_comm Contravariant.AddLECancellable hba hdc

Premises used: AddLECancellable.tsub_add_tsub_comm, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic
Goal:
α : Type u_1
inst : AddCommSemigroup α
inst_1 : PartialOrder α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
a b c : α
inst_6 : AddLeftReflectLE α
h : a ≤ c
⊢ b ≤ c - a ↔ a + b ≤ c

Tactic:
Contravariant.AddLECancellable.le_tsub_iff_left h

Premises used: AddLECancellable.le_tsub_iff_left, Contravariant.AddLECancellable