awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Star.Prod (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : NonUnitalSemiring α
inst_1 : NonUnitalSemiring β
inst_2 : PartialOrder α
inst_3 : PartialOrder β
inst_4 : StarRing α
inst_5 : StarRing β
inst_6 : StarOrderedRing α
inst_7 : StarOrderedRing β
xa : α
xy : β
ya : α
yb : β
⊢ (xa, xy) ≤ (ya, yb) ↔
    ∃ (p : α × β),
      Membership.mem (γ := AddSubmonoid (α × β)) (closure (Set.range fun (s : α × β) ↦ star s * s)) p ∧
        (ya, yb) = (xa, xy) + p
have this : Eq (α := AddSubmonoid (α × β)) (closure (Set.range fun (s : α × β) ↦ star s * s))
  (prod (closure (Set.range fun (s : α) ↦ star s * s)) (closure (Set.range fun (s : β) ↦ star s * s)))
Tactic: have :
        closure (Set.range fun s : α × β ↦ star s * s) =
          (closure <| Set.range fun s : α ↦ star s * s).prod
          (closure <| Set.range fun s : β ↦ star s * s) := by
      rw [← closure_prod (Set.mem_range.2 ⟨0, by simp⟩) (Set.mem_range.2 ⟨0, by simp⟩),
        Set.prod_range_range_eq]
      simp_rw [Prod.mul_def, Prod.star_def]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
⊢ b - a + a = b ↔ a ≤ b
have rw : a + (b - a) = b ↔ a ≤ b
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
⊢ a - b = 0 ↔ a ≤ b
have rw : a - b ≤ 0 ↔ a ≤ b
Tactic: rw [← nonpos_iff_eq_zero, tsub_le_iff_left, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
rw : a - b ≤ 0 ↔ a ≤ b
⊢ a - b = 0 ↔ a ≤ b
have rw₁ : a ≤ b + 0 ↔ a ≤ b
Tactic: rw [← nonpos_iff_eq_zero, tsub_le_iff_left, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
rw : a - b ≤ 0 ↔ a ≤ b
rw₁ : a ≤ b + 0 ↔ a ≤ b
⊢ a - b = 0 ↔ a ≤ b
have rw₂ : a ≤ b ↔ a ≤ b
Tactic: rw [← nonpos_iff_eq_zero, tsub_le_iff_left, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
⊢ 0 < a - b ↔ ¬a ≤ b
have rw : a - b ≠ 0 ↔ ¬a ≤ b
Tactic: rw [pos_iff_ne_zero, Ne, tsub_eq_zero_iff_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
rw : a - b ≠ 0 ↔ ¬a ≤ b
⊢ 0 < a - b ↔ ¬a ≤ b
have rw₁ : ¬a - b = 0 ↔ ¬a ≤ b
Tactic: rw [pos_iff_ne_zero, Ne, tsub_eq_zero_iff_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
rw : a - b ≠ 0 ↔ ¬a ≤ b
rw₁ : ¬a - b = 0 ↔ ¬a ≤ b
⊢ 0 < a - b ↔ ¬a ≤ b
have rw₂ : ¬a ≤ b ↔ ¬a ≤ b
Tactic: rw [pos_iff_ne_zero, Ne, tsub_eq_zero_iff_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b c : α
ha : AddLECancellable a
hc : AddLECancellable c
h : c ≤ a
⊢ a - b ≤ a - c ↔ c ≤ b
have refine : a - b ≤ a - c → c ≤ b
Tactic: refine ⟨?_, fun h => tsub_le_tsub_left h a⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b c : α
ha : AddLECancellable a
hc : AddLECancellable c
h : c ≤ a
⊢ a - b ≤ a - c → c ≤ b
have rw : a + c ≤ a + b → c ≤ b
Tactic: rw [tsub_le_iff_left, ← hc.add_tsub_assoc_of_le h, hc.le_tsub_iff_right (h.trans le_add_self),
    add_comm b]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b c : α
ha : AddLECancellable a
hb : AddLECancellable b
hc : AddLECancellable c
hba : b ≤ a
hca : c ≤ a
⊢ a - b = a - c ↔ b = c
have simp_rw : a - b ≤ a - c ∧ a - c ≤ a - b ↔ b ≤ c ∧ c ≤ b
Tactic: simp_rw [le_antisymm_iff, ha.tsub_le_tsub_iff_left hb hba, ha.tsub_le_tsub_iff_left hc hca,
    and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b c : α
ha : AddLECancellable a
hb : AddLECancellable b
hc : AddLECancellable c
hba : b ≤ a
hca : c ≤ a
simp_rw : a - b ≤ a - c ∧ a - c ≤ a - b ↔ b ≤ c ∧ c ≤ b
⊢ a - b = a - c ↔ b = c
have simp_rw₁ : a - b ≤ a - c ∧ b ≤ c ↔ b ≤ c ∧ c ≤ b
Tactic: simp_rw [le_antisymm_iff, ha.tsub_le_tsub_iff_left hb hba, ha.tsub_le_tsub_iff_left hc hca,
    and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b c : α
ha : AddLECancellable a
hb : AddLECancellable b
hc : AddLECancellable c
hba : b ≤ a
hca : c ≤ a
simp_rw : a - b ≤ a - c ∧ a - c ≤ a - b ↔ b ≤ c ∧ c ≤ b
simp_rw₁ : a - b ≤ a - c ∧ b ≤ c ↔ b ≤ c ∧ c ≤ b
⊢ a - b = a - c ↔ b = c
have simp_rw₂ : c ≤ b ∧ b ≤ c ↔ b ≤ c ∧ c ≤ b
Tactic: simp_rw [le_antisymm_iff, ha.tsub_le_tsub_iff_left hb hba, ha.tsub_le_tsub_iff_left hc hca,
    and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
⊢ 0 < a - b ↔ b < a
have rw : ¬a ≤ b ↔ b < a
Tactic: rw [tsub_pos_iff_not_le, not_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
rw : ¬a ≤ b ↔ b < a
⊢ 0 < a - b ↔ b < a
have rw₁ : b < a ↔ b < a
Tactic: rw [tsub_pos_iff_not_le, not_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
⊢ a - b = a - min a b
have inl : ∀ (h : a ≤ b), a - b = a - min a b
Tactic: rcases le_total a b with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
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 = a - min a b
⊢ a - b = a - min a b
have inr : ∀ (h : b ≤ a), a - b = a - min a b
Tactic: rcases le_total a b with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
h : a ≤ b
⊢ a - b = a - min a b
have inl : a - b = a - a
Tactic: rw [min_eq_left h, tsub_self, tsub_eq_zero_of_le h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
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 = a - a
⊢ a - b = a - min a b
have inl₁ : a - b = 0
Tactic: rw [min_eq_left h, tsub_self, tsub_eq_zero_of_le h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
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 = a - a
inl₁ : a - b = 0
⊢ a - b = a - min a b
have inl₂ : Eq.{u_1 + 1} (α := α) 0 0
Tactic: rw [min_eq_left h, tsub_self, tsub_eq_zero_of_le h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
h : b ≤ a
⊢ a - b = a - min a b
have inr : a - b = a - b
Tactic: rw [min_eq_right h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ a
⊢ a - c < b - c ↔ a < b
have rw : c + (a - c) < b ↔ a < b
Tactic: rw [hc.lt_tsub_iff_left, add_tsub_cancel_of_le h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b c : α
hc : AddLECancellable c
h : c ≤ a
rw : c + (a - c) < b ↔ a < b
⊢ a - c < b - c ↔ a < b
have rw₁ : a < b ↔ a < b
Tactic: rw [hc.lt_tsub_iff_left, add_tsub_cancel_of_le h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
ha : AddLECancellable a
h₁ : 0 < a
h₂ : 0 < b
⊢ a - b < a
have refine : ∀ (h : a - b = a), False
Tactic: refine tsub_le_self.lt_of_ne fun h => ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (hypothesis)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
ha : AddLECancellable a
h₁ : 0 < a
h₂ : 0 < b
h : a - b = a
⊢ False
have h₃ : b < a
Tactic: rw [← h, tsub_pos_iff_lt] at h₁
Cleared hypotheses: h₁, h₂, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
ha : AddLECancellable a
⊢ a - b < a ↔ 0 < a ∧ 0 < b
have refine : ∀ (h : a - b < a), b ≠ 0
Tactic: refine ⟨fun h => ⟨h.pos, pos_of_ne_zero ?_⟩, fun h => ha.tsub_lt_self h.1 h.2⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (hypothesis)
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
⊢ False
have h₁ : a < a
Tactic: rw [tsub_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
inst_5 : AddLeftReflectLE α
a b : α
⊢ a - (a - b) = min a b
have rw : a - (a - min a b) = min a b
Tactic: rw [tsub_eq_tsub_min _ b, tsub_tsub_cancel_of_le (min_le_left a _)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
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
⊢ a - (a - b) = min a b
have rw₁ : min a b = min a b
Tactic: rw [tsub_eq_tsub_min _ b, tsub_tsub_cancel_of_le (min_le_left a _)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
⊢ a - b + b = max a b
have inl : ∀ (h : a ≤ b), a - b + b = max a b
Tactic: rcases le_total a b with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
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
⊢ a - b + b = max a b
have inr : ∀ (h : b ≤ a), a - b + b = max a b
Tactic: rcases le_total a b with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
h : a ≤ b
⊢ a - b + b = max a b
have inl : a - b + b = b
Tactic: rw [max_eq_right h, tsub_eq_zero_of_le h, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
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
⊢ a - b + b = max a b
have inl₁ : 0 + b = b
Tactic: rw [max_eq_right h, tsub_eq_zero_of_le h, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
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
⊢ a - b + b = max a b
have inl₂ : b = b
Tactic: rw [max_eq_right h, tsub_eq_zero_of_le h, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
h : b ≤ a
⊢ a - b + b = max a b
have inr : a - b + b = a
Tactic: rw [max_eq_left h, tsub_add_cancel_of_le h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
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
⊢ a - b + b = max a b
have inr₁ : a = a
Tactic: rw [max_eq_left h, tsub_add_cancel_of_le h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
⊢ a + (b - a) = max a b
have rw : b - a + a = max a b
Tactic: rw [add_comm, max_comm, tsub_add_eq_max]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
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
⊢ a + (b - a) = max a b
have rw₁ : b - a + a = max b a
Tactic: rw [add_comm, max_comm, tsub_add_eq_max]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
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
⊢ a + (b - a) = max a b
have rw₂ : max b a = max b a
Tactic: rw [add_comm, max_comm, tsub_add_eq_max]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
a b : α
⊢ a - b + min a b = a
have h : min a b ≤ a
Tactic: rw [← tsub_min, @tsub_add_cancel_of_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
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
⊢ Even (m - n)
have obtain : ∀ (a : α), Even (a + a - n)
Tactic: obtain ⟨a, rfl⟩ := hm
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
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 : α
⊢ Even (a + a - n)
have obtain : ∀ (b : α), Even (a + a - (b + b))
Tactic: obtain ⟨b, rfl⟩ := hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
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))
have refine : a + a - (b + b) = a - b + (a - b)
Tactic: refine ⟨a - b, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
inst_5 : AddLeftReflectLE α
a b : α
⊢ a + a - (b + b) = a - b + (a - b)
have inl : ∀ (h : a ≤ b), a + a - (b + b) = a - b + (a - b)
Tactic: obtain h | h := le_total a b
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
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)
⊢ a + a - (b + b) = a - b + (a - b)
have inr : ∀ (h : b ≤ a), a + a - (b + b) = a - b + (a - b)
Tactic: obtain h | h := le_total a b
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
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
⊢ a + a - (b + b) = a - b + (a - b)
have inl : a + a - (b + b) = HAdd.hAdd (α := α) 0 0
Tactic: rw [tsub_eq_zero_of_le h, tsub_eq_zero_of_le (add_le_add h h), add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
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
⊢ a + a - (b + b) = a - b + (a - b)
have inl₁ : 0 = HAdd.hAdd (α := α) 0 0
Tactic: rw [tsub_eq_zero_of_le h, tsub_eq_zero_of_le (add_le_add h h), add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
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
⊢ a + a - (b + b) = a - b + (a - b)
have inl₂ : Eq.{u_1 + 1} (α := α) 0 0
Tactic: rw [tsub_eq_zero_of_le h, tsub_eq_zero_of_le (add_le_add h h), add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddRightReflectLE α
a b c : α
⊢ a - b ≤ c ↔ a ≤ c + b
have change : (if h : b ≤ a then Exists.choose (p := fun (c : α) ↦ a = b + c) sorry else 0) ≤ c ↔ a ≤ c + b
Tactic: change dite _ _ _ ≤ c ↔ _
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddRightReflectLE α
a b c : α
⊢ (if h : b ≤ a then Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯ else 0) ≤ c ↔ a ≤ c + b
have pos : ∀ (h : b ≤ a), Exists.choose (p := fun (c : α) ↦ a = b + c) sorry ≤ c ↔ a ≤ c + b
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
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
⊢ (if h : b ≤ a then Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯ else 0) ≤ c ↔ a ≤ c + b
have neg : ∀ (h : ¬b ≤ a), 0 ≤ c ↔ a ≤ c + b
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (hypothesis)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddRightReflectLE α
a b c : α
h : b ≤ a
⊢ Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯ ≤ c ↔ a ≤ c + b
have this : a = b + Exists.choose (p := fun (c : α) ↦ a = b + c) sorry
Tactic: have := (exists_add_of_le h).choose_spec
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (hypothesis)
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) ⋯
⊢ Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯ ≤ c ↔ a ≤ c + b
have h₁ : b ≤ b + Exists.choose (p := fun (c : α) ↦ a = b + c) sorry
Tactic: rw [this] at h
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
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) ⋯
| a ≤ c + b
have rw : Exists.choose (p := fun (c : α) ↦ a = b + c) sorry + b ≤ c + b
Tactic: rw [this, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
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) ⋯
⊢ Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯ ≤ c ↔ a ≤ c + b
have pos : Exists.choose (p := fun (c : α) ↦ a = b + c) sorry ≤ c ↔ Exists.choose (p := fun (c : α) ↦ a = b + c) sorry + b ≤ c + b
Tactic: conv_rhs => rw [this, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
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) ⋯
⊢ Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯ ≤ c ↔ Exists.choose (p := fun (c : α) ↦ a = b + c) ⋯ + b ≤ c + b
have pos : Exists.choose (p := fun (c : α) ↦ a = b + c) sorry ≤ c ↔ Exists.choose (p := fun (c : α) ↦ a = b + c) sorry ≤ c
Tactic: rw [add_le_add_iff_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (hypothesis)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddRightReflectLE α
a b c : α
h : ¬b ≤ a
⊢ 0 ≤ c ↔ a ≤ c + b
have h₁ : a < b
Tactic: rw [not_le] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddRightReflectLE α
a b c : α
h : a < b
⊢ 0 ≤ c ↔ a ≤ c + b
have neg : 0 ≤ c → a ≤ c + b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Basic (goal)
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
⊢ 0 ≤ c ↔ a ≤ c + b
have neg₁ : a ≤ c + b → 0 ≤ c
Tactic: constructor
-- 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 : α
⊢ a - b ≤ c ↔ a ≤ b + c
have rw : a ≤ c + b ↔ a ≤ b + c
Tactic: rw [tsub_le_iff_right, add_comm]
-- 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 : α
rw : a ≤ c + b ↔ a ≤ b + c
⊢ a - b ≤ c ↔ a ≤ b + c
have rw₁ : a ≤ b + c ↔ a ≤ b + c
Tactic: rw [tsub_le_iff_right, add_comm]
-- 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 : α
⊢ a - b ≤ c ↔ a - c ≤ b
have rw : a ≤ b + c ↔ a - c ≤ b
Tactic: rw [tsub_le_iff_left, tsub_le_iff_right]
-- 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 : α
rw : a ≤ b + c ↔ a - c ≤ b
⊢ a - b ≤ c ↔ a - c ≤ b
have rw₁ : a ≤ b + c ↔ a ≤ b + c
Tactic: rw [tsub_le_iff_left, tsub_le_iff_right]
-- 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 + (b - c)
have grw : a + b ≤ c + (a + (b - c))
Tactic: grw [tsub_le_iff_left, add_left_comm, ← le_add_tsub]