awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b : α
hb : AddLECancellable b
⊢ a ≤ b + a - b

Tactic:
exact hb.le_add_tsub_swap

Premises used: AddLECancellable.le_add_tsub_swap
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
ha : AddLECancellable a
h : a + b ≤ c
⊢ b ≤ c - a

Tactic:
ha <| h.trans le_add_tsub

Premises used: LE.le.trans, le_add_tsub
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
hb : AddLECancellable b
h rwa rwa₁ rwa₂ rwa₃ : a + b ≤ c
⊢ b + a ≤ c

Tactic:
rwa [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b : α
inst_4 : AddLeftReflectLE α
⊢ a ≤ b + a - b

Tactic:
Contravariant.AddLECancellable.le_add_tsub_swap

Premises used: AddLECancellable.le_add_tsub_swap, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b : α
inst_4 : AddLeftReflectLE α
⊢ a ≤ a + b - b

Tactic:
Contravariant.AddLECancellable.le_add_tsub

Premises used: AddLECancellable.le_add_tsub, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
inst_4 : AddLeftReflectLE α
h : a + b ≤ c
⊢ b ≤ c - a

Tactic:
Contravariant.AddLECancellable.le_tsub_of_add_le_left h

Premises used: AddLECancellable.le_tsub_of_add_le_left, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
inst_4 : AddLeftReflectLE α
h : a + b ≤ c
⊢ a ≤ c - b

Tactic:
Contravariant.AddLECancellable.le_tsub_of_add_le_right h

Premises used: AddLECancellable.le_tsub_of_add_le_right, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommMonoid α
inst_2 : Sub α
inst_3 : OrderedSub α
a b : α
rw : a ≤ b + 0 ↔ a ≤ b
rw₁ rw₂ : a ≤ b ↔ a ≤ b
⊢ a - b ≤ 0 ↔ a ≤ b

Tactic:
rw [tsub_le_iff_left, add_zero]

Premises used: tsub_le_iff_left, add_zero
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
b a c : α
a₁ : b - a - c ≤ b - (a + c)
a₂ : b - (a + c) ≤ b - a - c
⊢ b - a - c = b - (a + c)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
b a c : α
a₁ : b - a ≤ c + (b - (a + c))
a₂ : b ≤ a + (c + (b - (a + c)))
a₃ : b ≤ a + c + (b - (a + c))
a₄ a₅ : b - (a + c) ≤ b - (a + c)
⊢ b - a - c ≤ b - (a + c)

Tactic:
rw [tsub_le_iff_left, tsub_le_iff_left, ← add_assoc, ← tsub_le_iff_left]

Premises used: add_assoc, tsub_le_iff_left
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
b a c : α
a₁ : b ≤ a + c + (b - a - c)
a₂ : b ≤ a + (c + (b - a - c))
a₃ : b - a ≤ c + (b - a - c)
a₄ a₅ : b - a - c ≤ b - a - c
⊢ b - (a + c) ≤ b - a - c

Tactic:
rw [tsub_le_iff_left, add_assoc, ← tsub_le_iff_left, ← tsub_le_iff_left]

Premises used: add_assoc, tsub_le_iff_left
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
⊢ a - (b + c) = a - b - c

Tactic:
(tsub_tsub _ _ _).symm

Premises used: tsub_tsub, Eq.symm
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
rw : a - (c + b) = a - c - b
⊢ a - (b + c) = a - c - b

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
⊢ a - (c + b) = a - c - b

Tactic:
apply tsub_add_eq_tsub_tsub

Premises used: tsub_add_eq_tsub_tsub
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
rw : a - (b + c) = a - c - b
rw₁ rw₂ : a - c - b = a - c - b
⊢ a - b - c = a - c - b

Tactic:
rw [← tsub_add_eq_tsub_tsub, tsub_add_eq_tsub_tsub_swap]

Premises used: tsub_add_eq_tsub_tsub_swap, tsub_add_eq_tsub_tsub
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
hb : AddLECancellable b
h : a = c + b
rw : c ≤ c + b - b
⊢ c ≤ a - b

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
hb : AddLECancellable b
h : a = c + b
⊢ c ≤ c + b - b

Tactic:
hb.le_add_tsub

Premises used: AddLECancellable.le_add_tsub
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
hb : AddLECancellable b
h : a = c + b
⊢ c ≤ c + b - b

Tactic:
exact hb.le_add_tsub

Premises used: AddLECancellable.le_add_tsub
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
hc : AddLECancellable c
h : a + c = b
⊢ a = b - c

Tactic:
(hc.tsub_eq_of_eq_add h.symm).symm

Premises used: AddLECancellable.tsub_eq_of_eq_add, Eq.symm
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
inst_4 : AddLeftMono α
hb : AddLECancellable b
h : a + c = b
⊢ a = b - c

Tactic:
(hb.tsub_eq_of_eq_add' h.symm).symm

Premises used: AddLECancellable.tsub_eq_of_eq_add', Eq.symm
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
hb : AddLECancellable b
h rw : a = b + c
rw₁ rw₂ : b + c = b + c
⊢ a = c + b

Tactic:
rw [add_comm, h]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
inst_4 : AddLeftMono α
ha : AddLECancellable a
h rw : a = b + c
rw₁ rw₂ : b + c = b + c
⊢ a = c + b

Tactic:
rw [add_comm, h]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b : α
hb : AddLECancellable b
rw rw₁ : b + a = b + a
⊢ a + b = a + b

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b : α
ha : AddLECancellable a
⊢ a + b - a = b

Tactic:
ha.tsub_eq_of_eq_add <| add_comm a b

Premises used: add_comm, AddLECancellable.tsub_eq_of_eq_add
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
hb : AddLECancellable b
h : a - b < c
rw : a - b ≤ c ∧ a ≠ b + c
⊢ a < b + c

Tactic:
rw [lt_iff_le_and_ne, ← tsub_le_iff_left]

Premises used: lt_iff_le_and_ne, tsub_le_iff_left
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
hb : AddLECancellable b
h : a - b < c
⊢ a - b ≤ c ∧ a ≠ b + c

Tactic:
⟨h.le, ?_⟩

Premises used: LT.lt.le, And.intro
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
hb : AddLECancellable b
h : a - b < c
refine : a ≠ b + c
⊢ a - b ≤ c ∧ a ≠ b + c

Tactic:
refine ⟨h.le, ?_⟩
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
b c : α
hb : AddLECancellable b
h : b + c - b < c
⊢ False

Tactic:
simp [hb] at h
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
hc : AddLECancellable c
h : a - c < b
rw : a - c ≤ b ∧ a ≠ b + c
⊢ a < b + c

Tactic:
rw [lt_iff_le_and_ne, ← tsub_le_iff_right]

Premises used: lt_iff_le_and_ne, tsub_le_iff_right
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
hc : AddLECancellable c
h : a - c < b
⊢ a - c ≤ b ∧ a ≠ b + c

Tactic:
⟨h.le, ?_⟩

Premises used: LT.lt.le, And.intro
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
hc : AddLECancellable c
h : a - c < b
refine : a ≠ b + c
⊢ a - c ≤ b ∧ a ≠ b + c

Tactic:
refine ⟨h.le, ?_⟩
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
b c : α
hc : AddLECancellable c
h : b + c - c < b
⊢ False

Tactic:
simp [hc] at h
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
b c : α
hc : AddLECancellable c
h : b - c + c < b
⊢ False

Tactic:
h.not_ge le_tsub_add

Premises used: le_tsub_add, LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
b c : α
hc : AddLECancellable c
h : b - c + c < b
⊢ False

Tactic:
exact h.not_ge le_tsub_add

Premises used: le_tsub_add, LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
ha : AddLECancellable a
h rwa rwa₁ rwa₂ rwa₃ : a + c < b
⊢ c + a < b

Tactic:
rwa [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
inst_4 : AddLeftReflectLE α
h : a = c + b
⊢ a - b = c

Tactic:
Contravariant.AddLECancellable.tsub_eq_of_eq_add h

Premises used: AddLECancellable.tsub_eq_of_eq_add, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
inst_4 : AddLeftReflectLE α
h : a + c = b
⊢ a = b - c

Tactic:
Contravariant.AddLECancellable.eq_tsub_of_add_eq h

Premises used: AddLECancellable.eq_tsub_of_add_eq, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
inst_4 : AddLeftReflectLE α
h : a = b + c
⊢ a - b = c

Tactic:
Contravariant.AddLECancellable.tsub_eq_of_eq_add_rev h

Premises used: Contravariant.AddLECancellable, AddLECancellable.tsub_eq_of_eq_add_rev
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
inst_4 : AddLeftReflectLE α
a b : α
⊢ a + b - b = a

Tactic:
Contravariant.AddLECancellable.add_tsub_cancel_right

Premises used: AddLECancellable.add_tsub_cancel_right, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
inst_4 : AddLeftReflectLE α
a b : α
⊢ a + b - a = b

Tactic:
Contravariant.AddLECancellable.add_tsub_cancel_left

Premises used: Contravariant.AddLECancellable, AddLECancellable.add_tsub_cancel_left
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c d : α
inst_4 : AddLeftReflectLE α
h : a + d = c + b
rw rw₁ : a - b = a - b
⊢ a - b = a + d - d - b

Tactic:
rw [add_tsub_cancel_right]

Premises used: add_tsub_cancel_right
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c d : α
inst_4 : AddLeftReflectLE α
h : a + d = c + b
rw : c + b - d - b = c + b - b - d
rw₁ rw₂ : c + b - b - d = c + b - b - d
⊢ a + d - d - b = c + b - b - d

Tactic:
rw [h, tsub_right_comm]

Premises used: tsub_right_comm
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c d : α
inst_4 : AddLeftReflectLE α
h : a + d = c + b
rw rw₁ : c - d = c - d
⊢ c + b - b - d = c - d

Tactic:
rw [add_tsub_cancel_right]

Premises used: add_tsub_cancel_right
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c d : α
inst_4 : AddLeftReflectLE α
h : a + d = c + b
calc : a - b = a + d - d - b
calc₁ : a + d - d - b = c + b - b - d
calc₂ : c + b - b - d = c - d
⊢ a - b = c - d

Tactic:
calc a - b = a + d - d - b := by rw [add_tsub_cancel_right]
           _ = c + b - b - d := by rw [h, tsub_right_comm]
           _ = c - d := by rw [add_tsub_cancel_right]
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
inst_4 : AddLeftReflectLE α
h : a - b < c
⊢ a < b + c

Tactic:
Contravariant.AddLECancellable.lt_add_of_tsub_lt_left h

Premises used: Contravariant.AddLECancellable, AddLECancellable.lt_add_of_tsub_lt_left
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
inst_4 : AddLeftReflectLE α
h : a - c < b
⊢ a < b + c

Tactic:
Contravariant.AddLECancellable.lt_add_of_tsub_lt_right h

Premises used: Contravariant.AddLECancellable, AddLECancellable.lt_add_of_tsub_lt_right
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
inst_4 : AddLeftReflectLE α
⊢ a + c < b → c < b - a

Tactic:
Contravariant.AddLECancellable.lt_tsub_of_add_lt_left

Premises used: AddLECancellable.lt_tsub_of_add_lt_left, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
inst_4 : AddLeftReflectLE α
⊢ a + c < b → a < b - c

Tactic:
Contravariant.AddLECancellable.lt_tsub_of_add_lt_right

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

Tactic:
add_tsub_add_le_tsub_right.antisymm (tsub_le_iff_right.2 <| ?_)

Premises used: Iff.mpr, LE.le.antisymm, tsub_le_iff_right, add_tsub_add_le_tsub_right
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
inst_4 : AddLeftMono α
inst_5 : AddLeftReflectLE α
a c b : α
refine : a ≤ a + c - (b + c) + b
⊢ a + c - (b + c) = a - b

Tactic:
refine add_tsub_add_le_tsub_right.antisymm (tsub_le_iff_right.2 <| ?_)

Premises used: Iff.mpr, LE.le.antisymm, tsub_le_iff_right, add_tsub_add_le_tsub_right
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
inst_4 : AddLeftMono α
inst_5 : AddLeftReflectLE α
a c b : α
bc : a + c ≤ a + c - (b + c) + b + c
a₁ : α
⊢ a ≤ a + c - (b + c) + b

Tactic:
apply le_of_add_le_add_right

Premises used: le_of_add_le_add_right
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
inst_4 : AddLeftMono α
inst_5 : AddLeftReflectLE α
a c b : α
⊢ a + c ≤ a + c - (b + c) + (b + c)

Tactic:
le_tsub_add

Premises used: le_tsub_add
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
inst_4 : AddLeftMono α
inst_5 : AddLeftReflectLE α
a b c : α
rw : b + a - (a + c) = b - c
rw₁ : b + a - (c + a) = b - c
rw₂ rw₃ : b - c = b - c
⊢ a + b - (a + c) = b - c

Tactic:
rw [add_comm a b, add_comm a c, add_tsub_add_eq_tsub_right]

Premises used: add_comm, add_tsub_add_eq_tsub_right
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
a b c : α
inst : LinearOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
h : a - c < b - c
⊢ a < b

Tactic:
lt_imp_lt_of_le_imp_le (fun h => tsub_le_tsub_right h c) h

Premises used: tsub_le_tsub_right, lt_imp_lt_of_le_imp_le
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
a b c : α
inst : LinearOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
⊢ a < b - c ↔ a + c < b

Tactic:
lt_iff_lt_of_le_iff_le tsub_le_iff_right

Premises used: tsub_le_iff_right, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
a b c : α
inst : LinearOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
⊢ a < b - c ↔ c + a < b

Tactic:
lt_iff_lt_of_le_iff_le tsub_le_iff_left

Premises used: tsub_le_iff_left, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
a b c : α
inst : LinearOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
⊢ a < b - c ↔ c < b - a

Tactic:
lt_tsub_iff_left.trans lt_tsub_iff_right.symm

Premises used: lt_tsub_iff_right, Iff.trans, Iff.symm, lt_tsub_iff_left
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
a b c : α
inst : LinearOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
inst_4 : AddLeftMono α
h : a - b < a - c
⊢ c < b

Tactic:
lt_imp_lt_of_le_imp_le (fun h => tsub_le_tsub_left h a) h

Premises used: tsub_le_tsub_left, lt_imp_lt_of_le_imp_le
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommMonoid α
inst_2 : Sub α
inst_3 : OrderedSub α
a : α
⊢ a - 0 = a

Tactic:
AddLECancellable.tsub_eq_of_eq_add addLECancellable_zero (add_zero _).symm

Premises used: addLECancellable_zero, add_zero, AddLECancellable.tsub_eq_of_eq_add, Eq.symm
-- 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 : α
h : a ≤ b
⊢ a + (b - a) = b

Tactic:
le_antisymm ?_ le_add_tsub

Premises used: le_antisymm, le_add_tsub
-- 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 : α
h : a ≤ b
refine : a + (b - a) ≤ b
⊢ a + (b - a) = b

Tactic:
refine le_antisymm ?_ le_add_tsub

Premises used: le_antisymm, le_add_tsub
-- 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 : α
h : a ≤ b
obtain : ∀ (c : α) (h : a ≤ a + c), a + (a + c - a) ≤ a + c
⊢ a + (b - a) ≤ b

Tactic:
obtain ⟨c, rfl⟩ := exists_add_of_le h

Premises used: ExistsAddOfLE.exists_add_of_le, rfl
-- 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 : a ≤ a + c
grw grw₁ : a + c ≤ a + c
⊢ a + (a + c - a) ≤ a + c

Tactic:
grw [add_tsub_le_left]

Premises used: add_tsub_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 : α
h : a ≤ b
rw : a + (b - a) = b
⊢ b - a + 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 : α
h : a ≤ b
⊢ a + (b - a) = b

Tactic:
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 : α
h : a ≤ b
⊢ a + (b - a) = b

Tactic:
exact 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 : α
h : b ≤ c
h2 : a ≤ c - b
grw : c - b + b ≤ c
grw₁ grw₂ : c ≤ c
⊢ a + b ≤ c

Tactic:
grw [h2, 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 : α
h : a ≤ c
h2 : b ≤ c - a
grw : a + (c - a) ≤ c
grw₁ grw₂ : c ≤ c
⊢ a + b ≤ c

Tactic:
grw [h2, 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 : α
h : c ≤ b
rw : a ≤ b - c + c ↔ a ≤ b
rw₁ rw₂ : a ≤ b ↔ a ≤ b
⊢ a - c ≤ b - c ↔ a ≤ b

Tactic:
rw [tsub_le_iff_right, tsub_add_cancel_of_le h]

Premises used: tsub_add_cancel_of_le, tsub_le_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 : α
h1 : c ≤ a
h2 : c ≤ b
simp_rw : a - c ≤ b - c ∧ b - c ≤ a - c ↔ a ≤ b ∧ b ≤ a
simp_rw₁ : a - c ≤ b - c ∧ b ≤ a ↔ a ≤ b ∧ b ≤ a
⊢ a - c = b - c ↔ a = b

Tactic:
simp_rw [le_antisymm_iff, tsub_le_tsub_iff_right h1, tsub_le_tsub_iff_right h2]

Premises used: tsub_le_tsub_iff_right, le_antisymm_iff
-- 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₁ : a ≤ b
h₂ : a ≤ c
⊢ b - a = c - a → b = c

Tactic:
(tsub_left_inj h₁ h₂).1

Premises used: tsub_left_inj, Iff.mp
-- 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
h2 : a - c < b - c
⊢ a < b

Tactic:
((tsub_le_tsub_iff_right h).mp h2.le).lt_of_ne ?_

Premises used: LT.lt.le, tsub_le_tsub_iff_right, LE.le.lt_of_ne, Iff.mp
-- 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
h2 : a - c < b - c
refine : a ≠ b
⊢ a < b

Tactic:
refine ((tsub_le_tsub_iff_right h).mp h2.le).lt_of_ne ?_

Premises used: LT.lt.le, tsub_le_tsub_iff_right, LE.le.lt_of_ne, Iff.mp