awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
grw : a + (c - a) ≤ c
⊢ a + b ≤ c
have grw₁ : c ≤ c
Tactic: grw [h2, add_tsub_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 : c ≤ b
⊢ a - c ≤ b - c ↔ a ≤ b
have rw : a ≤ b - c + c ↔ a ≤ b
Tactic: rw [tsub_le_iff_right, 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 : c ≤ b
rw : a ≤ b - c + c ↔ a ≤ b
⊢ a - c ≤ b - c ↔ a ≤ b
have rw₁ : a ≤ b ↔ a ≤ b
Tactic: rw [tsub_le_iff_right, 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 : α
h1 : c ≤ a
h2 : c ≤ b
⊢ a - c = b - c ↔ a = b
have simp_rw : a - c ≤ b - c ∧ b - c ≤ a - c ↔ a ≤ b ∧ b ≤ a
Tactic: simp_rw [le_antisymm_iff, tsub_le_tsub_iff_right h1, tsub_le_tsub_iff_right h2]
-- 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 : α
h1 : c ≤ a
h2 : c ≤ b
simp_rw : a - c ≤ b - c ∧ b - c ≤ a - c ↔ a ≤ b ∧ b ≤ a
⊢ a - c = b - c ↔ a = b
have simp_rw₁ : a - c ≤ b - c ∧ b ≤ a ↔ a ≤ b ∧ b ≤ a
Tactic: simp_rw [le_antisymm_iff, tsub_le_tsub_iff_right h1, tsub_le_tsub_iff_right h2]
-- 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 : c ≤ b
h2 : a - c < b - c
⊢ a < b
have refine : a ≠ b
Tactic: refine ((tsub_le_tsub_iff_right h).mp h2.le).lt_of_ne ?_
-- 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 : α
hab : b ≤ a
hcb : c ≤ b
⊢ a - b + (b - c) = a - c
have h : a - b = a - c - (b - c)
Tactic: convert! tsub_add_cancel_of_le (tsub_le_tsub_right hab c) using 2
-- 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 : α
hab : b ≤ a
hcb : c ≤ b
⊢ a - b = a - c - (b - c)
have h : a - b = a - (c + (b - c))
Tactic: rw [tsub_tsub, add_tsub_cancel_of_le hcb]
-- 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 : α
hab : b ≤ a
hcb : c ≤ b
h : a - b = a - (c + (b - c))
⊢ a - b = a - c - (b - c)
have h₁ : a - b = a - b
Tactic: rw [tsub_tsub, add_tsub_cancel_of_le hcb]
-- 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 : c ≤ b
⊢ a - c - (b - c) = a - b
have rw : a - (c + (b - c)) = a - b
Tactic: rw [tsub_tsub, add_tsub_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 : c ≤ b
rw : a - (c + (b - c)) = a - b
⊢ a - c - (b - c) = a - b
have rw₁ : a - b = a - b
Tactic: rw [tsub_tsub, add_tsub_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 : α
hb : AddLECancellable b
h : b ≤ a
⊢ a - b = c ↔ a = c + b
have rw : c = a - b ↔ a = c + b
Tactic: rw [eq_comm, hb.eq_tsub_iff_add_eq_of_le h, eq_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 : α
hb : AddLECancellable b
h : b ≤ a
rw : c = a - b ↔ a = c + b
⊢ a - b = c ↔ a = c + b
have rw₁ : c + b = a ↔ a = c + b
Tactic: rw [eq_comm, hb.eq_tsub_iff_add_eq_of_le h, eq_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 : α
hb : AddLECancellable b
h : b ≤ a
rw : c = a - b ↔ a = c + b
rw₁ : c + b = a ↔ a = c + b
⊢ a - b = c ↔ a = c + b
have rw₂ : a = c + b ↔ a = c + b
Tactic: rw [eq_comm, hb.eq_tsub_iff_add_eq_of_le h, eq_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 α
b c : α
hc : AddLECancellable c
h : c ≤ b
a : α
| a + b - c
have rw : a + (b - c)
Tactic: rw [← add_tsub_cancel_of_le h, add_comm c, ← add_assoc, hc.add_tsub_cancel_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 α
b c : α
hc : AddLECancellable c
h : c ≤ b
a : α
⊢ a + b - c = a + (b - c)
have conv_lhs : 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]
-- 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 α
b c : α
hc : AddLECancellable c
h : c ≤ b
a : α
conv_lhs : a + b - c = a + (b - c)
⊢ a + b - c = a + (b - c)
have conv_lhs₁ : 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]
-- 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 : α
hb : AddLECancellable b
h : b ≤ a
⊢ a - b + c = a + c - b
have rw : a - b + c = c + a - b
Tactic: rw [add_comm a, hb.add_tsub_assoc_of_le h, 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 : α
hb : AddLECancellable b
h : b ≤ a
rw : a - b + c = c + a - b
⊢ a - b + c = a + c - b
have rw₁ : a - b + c = c + (a - b)
Tactic: rw [add_comm a, hb.add_tsub_assoc_of_le h, 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 : α
hb : AddLECancellable b
h : b ≤ a
rw : a - b + c = c + a - b
rw₁ : a - b + c = c + (a - b)
⊢ a - b + c = a + c - b
have rw₂ : c + (a - b) = c + (a - b)
Tactic: rw [add_comm a, hb.add_tsub_assoc_of_le h, 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 : α
hbc : AddLECancellable (b - c)
h₁ : b ≤ a
h₂ : c ≤ b
⊢ a = a - b + c + (b - c)
have rw : a = a - b + (c + (b - c))
Tactic: rw [add_assoc, add_tsub_cancel_of_le h₂, 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 : α
hbc : AddLECancellable (b - c)
h₁ : b ≤ a
h₂ : c ≤ b
rw : a = a - b + (c + (b - c))
⊢ a = a - b + c + (b - c)
have rw₁ : a = a - b + b
Tactic: rw [add_assoc, add_tsub_cancel_of_le h₂, 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 : α
hbc : AddLECancellable (b - c)
h₁ : b ≤ a
h₂ : c ≤ b
rw : a = a - b + (c + (b - c))
rw₁ : a = a - b + b
⊢ a = a - b + c + (b - c)
have rw₂ : a = a
Tactic: rw [add_assoc, add_tsub_cancel_of_le h₂, 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 d : α
hb : AddLECancellable b
hd : AddLECancellable d
hba : b ≤ a
hdc : d ≤ c
⊢ a - b + (c - d) = a + c - (b + d)
have rw : a + (c - d) - b = 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]
-- 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 d : α
hb : AddLECancellable b
hd : AddLECancellable d
hba : b ≤ a
hdc : d ≤ c
rw : a + (c - d) - b = a + c - (b + d)
⊢ a - b + (c - d) = a + c - (b + d)
have rw₁ : a + c - d - b = 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]
-- 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 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)
⊢ a - b + (c - d) = a + c - (b + d)
have rw₂ : a + c - (d + b) = 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]
-- 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 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)
⊢ a - b + (c - d) = a + c - (b + d)
have rw₃ : a + c - (b + 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]
-- 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 : α
ha : AddLECancellable a
h : a ≤ c
⊢ b ≤ c - a ↔ b + a ≤ c
have rw : b ≤ c - a ↔ a + b ≤ c
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 : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a - b < c ↔ a < b + c
have refine : a < b + c → a - b < c
Tactic: refine ⟨hb.lt_add_of_tsub_lt_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 c : α
hb : AddLECancellable b
hba : b ≤ a
h : a < b + c
⊢ a - b < c
have refine : a - b ≠ c
Tactic: refine (tsub_le_iff_left.mpr h.le).lt_of_ne ?_
-- 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 : α
hb : AddLECancellable b
hba : b ≤ a
⊢ a - b < c ↔ a < c + b
have rw : a - b < c ↔ a < b + c
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 : α
hb : AddLECancellable b
hc : AddLECancellable c
h₁ : b ≤ a
h₂ : c ≤ a
⊢ a - b < c ↔ a - c < b
have rw : a < b + c ↔ a - c < b
Tactic: rw [hb.tsub_lt_iff_left h₁, hc.tsub_lt_iff_right 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 : α
hb : AddLECancellable b
hc : AddLECancellable c
h₁ : b ≤ a
h₂ : c ≤ a
rw : a < b + c ↔ a - c < b
⊢ a - b < c ↔ a - c < b
have rw₁ : a < b + c ↔ a < b + c
Tactic: rw [hb.tsub_lt_iff_left h₁, hc.tsub_lt_iff_right 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 : α
ha : AddLECancellable a
hc : AddLECancellable c
h₁ : a ≤ b
h₂ : c ≤ b
⊢ a ≤ b - c ↔ c ≤ b - a
have rw : a ≤ b - c ↔ a + c ≤ b
Tactic: rw [ha.le_tsub_iff_left h₁, hc.le_tsub_iff_right 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 : α
ha : AddLECancellable a
hc : AddLECancellable c
h₁ : a ≤ b
h₂ : c ≤ b
rw : a ≤ b - c ↔ a + c ≤ b
⊢ a ≤ b - c ↔ c ≤ b - a
have rw₁ : a + c ≤ b ↔ a + c ≤ b
Tactic: rw [ha.le_tsub_iff_left h₁, hc.le_tsub_iff_right 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 : α
hc : AddLECancellable c
h : c ≤ b
⊢ a < b - c ↔ a + c < b
have refine : ∀ (h' : 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⟩
-- 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 : α
hc : AddLECancellable c
h : c ≤ b
⊢ a < b - c ↔ c + a < b
have rw : a < b - c ↔ a + c < 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 : α
hab : AddLECancellable (a - b)
h₁ : b ≤ a
h₂ : c ≤ a
h₃ : a - b = a - c
⊢ b = c
have rw : a - b + b = a - b + c
Tactic: rw [← hab.inj]
-- 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 : α
hab : AddLECancellable (a - b)
h₁ : b ≤ a
h₂ : c ≤ a
h₃ : a - b = a - c
⊢ a - b + b = a - b + c
have rw : a = a - b + c
Tactic: rw [tsub_add_cancel_of_le h₁, h₃, 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 : α
hab : AddLECancellable (a - b)
h₁ : b ≤ a
h₂ : c ≤ a
h₃ : a - b = a - c
rw : a = a - b + c
⊢ a - b + b = a - b + c
have rw₁ : a = a - c + c
Tactic: rw [tsub_add_cancel_of_le h₁, h₃, 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 : α
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
⊢ a - b + b = a - b + c
have rw₂ : a = a
Tactic: rw [tsub_add_cancel_of_le h₁, h₃, 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 : α
inst_6 : AddLeftReflectLT α
hb : AddLECancellable b
hca : c ≤ a
h : a - b < a - c
| a - b
have rw : a - c + c - b
Tactic: rw [← tsub_add_cancel_of_le hca]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Unbundled.Basic (hypothesis)
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
⊢ c < b
have h₁ : a - c + c - b < a - c
Tactic: conv_lhs at h => rw [← tsub_add_cancel_of_le hca]
Cleared hypotheses: 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 : α
hc : AddLECancellable c
h : c ≤ a
h2 : a < b
⊢ a - c < b - c
have apply : c + (a - c) < b
Tactic: apply hc.lt_tsub_of_add_lt_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 c : α
hc : AddLECancellable c
hcb : c ≤ b
⊢ a + c + (b - c) = a + b
have rw : a + c + b - c = a + b
Tactic: rw [← hc.add_tsub_assoc_of_le hcb, add_right_comm, hc.add_tsub_cancel_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 c : α
hc : AddLECancellable c
hcb : c ≤ b
rw : a + c + b - c = a + b
⊢ a + c + (b - c) = a + b
have rw₁ : a + b + c - c = a + b
Tactic: rw [← hc.add_tsub_assoc_of_le hcb, add_right_comm, hc.add_tsub_cancel_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 c : α
hc : AddLECancellable c
hcb : c ≤ b
rw : a + c + b - c = a + b
rw₁ : a + b + c - c = a + b
⊢ a + c + (b - c) = a + b
have rw₂ : a + b = a + b
Tactic: rw [← hc.add_tsub_assoc_of_le hcb, add_right_comm, hc.add_tsub_cancel_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 c : α
hac : AddLECancellable (a - c)
h : c ≤ a
⊢ a + b = b + c + (a - c)
have rw : a + b = b + (c + (a - c))
Tactic: rw [add_assoc, add_tsub_cancel_of_le h, 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 : α
hac : AddLECancellable (a - c)
h : c ≤ a
rw : a + b = b + (c + (a - c))
⊢ a + b = b + c + (a - c)
have rw₁ : a + b = b + a
Tactic: rw [add_assoc, add_tsub_cancel_of_le h, 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 : α
hac : AddLECancellable (a - c)
h : c ≤ a
rw : a + b = b + (c + (a - c))
rw₁ : a + b = b + a
⊢ a + b = b + c + (a - c)
have rw₂ : b + a = b + a
Tactic: rw [add_assoc, add_tsub_cancel_of_le h, 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 : α
hab : AddLECancellable (a - b)
h : b ≤ a
⊢ a - c - (a - b) = b - c
have rw : a - (a - b) - c = b - c
Tactic: rw [tsub_right_comm, hab.tsub_tsub_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 : α
hab : AddLECancellable (a - b)
h : b ≤ a
rw : a - (a - b) - c = b - c
⊢ a - c - (a - b) = b - c
have rw₁ : b - c = b - c
Tactic: rw [tsub_right_comm, hab.tsub_tsub_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 : α
inst_6 : AddLeftReflectLE α
h : c ≤ b
⊢ a - (b - c) = a + c - b
have obtain : ∀ (d : α) (h : c ≤ c + d), a - (c + d - c) = a + c - (c + d)
Tactic: obtain ⟨d, 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 : α
inst_6 : AddLeftReflectLE α
d : α
h : c ≤ c + d
⊢ a - (c + d - c) = a + c - (c + d)
have rw : a - d = a + c - (c + d)
Tactic: rw [add_tsub_cancel_left c, add_comm a c, add_tsub_add_eq_tsub_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 c : α
inst_6 : AddLeftReflectLE α
d : α
h : c ≤ c + d
rw : a - d = a + c - (c + d)
⊢ a - (c + d - c) = a + c - (c + d)
have rw₁ : a - d = c + a - (c + d)
Tactic: rw [add_tsub_cancel_left c, add_comm a c, add_tsub_add_eq_tsub_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 c : α
inst_6 : AddLeftReflectLE α
d : α
h : c ≤ c + d
rw : a - d = a + c - (c + d)
rw₁ : a - d = c + a - (c + d)
⊢ a - (c + d - c) = a + c - (c + d)
have rw₂ : a - d = a - d
Tactic: rw [add_tsub_cancel_left c, add_comm a c, add_tsub_add_eq_tsub_left]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Unbundled.Hom (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Add α
inst_2 : Sub α
inst_3 : OrderedSub α
inst_4 : Preorder β
inst_5 : Add β
inst_6 : Sub β
inst_7 : OrderedSub β
f : α →ₙ+ β
hf : Monotone.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)
a b : α
⊢ HSub.hSub (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β) ≤ (f : (a : α) → β) (a - b)
have rw : LE.le.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) (a - b + b) : β)
Tactic: rw [tsub_le_iff_right, ← f.map_add]