awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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))
⊢ a + b - c ≤ a + (b - c)
have grw₁ : a + b ≤ a + (c + (b - c))
Tactic: grw [tsub_le_iff_left, add_left_comm, ← le_add_tsub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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))
⊢ a + b - c ≤ a + (b - c)
have grw₂ : a + b ≤ a + b
Tactic: grw [tsub_le_iff_left, add_left_comm, ← le_add_tsub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
inst_4 : AddLeftMono α
⊢ a + b - c ≤ a - c + b
have rw : b + a - c ≤ b + (a - c)
Tactic: rw [add_comm, add_comm _ b]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
inst_4 : AddLeftMono α
⊢ a + b ≤ a + c + (b - c)
have grw : a + b ≤ a + (c + (b - c))
Tactic: grw [add_assoc, ← le_add_tsub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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))
⊢ a + b ≤ a + c + (b - c)
have grw₁ : a + b ≤ a + b
Tactic: grw [add_assoc, ← le_add_tsub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
inst_4 : AddLeftMono α
⊢ a + b ≤ a - c + (b + c)
have rw : b + a ≤ b + c + (a - c)
Tactic: rw [add_comm a, add_comm (a - c)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
inst_4 : AddLeftMono α
⊢ a - c ≤ a - b + (b - c)
have grw : a ≤ c + (a - b + (b - c))
Tactic: grw [tsub_le_iff_left, ← add_assoc, add_right_comm, ← le_add_tsub, ← le_add_tsub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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))
⊢ a - c ≤ a - b + (b - c)
have grw₁ : a ≤ c + (a - b) + (b - c)
Tactic: grw [tsub_le_iff_left, ← add_assoc, add_right_comm, ← le_add_tsub, ← le_add_tsub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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)
⊢ a - c ≤ a - b + (b - c)
have grw₂ : a ≤ c + (b - c) + (a - b)
Tactic: grw [tsub_le_iff_left, ← add_assoc, add_right_comm, ← le_add_tsub, ← le_add_tsub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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)
⊢ a - c ≤ a - b + (b - c)
have grw₃ : a ≤ b + (a - b)
Tactic: grw [tsub_le_iff_left, ← add_assoc, add_right_comm, ← le_add_tsub, ← le_add_tsub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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)
⊢ a - c ≤ a - b + (b - c)
have grw₄ : a ≤ a
Tactic: grw [tsub_le_iff_left, ← add_assoc, add_right_comm, ← le_add_tsub, ← le_add_tsub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
inst_4 : AddLeftMono α
⊢ c - a - (c - b) ≤ b - a
have grw : 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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)
⊢ c - a - (c - b) ≤ b - a
have grw₁ : 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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))
⊢ c - a - (c - b) ≤ b - a
have grw₂ : c ≤ c - b + (a + (b - a))
Tactic: grw [tsub_le_iff_left, tsub_le_iff_left, add_left_comm, ← le_add_tsub, ← le_tsub_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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))
⊢ c - a - (c - b) ≤ b - a
have grw₃ : c ≤ c - b + b
Tactic: grw [tsub_le_iff_left, tsub_le_iff_left, add_left_comm, ← le_add_tsub, ← le_tsub_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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
⊢ c - a - (c - b) ≤ b - a
have grw₄ : c ≤ c
Tactic: grw [tsub_le_iff_left, tsub_le_iff_left, add_left_comm, ← le_add_tsub, ← le_tsub_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
inst_4 : AddLeftMono α
a b c : α
⊢ a - b + b ≤ a - b + (c + (b - c))
have grw : a - b + b ≤ a - b + b
Tactic: grw [← le_add_tsub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c d : α
inst_4 : AddLeftMono α
⊢ a + b - (c + d) ≤ a - c + (b - d)
have rw : a + b - d - c ≤ a - c + (b - d)
Tactic: rw [add_comm c, tsub_le_iff_left, add_assoc, ← tsub_le_iff_left, ← tsub_le_iff_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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)
have refine : a + (b - d) - c ≤ a - c + (b - d)
Tactic: refine (tsub_le_tsub_right add_tsub_le_assoc c).trans ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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)
have rw : b - d + a - c ≤ b - d + (a - c)
Tactic: rw [add_comm a, add_comm (a - c)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
inst_4 : AddLeftMono α
⊢ a + b - (a + c) ≤ b - c
have grw : a + b ≤ a + c + (b - c)
Tactic: grw [tsub_le_iff_left, add_assoc, ← le_add_tsub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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)
⊢ a + b - (a + c) ≤ b - c
have grw₁ : a + b ≤ a + (c + (b - c))
Tactic: grw [tsub_le_iff_left, add_assoc, ← le_add_tsub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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))
⊢ a + b - (a + c) ≤ b - c
have grw₂ : a + b ≤ a + b
Tactic: grw [tsub_le_iff_left, add_assoc, ← le_add_tsub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
inst_4 : AddLeftMono α
⊢ a + c - (b + c) ≤ a - b
have grw : a + c ≤ b + c + (a - b)
Tactic: grw [tsub_le_iff_left, add_right_comm, ← le_add_tsub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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)
⊢ a + c - (b + c) ≤ a - b
have grw₁ : a + c ≤ b + (a - b) + c
Tactic: grw [tsub_le_iff_left, add_right_comm, ← le_add_tsub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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
⊢ a + c - (b + c) ≤ a - b
have grw₂ : a + c ≤ a + c
Tactic: grw [tsub_le_iff_left, add_right_comm, ← le_add_tsub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b : α
hb : AddLECancellable b
⊢ a ≤ a + b - b
have rw : a ≤ b + a - b
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommMonoid α
inst_2 : Sub α
inst_3 : OrderedSub α
a b : α
⊢ a - b ≤ 0 ↔ a ≤ b
have rw : a ≤ b + 0 ↔ a ≤ b
Tactic: rw [tsub_le_iff_left, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommMonoid α
inst_2 : Sub α
inst_3 : OrderedSub α
a b : α
rw : a ≤ b + 0 ↔ a ≤ b
⊢ a - b ≤ 0 ↔ a ≤ b
have rw₁ : a ≤ b ↔ a ≤ b
Tactic: rw [tsub_le_iff_left, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
b a c : α
⊢ b - a - c = b - (a + c)
have a₁ : b - a - c ≤ b - (a + c)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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)
⊢ b - a - c = b - (a + c)
have a₂ : b - (a + c) ≤ b - a - c
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
b a c : α
⊢ b - a - c ≤ b - (a + c)
have a₁ : b - a ≤ c + (b - (a + c))
Tactic: rw [tsub_le_iff_left, tsub_le_iff_left, ← add_assoc, ← tsub_le_iff_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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))
⊢ b - a - c ≤ b - (a + c)
have a₂ : b ≤ a + (c + (b - (a + c)))
Tactic: rw [tsub_le_iff_left, tsub_le_iff_left, ← add_assoc, ← tsub_le_iff_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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)
have a₃ : b ≤ a + c + (b - (a + c))
Tactic: rw [tsub_le_iff_left, tsub_le_iff_left, ← add_assoc, ← tsub_le_iff_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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))
⊢ b - a - c ≤ b - (a + c)
have a₄ : b - (a + c) ≤ b - (a + c)
Tactic: rw [tsub_le_iff_left, tsub_le_iff_left, ← add_assoc, ← tsub_le_iff_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
b a c : α
⊢ b - (a + c) ≤ b - a - c
have a₁ : b ≤ a + c + (b - a - c)
Tactic: rw [tsub_le_iff_left, add_assoc, ← tsub_le_iff_left, ← tsub_le_iff_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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)
⊢ b - (a + c) ≤ b - a - c
have a₂ : b ≤ a + (c + (b - a - c))
Tactic: rw [tsub_le_iff_left, add_assoc, ← tsub_le_iff_left, ← tsub_le_iff_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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
have a₃ : b - a ≤ c + (b - a - c)
Tactic: rw [tsub_le_iff_left, add_assoc, ← tsub_le_iff_left, ← tsub_le_iff_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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)
⊢ b - (a + c) ≤ b - a - c
have a₄ : b - a - c ≤ b - a - c
Tactic: rw [tsub_le_iff_left, add_assoc, ← tsub_le_iff_left, ← tsub_le_iff_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
⊢ a - (b + c) = a - c - b
have rw : a - (c + b) = a - c - b
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b c : α
⊢ a - b - c = a - c - b
have rw : a - (b + c) = a - c - b
Tactic: rw [← tsub_add_eq_tsub_tsub, tsub_add_eq_tsub_tsub_swap]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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
⊢ a - b - c = a - c - b
have rw₁ : a - c - b = a - c - b
Tactic: rw [← tsub_add_eq_tsub_tsub, tsub_add_eq_tsub_tsub_swap]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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 ≤ a - b
have rw : c ≤ c + b - b
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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
⊢ a = c + b
have rw₁ : b + c = b + c
Tactic: rw [add_comm, h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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
⊢ a = c + b
have rw₁ : b + c = b + c
Tactic: rw [add_comm, h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
a b : α
hb : AddLECancellable b
⊢ a + b = a + b
have rw : b + a = b + a
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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
have rw : a - b ≤ c ∧ a ≠ b + c
Tactic: rw [lt_iff_le_and_ne, ← tsub_le_iff_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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
have refine : a ≠ b + c
Tactic: refine ⟨h.le, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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
have rw : a - c ≤ b ∧ a ≠ b + c
Tactic: rw [lt_iff_le_and_ne, ← tsub_le_iff_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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
have refine : a ≠ b + c
Tactic: refine ⟨h.le, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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
⊢ a - b = a + d - d - b
have rw : a - b = a - b
Tactic: rw [add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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
⊢ a + d - d - b = c + b - b - d
have rw : c + b - d - b = c + b - b - d
Tactic: rw [h, tsub_right_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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
⊢ a + d - d - b = c + b - b - d
have rw₁ : c + b - b - d = c + b - b - d
Tactic: rw [h, tsub_right_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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
⊢ c + b - b - d = c - d
have rw : c - d = c - d
Tactic: rw [add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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
⊢ a - b = c - d
have calc : a - b = a + d - d - b
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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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
⊢ a - b = c - d
have calc₁ : a + d - d - b = c + b - b - 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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
⊢ a - b = c - d
have calc₂ : c + b - b - d = 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]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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
have refine : a ≤ a + c - (b + c) + b
Tactic: refine add_tsub_add_le_tsub_right.antisymm (tsub_le_iff_right.2 <| ?_)
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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 ≤ a + c - (b + c) + b
have bc : a + c ≤ a + c - (b + c) + b + c
Tactic: apply le_of_add_le_add_right
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : Sub α
inst_3 : OrderedSub α
inst_4 : AddLeftMono α
inst_5 : AddLeftReflectLE α
a b c : α
⊢ a + b - (a + c) = b - c
have rw : b + a - (a + c) = b - c
Tactic: rw [add_comm a b, add_comm a c, add_tsub_add_eq_tsub_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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
⊢ a + b - (a + c) = b - c
have rw₁ : b + a - (c + a) = b - c
Tactic: rw [add_comm a b, add_comm a c, add_tsub_add_eq_tsub_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Defs (goal)
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
⊢ a + b - (a + c) = b - c
have rw₂ : b - c = b - c
Tactic: rw [add_comm a b, add_comm a c, add_tsub_add_eq_tsub_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Unbundled.Basic (goal)
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
have refine : a + (b - a) ≤ b
Tactic: refine le_antisymm ?_ le_add_tsub
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Unbundled.Basic (goal)
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
have obtain : ∀ (c : α) (h : a ≤ a + c), a + (a + c - a) ≤ a + c
Tactic: obtain ⟨c, rfl⟩ := exists_add_of_le h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Unbundled.Basic (goal)
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
⊢ a + (a + c - a) ≤ a + c
have grw : a + c ≤ a + c
Tactic: grw [add_tsub_le_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Unbundled.Basic (goal)
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
⊢ b - a + a = b
have rw : a + (b - a) = b
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Unbundled.Basic (goal)
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
⊢ a + b ≤ c
have grw : c - b + b ≤ c
Tactic: grw [h2, tsub_add_cancel_of_le h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Unbundled.Basic (goal)
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
⊢ a + b ≤ c
have grw₁ : c ≤ c
Tactic: grw [h2, tsub_add_cancel_of_le h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Unbundled.Basic (goal)
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
⊢ a + b ≤ c
have grw : a + (c - a) ≤ c
Tactic: grw [h2, add_tsub_cancel_of_le h]