awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
ha : AddLECancellable a
refine : ∀ (h : a - b < a), b ≠ 0
⊢ a - b < a ↔ 0 < a ∧ 0 < b

Tactic:
refine ⟨fun h => ⟨h.pos, pos_of_ne_zero ?_⟩, fun h => ha.tsub_lt_self h.1 h.2⟩
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a : α
ha : AddLECancellable a
h : a - 0 < a
⊢ a < a

Tactic:
rw [tsub_zero] at h

Premises used: tsub_zero
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a : α
ha : AddLECancellable a
h : a < a
⊢ False

Tactic:
h.false

Premises used: LT.lt.false
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a : α
ha : AddLECancellable a
h : a < a
⊢ False

Tactic:
exact h.false

Premises used: LT.lt.false
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b c : α
ha : AddLECancellable a
hb : AddLECancellable b
h : b ≤ a
⊢ a - b < a - c ↔ c < b

Tactic:
lt_iff_lt_of_le_iff_le <| ha.tsub_le_tsub_iff_left hb h

Premises used: AddLECancellable.tsub_le_tsub_iff_left, lt_iff_lt_of_le_iff_le
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b c : α
inst_5 : AddLeftReflectLE α
h : c ≤ a
⊢ a - c < b - c ↔ a < b

Tactic:
Contravariant.AddLECancellable.tsub_lt_tsub_iff_right h

Premises used: AddLECancellable.tsub_lt_tsub_iff_right, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
inst_5 : AddLeftReflectLE α
⊢ 0 < a → 0 < b → a - b < a

Tactic:
Contravariant.AddLECancellable.tsub_lt_self

Premises used: AddLECancellable.tsub_lt_self, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
inst_5 : AddLeftReflectLE α
⊢ a - b < a ↔ 0 < a ∧ 0 < b

Tactic:
Contravariant.AddLECancellable.tsub_lt_self_iff

Premises used: Contravariant.AddLECancellable, AddLECancellable.tsub_lt_self_iff
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b c : α
inst_5 : AddLeftReflectLE α
h : b ≤ a
⊢ a - b < a - c ↔ c < b

Tactic:
Contravariant.AddLECancellable.tsub_lt_tsub_iff_left_of_le Contravariant.AddLECancellable h

Premises used: AddLECancellable.tsub_lt_tsub_iff_left_of_le, Contravariant.AddLECancellable
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
inst_5 : AddLeftReflectLE α
a b : α
rw : a - (a - min a b) = min a b
rw₁ rw₂ : min a b = min a b
⊢ a - (a - b) = min a b

Tactic:
rw [tsub_eq_tsub_min _ b, tsub_tsub_cancel_of_le (min_le_left a _)]

Premises used: tsub_eq_tsub_min, min_le_left, tsub_tsub_cancel_of_le
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
inl : ∀ (h : a ≤ b), a - b + b = max a b
inr : ∀ (h : b ≤ a), a - b + b = max a b
⊢ a - b + b = max a b

Tactic:
rcases le_total a b with h | h

Premises used: le_total
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
h : a ≤ b
inl : a - b + b = b
inl₁ : 0 + b = b
inl₂ inl₃ : b = b
⊢ a - b + b = max a b

Tactic:
rw [max_eq_right h, tsub_eq_zero_of_le h, zero_add]

Premises used: tsub_eq_zero_of_le, zero_add, max_eq_right
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
h : b ≤ a
inr : a - b + b = a
inr₁ inr₂ : a = a
⊢ a - b + b = max a b

Tactic:
rw [max_eq_left h, tsub_add_cancel_of_le h]

Premises used: tsub_add_cancel_of_le, max_eq_left
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
rw : b - a + a = max a b
rw₁ : b - a + a = max b a
rw₂ rw₃ : max b a = max b a
⊢ a + (b - a) = max a b

Tactic:
rw [add_comm, max_comm, tsub_add_eq_max]

Premises used: add_comm, tsub_add_eq_max, max_comm
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
⊢ a - min a b = a - b

Tactic:
(tsub_eq_tsub_min a b).symm

Premises used: tsub_eq_tsub_min, Eq.symm
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
h : min a b ≤ a
⊢ a - b + min a b = a

Tactic:
rw [← tsub_min, @tsub_add_cancel_of_le]

Premises used: tsub_add_cancel_of_le, tsub_min
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
⊢ min a b ≤ a

Tactic:
apply min_le_left

Premises used: min_le_left
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
inst_5 : AddLeftReflectLE α
m n : α
hm : Even m
hn : Even n
obtain : ∀ (a : α), Even (a + a - n)
⊢ Even (m - n)

Tactic:
obtain ⟨a, rfl⟩ := hm

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
inst_5 : AddLeftReflectLE α
n : α
hn : Even n
a : α
obtain : ∀ (b : α), Even (a + a - (b + b))
⊢ Even (a + a - n)

Tactic:
obtain ⟨b, rfl⟩ := hn

Premises used: rfl
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
inst_5 : AddLeftReflectLE α
a b : α
⊢ Even (a + a - (b + b))

Tactic:
⟨a - b, ?_⟩

Premises used: HSub.hSub, Even, Exists.intro
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
inst_5 : AddLeftReflectLE α
a b : α
refine : a + a - (b + b) = a - b + (a - b)
⊢ Even (a + a - (b + b))

Tactic:
refine ⟨a - b, ?_⟩
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
inst_5 : AddLeftReflectLE α
a b : α
inl : ∀ (h : a ≤ b), a + a - (b + b) = a - b + (a - b)
inr : ∀ (h : b ≤ a), a + a - (b + b) = a - b + (a - b)
⊢ a + a - (b + b) = a - b + (a - b)

Tactic:
obtain h | h := le_total a b

Premises used: le_total
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
inst_5 : AddLeftReflectLE α
a b : α
h : a ≤ b
inl : a + a - (b + b) = HAdd.hAdd (α := α) 0 0
inl₁ : 0 = HAdd.hAdd (α := α) 0 0
inl₂ inl₃ : Eq.{u_1 + 1} (α := α) 0 0
⊢ a + a - (b + b) = a - b + (a - b)

Tactic:
rw [tsub_eq_zero_of_le h, tsub_eq_zero_of_le (add_le_add h h), add_zero]

Premises used: tsub_eq_zero_of_le, add_le_add, add_zero
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
inst_5 : AddLeftReflectLE α
a b : α
h : b ≤ a
⊢ a + a - (b + b) = a - b + (a - b)

Tactic:
(tsub_add_tsub_comm h h).symm

Premises used: tsub_add_tsub_comm, Eq.symm
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
inst_5 : AddLeftReflectLE α
a b : α
h : b ≤ a
⊢ a + a - (b + b) = a - b + (a - b)

Tactic:
exact (tsub_add_tsub_comm h h).symm

Premises used: tsub_add_tsub_comm, Eq.symm
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddRightReflectLE α
a b c : α
change : (if h : b ≤ a then Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯ else 0) ≤ c ↔ a ≤ c + b
⊢ a - b ≤ c ↔ a ≤ c + b

Tactic:
change dite _ _ _ ≤ c ↔ _

Premises used: dite
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddRightReflectLE α
a b c : α
pos : ∀ (h : b ≤ a), Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯ ≤ c ↔ a ≤ c + b
neg : ∀ (h : ¬b ≤ a), 0 ≤ c ↔ a ≤ c + b
⊢ (if h : b ≤ a then Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯ else 0) ≤ c ↔ a ≤ c + b

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddRightReflectLE α
a b c : α
h : b ≤ a
⊢ a = b + Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯

Tactic:
have := (exists_add_of_le h).choose_spec
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddRightReflectLE α
a b c : α
h : b ≤ a
this : a = b + Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯
⊢ b ≤ b + Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯

Tactic:
rw [this] at h
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddRightReflectLE α
a b c : α
h : b ≤ a
this : a = b + Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯
h₁ : b ≤ b + Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯
⊢ a = b + Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯

Tactic:
rw [this] at h
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddRightReflectLE α
a b c : α
h_1 : b ≤ a
h : b ≤ b + Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯
this : a = b + Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯
rw : Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯ + b ≤ c + b
| a ≤ c + b

Tactic:
rw [this, add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddRightReflectLE α
a b c : α
h_1 : b ≤ a
h : b ≤ b + Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯
this : a = b + Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯
pos : Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯ ≤ c ↔ Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯ + b ≤ c + b
⊢ Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯ ≤ c ↔ a ≤ c + b

Tactic:
conv_rhs => rw [this, add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddRightReflectLE α
a b c : α
h_1 : b ≤ a
h : b ≤ b + Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯
this : a = b + Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯
pos pos₁ : Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯ ≤ c ↔ Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯ ≤ c
⊢ Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯ ≤ c ↔ Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯ + b ≤ c + b

Tactic:
rw [add_le_add_iff_right]

Premises used: add_le_add_iff_right
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddRightReflectLE α
a b c : α
h : ¬b ≤ a
⊢ a < b

Tactic:
rw [not_le] at h

Premises used: not_le
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddRightReflectLE α
a b c : α
h : a < b
neg : 0 ≤ c → a ≤ c + b
neg₁ : a ≤ c + b → 0 ≤ c
⊢ 0 ≤ c ↔ a ≤ c + b

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddRightReflectLE α
a b c : α
h : a < b
h' : 0 ≤ c
⊢ a ≤ c + b

Tactic:
simpa using add_le_add h' h.le

Premises used: add_le_add, LT.lt.le
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddRightReflectLE α
a b c : α
h : a < b
h' : a ≤ c + b
⊢ 0 ≤ c

Tactic:
zero_le

Premises used: zero_le
-- Module: Mathlib.Algebra.Order.Sub.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddRightReflectLE α
a b c : α
h : a < b
h' : a ≤ c + b
⊢ 0 ≤ c

Tactic:
exact zero_le

Premises used: zero_le
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : LE α
inst_1 : Add α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
⊢ a - b ≤ c ↔ a ≤ c + b

Tactic:
OrderedSub.tsub_le_iff_right a b c

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

Tactic:
tsub_le_iff_right.mpr le_rfl

Premises used: Iff.mpr, le_rfl, tsub_le_iff_right
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Add α
inst_2 : Sub α
inst_3 : OrderedSub α
a b : α
⊢ b ≤ b - a + a

Tactic:
tsub_le_iff_right.mp le_rfl

Premises used: le_rfl, tsub_le_iff_right, Iff.mp
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
rw : a ≤ c + b ↔ a ≤ b + c
rw₁ rw₂ : a ≤ b + c ↔ a ≤ b + c
⊢ a - b ≤ c ↔ a ≤ b + c

Tactic:
rw [tsub_le_iff_right, add_comm]

Premises used: tsub_le_iff_right, 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 : α
⊢ a ≤ b + (a - b)

Tactic:
tsub_le_iff_left.mp le_rfl

Premises used: le_rfl, tsub_le_iff_left, Iff.mp
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b : α
⊢ a + b - a ≤ b

Tactic:
tsub_le_iff_left.mpr le_rfl

Premises used: Iff.mpr, le_rfl, tsub_le_iff_left
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b : α
h : a ≤ b
c : α
⊢ a - c ≤ b - c

Tactic:
tsub_le_iff_left.mpr <| h.trans le_add_tsub

Premises used: Iff.mpr, tsub_le_iff_left, 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 : α
rw : a ≤ b + c ↔ a - c ≤ b
rw₁ rw₂ : a ≤ b + c ↔ a ≤ b + c
⊢ a - b ≤ c ↔ a - c ≤ b

Tactic:
rw [tsub_le_iff_left, tsub_le_iff_right]

Premises used: tsub_le_iff_left, tsub_le_iff_right
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b : α
⊢ b - (b - a) ≤ a

Tactic:
tsub_le_iff_right.mpr le_add_tsub

Premises used: Iff.mpr, tsub_le_iff_right, 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 : α
inst_4 : AddLeftMono α
h : a ≤ b
c : α
⊢ a + (c - a) ≤ b + (c - a)

Tactic:
gcongr
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c d : α
inst_4 : AddLeftMono α
hab : a ≤ b
hcd : c ≤ d
⊢ a - d ≤ b - c

Tactic:
(tsub_le_tsub_right hab _).trans <| tsub_le_tsub_left hcd _

Premises used: tsub_le_tsub_left, tsub_le_tsub_right, LE.le.trans
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
c : α
inst_4 : AddLeftMono α
⊢ Antitone (β := α) fun (x : α) ↦ c - x

Tactic:
fun _ _ hxy => tsub_le_tsub rfl.le hxy

Premises used: tsub_le_tsub, Eq.le, Antitone, rfl
-- 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 : AddLeftMono α
grw : a + b ≤ c + (a + (b - c))
grw₁ : a + b ≤ a + (c + (b - c))
grw₂ grw₃ : a + b ≤ a + b
⊢ a + b - c ≤ a + (b - c)

Tactic:
grw [tsub_le_iff_left, add_left_comm, ← le_add_tsub]

Premises used: add_left_comm, tsub_le_iff_left, 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 : α
inst_4 : AddLeftMono α
rw : b + a - c ≤ b + (a - c)
⊢ a + b - c ≤ a - c + b

Tactic:
rw [add_comm, add_comm _ b]

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 c : α
inst_4 : AddLeftMono α
⊢ b + a - c ≤ b + (a - c)

Tactic:
add_tsub_le_assoc

Premises used: add_tsub_le_assoc
-- 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 : AddLeftMono α
⊢ b + a - c ≤ b + (a - c)

Tactic:
exact add_tsub_le_assoc

Premises used: add_tsub_le_assoc
-- 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 : AddLeftMono α
grw : a + b ≤ a + (c + (b - c))
grw₁ grw₂ : a + b ≤ a + b
⊢ a + b ≤ a + c + (b - c)

Tactic:
grw [add_assoc, ← le_add_tsub]

Premises used: add_assoc, 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 : α
inst_4 : AddLeftMono α
rw : b + a ≤ b + c + (a - c)
⊢ a + b ≤ a - c + (b + c)

Tactic:
rw [add_comm a, add_comm (a - c)]

Premises used: HSub.hSub, 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 c : α
inst_4 : AddLeftMono α
⊢ b + a ≤ b + c + (a - c)

Tactic:
add_le_add_add_tsub

Premises used: add_le_add_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 : α
inst_4 : AddLeftMono α
⊢ b + a ≤ b + c + (a - c)

Tactic:
exact add_le_add_add_tsub

Premises used: add_le_add_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 : α
inst_4 : AddLeftMono α
grw : a ≤ c + (a - b + (b - c))
grw₁ : a ≤ c + (a - b) + (b - c)
grw₂ : a ≤ c + (b - c) + (a - b)
grw₃ : a ≤ b + (a - b)
grw₄ grw₅ : a ≤ a
⊢ a - c ≤ a - b + (b - c)

Tactic:
grw [tsub_le_iff_left, ← add_assoc, add_right_comm, ← le_add_tsub, ← le_add_tsub]

Premises used: add_assoc, add_right_comm, tsub_le_iff_left, 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 : α
inst_4 : AddLeftMono α
grw : c - a ≤ c - b + (b - a)
grw₁ : c ≤ a + (c - b + (b - a))
grw₂ : c ≤ c - b + (a + (b - a))
grw₃ : c ≤ c - b + b
grw₄ grw₅ : c ≤ c
⊢ c - a - (c - b) ≤ b - a

Tactic:
grw [tsub_le_iff_left, tsub_le_iff_left, add_left_comm, ← le_add_tsub, ← le_tsub_add]

Premises used: add_left_comm, tsub_le_iff_left, le_tsub_add, le_add_tsub
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
inst_4 : AddLeftMono α
a b c : α
grw grw₁ : a - b + b ≤ a - b + b
⊢ a - b + b ≤ a - b + (c + (b - c))

Tactic:
grw [← le_add_tsub]

Premises used: 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 d : α
inst_4 : AddLeftMono α
rw : a + b - d - c ≤ a - c + (b - d)
⊢ a + b - (c + d) ≤ a - c + (b - d)

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

Premises used: add_assoc, tsub_le_iff_left, 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 c d : α
inst_4 : AddLeftMono α
⊢ a + b - d - c ≤ a - c + (b - d)

Tactic:
(tsub_le_tsub_right add_tsub_le_assoc c).trans ?_

Premises used: add_tsub_le_assoc, tsub_le_tsub_right, LE.le.trans
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c d : α
inst_4 : AddLeftMono α
refine : a + (b - d) - c ≤ a - c + (b - d)
⊢ a + b - d - c ≤ a - c + (b - d)

Tactic:
refine (tsub_le_tsub_right add_tsub_le_assoc c).trans ?_

Premises used: add_tsub_le_assoc, tsub_le_tsub_right, LE.le.trans
-- Module: Mathlib.Algebra.Order.Sub.Defs
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c d : α
inst_4 : AddLeftMono α
rw : b - d + a - c ≤ b - d + (a - c)
⊢ a + (b - d) - c ≤ a - c + (b - d)

Tactic:
rw [add_comm a, add_comm (a - c)]

Premises used: HSub.hSub, 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 c d : α
inst_4 : AddLeftMono α
⊢ b - d + a - c ≤ b - d + (a - c)

Tactic:
add_tsub_le_assoc

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

Tactic:
exact add_tsub_le_assoc

Premises used: add_tsub_le_assoc
-- 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 : AddLeftMono α
grw : a + b ≤ a + c + (b - c)
grw₁ : a + b ≤ a + (c + (b - c))
grw₂ grw₃ : a + b ≤ a + b
⊢ a + b - (a + c) ≤ b - c

Tactic:
grw [tsub_le_iff_left, add_assoc, ← le_add_tsub]

Premises used: add_assoc, tsub_le_iff_left, 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 : α
inst_4 : AddLeftMono α
grw : a + c ≤ b + c + (a - b)
grw₁ : a + c ≤ b + (a - b) + c
grw₂ grw₃ : a + c ≤ a + c
⊢ a + c - (b + c) ≤ a - b

Tactic:
grw [tsub_le_iff_left, add_right_comm, ← le_add_tsub]

Premises used: add_right_comm, tsub_le_iff_left, 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 : α
hb : AddLECancellable b
⊢ a ≤ b + a - b

Tactic:
hb le_add_tsub

Premises used: 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 : α
hb : AddLECancellable b
rw : a ≤ b + a - b
⊢ a ≤ a + b - b

Tactic:
rw [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 : α
hb : AddLECancellable b
⊢ a ≤ b + a - b

Tactic:
hb.le_add_tsub_swap

Premises used: AddLECancellable.le_add_tsub_swap