awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
h : a < b
this : a < b + c
inl : a < b + c → a < b ∨ ∃ d < c, a = b + d
⊢ a < b + c ↔ a < b ∨ ∃ d < c, a = b + d
have inl₁ : (a < b ∨ ∃ d < c, a = b + d) → a < b + c
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
h : a < b
this : a < b + c
inl : a < b + c → a < b ∨ ∃ d < c, a = b + d
inl₁ : (a < b ∨ ∃ d < c, a = b + d) → a < b + c
inl₂ inl₃ : a < b + c → a < b ∨ ∃ d < c, a = b + d
⊢ a < b + c ↔ a < b ∨ ∃ d < c, a = b + d
have inl₄ : a < b + c → ¬a < b → ∃ d < c, a = b + d
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
h : a < b
this : a < b + c
inl : a < b + c → a < b ∨ ∃ d < c, a = b + d
inl₁ : (a < b ∨ ∃ d < c, a = b + d) → a < b + c
inl₂ inl₃ : a < b + c → a < b ∨ ∃ d < c, a = b + d
inl₄ : a < b + c → ¬a < b → ∃ d < c, a = b + d
⊢ a < b + c ↔ a < b ∨ ∃ d < c, a = b + d
have inl₅ : a < b → a < b + c
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
h : a < b
this : a < b + c
inl : a < b + c → a < b ∨ ∃ d < c, a = b + d
inl₁ : (a < b ∨ ∃ d < c, a = b + d) → a < b + c
inl₂ inl₃ : a < b + c → a < b ∨ ∃ d < c, a = b + d
inl₄ : a < b + c → ¬a < b → ∃ d < c, a = b + d
inl₅ : a < b → a < b + c
⊢ a < b + c ↔ a < b ∨ ∃ d < c, a = b + d
have inl₆ : ∀ w < c, a = b + w → a < b + c
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
h : b ≤ a
⊢ a < b + c ↔ a < b ∨ ∃ d < c, a = b + d
have inr : ∀ (a : α) (h : b ≤ b + a), b + a < b + c ↔ b + a < b ∨ ∃ d < c, b + a = b + d
Tactic: obtain ⟨a, rfl⟩ := exists_add_of_le h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
⊢ (∀ a < b + c, P a) ↔ (∀ a < b, P a) ∧ ∀ d < c, P (b + d)
have simp_rw : (∀ (a : α), (a < b ∨ ∃ d < c, a = b + d) → P a) ↔ (∀ a < b, P a) ∧ ∀ d < c, P (b + d)
Tactic: simp_rw [lt_add_iff_lt_left_or_exists_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
⊢ (∃ a < b + c, P a) ↔ (∃ a < b, P a) ∨ ∃ d < c, P (b + d)
have simp_rw : (∃ (a : α), (a < b ∨ ∃ d < c, a = b + d) ∧ P a) ↔ (∃ a < b, P a) ∨ ∃ d < c, P (b + d)
Tactic: simp_rw [lt_add_iff_lt_left_or_exists_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
⊢ a ≤ b + c ↔ a < b ∨ ∃ d ≤ c, a = b + d
have inl : ∀ (h : a < b), a ≤ b + c ↔ a < b ∨ ∃ d ≤ c, a = b + d
Tactic: obtain h | h := lt_or_ge a b
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
inl : ∀ (h : a < b), a ≤ b + c ↔ a < b ∨ ∃ d ≤ c, a = b + d
⊢ a ≤ b + c ↔ a < b ∨ ∃ d ≤ c, a = b + d
have inr : ∀ (h : b ≤ a), a ≤ b + c ↔ a < b ∨ ∃ d ≤ c, a = b + d
Tactic: obtain h | h := lt_or_ge a b
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
h : a < b
⊢ a ≤ b + c ↔ a < b ∨ ∃ d ≤ c, a = b + d
have this : a ≤ b + c
Tactic: have : a ≤ b + c := h.le.trans (le_self_add ..)
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
h : a < b
this : a ≤ b + c
⊢ a ≤ b + c ↔ a < b ∨ ∃ d ≤ c, a = b + d
have inl : a ≤ b + c → a < b ∨ ∃ d ≤ c, a = b + d
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
h : a < b
this : a ≤ b + c
inl : a ≤ b + c → a < b ∨ ∃ d ≤ c, a = b + d
⊢ a ≤ b + c ↔ a < b ∨ ∃ d ≤ c, a = b + d
have inl₁ : (a < b ∨ ∃ d ≤ c, a = b + d) → a ≤ b + c
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
h : a < b
this : a ≤ b + c
inl : a ≤ b + c → a < b ∨ ∃ d ≤ c, a = b + d
inl₁ : (a < b ∨ ∃ d ≤ c, a = b + d) → a ≤ b + c
inl₂ inl₃ : a ≤ b + c → a < b ∨ ∃ d ≤ c, a = b + d
⊢ a ≤ b + c ↔ a < b ∨ ∃ d ≤ c, a = b + d
have inl₄ : a ≤ b + c → ¬a < b → ∃ d ≤ c, a = b + d
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
h : a < b
this : a ≤ b + c
inl : a ≤ b + c → a < b ∨ ∃ d ≤ c, a = b + d
inl₁ : (a < b ∨ ∃ d ≤ c, a = b + d) → a ≤ b + c
inl₂ inl₃ : a ≤ b + c → a < b ∨ ∃ d ≤ c, a = b + d
inl₄ : a ≤ b + c → ¬a < b → ∃ d ≤ c, a = b + d
⊢ a ≤ b + c ↔ a < b ∨ ∃ d ≤ c, a = b + d
have inl₅ : a < b → a ≤ b + c
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
h : a < b
this : a ≤ b + c
inl : a ≤ b + c → a < b ∨ ∃ d ≤ c, a = b + d
inl₁ : (a < b ∨ ∃ d ≤ c, a = b + d) → a ≤ b + c
inl₂ inl₃ : a ≤ b + c → a < b ∨ ∃ d ≤ c, a = b + d
inl₄ : a ≤ b + c → ¬a < b → ∃ d ≤ c, a = b + d
inl₅ : a < b → a ≤ b + c
⊢ a ≤ b + c ↔ a < b ∨ ∃ d ≤ c, a = b + d
have inl₆ : ∀ w ≤ c, a = b + w → a ≤ b + c
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
h : b ≤ a
⊢ a ≤ b + c ↔ a < b ∨ ∃ d ≤ c, a = b + d
have inr : ∀ (a : α) (h : b ≤ b + a), b + a ≤ b + c ↔ b + a < b ∨ ∃ d ≤ c, b + a = b + d
Tactic: obtain ⟨a, rfl⟩ := exists_add_of_le h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
⊢ (∀ a ≤ b + c, P a) ↔ (∀ a < b, P a) ∧ ∀ d ≤ c, P (b + d)
have simp_rw : (∀ (a : α), (a < b ∨ ∃ d ≤ c, a = b + d) → P a) ↔ (∀ a < b, P a) ∧ ∀ d ≤ c, P (b + d)
Tactic: simp_rw [le_add_iff_lt_left_or_exists_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
⊢ (∃ a ≤ b + c, P a) ↔ (∃ a < b, P a) ∨ ∃ d ≤ c, P (b + d)
have simp_rw : (∃ (a : α), (a < b ∨ ∃ d ≤ c, a = b + d) ∧ P a) ↔ (∃ a < b, P a) ∨ ∃ d ≤ c, P (b + d)
Tactic: simp_rw [le_add_iff_lt_left_or_exists_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : AddCommMagma α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
⊢ a < b + c ↔ a < c ∨ ∃ d < b, a = d + c
have rw : (a < c ∨ ∃ d < b, a = c + d) ↔ a < c ∨ ∃ d < b, a = d + c
Tactic: rw [add_comm, lt_add_iff_lt_left_or_exists_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : AddCommMagma α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
⊢ (∀ a < b + c, P a) ↔ (∀ a < c, P a) ∧ ∀ d < b, P (d + c)
have simp_rw : (∀ (a : α), (a < c ∨ ∃ d < b, a = d + c) → P a) ↔ (∀ a < c, P a) ∧ ∀ d < b, P (d + c)
Tactic: simp_rw [lt_add_iff_lt_right_or_exists_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : AddCommMagma α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
⊢ (∃ a < b + c, P a) ↔ (∃ a < c, P a) ∨ ∃ d < b, P (d + c)
have simp_rw : (∃ (a : α), (a < c ∨ ∃ d < b, a = d + c) ∧ P a) ↔ (∃ a < c, P a) ∨ ∃ d < b, P (d + c)
Tactic: simp_rw [lt_add_iff_lt_right_or_exists_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : AddCommMagma α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
⊢ a ≤ b + c ↔ a < c ∨ ∃ d ≤ b, a = d + c
have rw : (a < c ∨ ∃ d ≤ b, a = c + d) ↔ a < c ∨ ∃ d ≤ b, a = d + c
Tactic: rw [add_comm, le_add_iff_lt_left_or_exists_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : AddCommMagma α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
⊢ (∀ a ≤ b + c, P a) ↔ (∀ a < c, P a) ∧ ∀ d ≤ b, P (d + c)
have simp_rw : (∀ (a : α), (a < c ∨ ∃ d ≤ b, a = d + c) → P a) ↔ (∀ a < c, P a) ∧ ∀ d ≤ b, P (d + c)
Tactic: simp_rw [le_add_iff_lt_right_or_exists_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : AddCommMagma α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
⊢ (∃ a ≤ b + c, P a) ↔ (∃ a < c, P a) ∨ ∃ d ≤ b, P (d + c)
have simp_rw : (∃ (a : α), (a < c ∨ ∃ d ≤ b, a = d + c) ∧ P a) ↔ (∃ a < c, P a) ∨ ∃ d ≤ b, P (d + c)
Tactic: simp_rw [le_add_iff_lt_right_or_exists_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Defs (goal)
Goal:
α : Type u
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a b : α
h : a < b
⊢ ∃ (c : α), ∃ (x : 1 < c), a * c = b
have obtain : ∀ (c : α) (hc : b = a * c), ∃ (c : α), ∃ (x : 1 < c), a * c = b
Tactic: obtain ⟨c, hc⟩ := le_iff_exists_mul.1 h.le
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Defs (goal)
Goal:
α : Type u
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a b : α
h : a < b
c : α
hc : b = a * c
⊢ ∃ (c : α), ∃ (x : 1 < c), a * c = b
have refine : c ≠ 1
Tactic: refine ⟨c, one_lt_iff_ne_one.2 ?_, hc.symm⟩
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Defs (goal)
Goal:
α : Type u
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a b : α
inst_3 : MulLeftStrictMono α
⊢ a < b ↔ ∃ (c : α), c > 1 ∧ b = a * c
have rw : (∃ (x : α), b = a * x ∧ a ≠ b) ↔ ∃ (c : α), c > 1 ∧ b = a * c
Tactic: rw [lt_iff_le_and_ne, le_iff_exists_mul, ← exists_and_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Defs (goal)
Goal:
α : Type u
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a b : α
inst_3 : MulLeftStrictMono α
⊢ (∃ (x : α), b = a * x ∧ a ≠ b) ↔ ∃ (c : α), c > 1 ∧ b = a * c
have h : ∀ (a_1 : α), b = a * a_1 ∧ a ≠ b ↔ a_1 > 1 ∧ b = a * a_1
Tactic: apply exists_congr
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Defs (goal)
Goal:
α : Type u
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a b : α
inst_3 : MulLeftStrictMono α
c : α
⊢ b = a * c ∧ a ≠ b ↔ c > 1 ∧ b = a * c
have h : b = a * c → (a ≠ b ↔ 1 < c)
Tactic: rw [and_comm, and_congr_left_iff, gt_iff_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Defs (goal)
Goal:
α : Type u
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a : α
inst_3 : MulLeftStrictMono α
c : α
⊢ a ≠ a * c ↔ 1 < c
have h : a ≠ a * c → 1 < c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Defs (goal)
Goal:
α : Type u
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a : α
inst_3 : MulLeftStrictMono α
c : α
h : a ≠ a * c → 1 < c
⊢ a ≠ a * c ↔ 1 < c
have h₁ : 1 < c → a ≠ a * c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Defs (goal)
Goal:
α : Type u
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a : α
inst_3 : MulLeftStrictMono α
c : α
⊢ a ≠ a * c → 1 < c
have h : a ≠ a * c → c ≠ 1
Tactic: rw [one_lt_iff_ne_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Defs (goal)
Goal:
α : Type u
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a : α
inst_3 : MulLeftStrictMono α
c : α
⊢ a ≠ a * c → c ≠ 1
have h : c = 1 → a = a * c
Tactic: apply mt
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Defs (goal)
Goal:
α : Type u
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a : α
inst_3 : MulLeftStrictMono α
⊢ a = a * 1
have h : a = a
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Defs (goal)
Goal:
α : Type u
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a : α
inst_3 : MulLeftStrictMono α
c : α
⊢ 1 < c → a ≠ a * c
have h : 1 < c → a < a * c
Tactic: rw [← (self_le_mul_right a c).lt_iff_ne]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Defs (goal)
Goal:
α : Type u
inst : Semigroup α
inst_1 : LE α
inst_2 : CanonicallyOrderedMul α
a b c : α
hbc : (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
⊢ (fun (x1 x2 : α) ↦ x1 ≤ x2) ((fun (x1 x2 : α) ↦ x1 * x2) a b) ((fun (x1 x2 : α) ↦ x1 * x2) a c)
have obtain : ∀ (c : α) (hbc : b ≤ b * c),
  LE.le.{u} (α := α) ((fun (x1 x2 : α) ↦ x1 * x2) a b) ((fun (x1 x2 : α) ↦ x1 * x2) a (b * c))
Tactic: obtain ⟨c, hc, rfl⟩ := exists_mul_of_le hbc
Cleared hypotheses: c, hbc
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Defs (goal)
Goal:
α : Type u
inst : Semigroup α
inst_1 : LE α
inst_2 : CanonicallyOrderedMul α
a b c : α
hbc : b ≤ b * c
⊢ LE.le.{u} (α := α) ((fun (x1 x2 : α) ↦ x1 * x2) a b) ((fun (x1 x2 : α) ↦ x1 * x2) a (b * c))
have rw : ∃ (c_1 : α), (fun (x1 x2 : α) ↦ x1 * x2) a (b * c) = (fun (x1 x2 : α) ↦ x1 * x2) a b * c_1
Tactic: rw [le_iff_exists_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Defs (goal)
Goal:
α : Type u
inst : Monoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedMul α
a b c : α
⊢ min a (b * c) = min a (min a b * min a c)
have inl : ∀ (hb : a ≤ b), min a (b * c) = min a (min a b * min a c)
Tactic: rcases le_total a b with hb | hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Defs (goal)
Goal:
α : Type u
inst : Monoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedMul α
a b c : α
inl : ∀ (hb : a ≤ b), min a (b * c) = min a (min a b * min a c)
⊢ min a (b * c) = min a (min a b * min a c)
have inr : ∀ (hb : b ≤ a), min a (b * c) = min a (min a b * min a c)
Tactic: rcases le_total a b with hb | hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Defs (goal)
Goal:
α : Type u
inst : Monoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
⊢ min a (b * c) = min a (min a b * min a c)
have inr : ∀ (hc : a ≤ c), min a (b * c) = min a (min a b * min a c)
Tactic: rcases le_total a c with hc | hc
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Canonical.Defs (goal)
Goal:
α : Type u
inst : Monoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedMul α
a b c : α
hb : b ≤ a
inr : ∀ (hc : a ≤ c), min a (b * c) = min a (min a b * min a c)
⊢ min a (b * c) = min a (min a b * min a c)
have inr₁ : ∀ (hc : c ≤ a), min a (b * c) = min a (min a b * min a c)
Tactic: rcases le_total a c with hc | hc
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Defs (goal)
Goal:
α_1 : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : Preorder α
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a + c ≤ b + c
a b : α
h : a ≤ b
c : α
⊢ c + a ≤ c + b
have rw : a + c ≤ b + c
Tactic: rw [add_comm c, add_comm c]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Defs (goal)
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a * c ≤ b * c
a b : α
h : a ≤ b
c : α
⊢ c * a ≤ c * b
have rw : a * c ≤ b * c
Tactic: rw [mul_comm c, mul_comm c]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Defs (hypothesis)
Goal:
α_1 : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : Preorder α
add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a + c ≤ b + c
add_le_add_right : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
toIsOrderedAddMonoid : IsOrderedAddMonoid α := ⋯
le_of_add_le_add_left : ∀ (a b c : α), a + b ≤ a + c → b ≤ c
a b c : α
h : b + a ≤ c + a
⊢ b ≤ c
have h₁ : a + b ≤ a + c
Tactic: rw [add_comm _ a, add_comm _ a] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Defs (hypothesis)
Goal:
α_1 : Type u_1
α : Type u_2
inst : CommMonoid α
inst_1 : Preorder α
mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), a * c ≤ b * c
mul_le_mul_right : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b
toIsOrderedMonoid : IsOrderedMonoid α := ⋯
le_of_mul_le_mul_left : ∀ (a b c : α), a * b ≤ a * c → b ≤ c
a b c : α
h : b * a ≤ c * a
⊢ b ≤ c
have h₁ : a * b ≤ a * c
Tactic: rw [mul_comm _ a, mul_comm _ a] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a b : α
h : a ≤ b
c : α
⊢ a * c ≤ b * c
have inl : ∀ (h : a ≤ a), a * c ≤ a * c
Tactic: obtain rfl | h := eq_or_lt_of_le h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a b : α
h : a ≤ b
c : α
inl : ∀ (h : a ≤ a), a * c ≤ a * c
⊢ a * c ≤ b * c
have inr : ∀ (h : a < b), a * c ≤ b * c
Tactic: obtain rfl | h := eq_or_lt_of_le h
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Defs (goal)
Goal:
α : Type u_2
inst : CommMonoid α
inst_1 : LinearOrder α
hmul : ∀ (a b c : α), b < c → a * b < a * c
a b c : α
h : a * b ≤ a * c
⊢ b ≤ c
have contrapose! : ∀ (h : c < b), a * c < a * b
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
h : 1 ≤ a * a
⊢ 1 ≤ a
have contrapose! : ∀ (h : a < 1), a * a < 1
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
h : 1 < a * a
⊢ 1 < a
have contrapose! : ∀ (h : a ≤ 1), a * a ≤ 1
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ a * a ≤ 1 ↔ a ≤ 1
have contrapose! : 1 < a * a ↔ 1 < a
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.Defs (goal)
Goal:
α : Type u_1
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
a : α
⊢ a * a < 1 ↔ a < 1
have contrapose! : 1 ≤ a * a ↔ 1 ≤ a
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : ExistsMulOfLE M
a b c : M
⊢ Ico (a * c) (b * c) = map (mulRightEmbedding c) (Ico a b)
have h : ∀ (x : M), x ∈ Ico (a * c) (b * c) ↔ x ∈ map (mulRightEmbedding c) (Ico a b)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : ExistsMulOfLE M
a b c x : M
⊢ x ∈ Ico (a * c) (b * c) ↔ x ∈ map (mulRightEmbedding c) (Ico a b)
have h : a * c ≤ x ∧ x < b * c ↔ ∃ (a_1 : M), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 * c = x
Tactic: simp only [mem_Ico, mem_map, mulRightEmbedding_apply]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : ExistsMulOfLE M
a b c x : M
⊢ a * c ≤ x ∧ x < b * c ↔ ∃ (a_1 : M), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 * c = x
have h : a * c ≤ x ∧ x < b * c → ∃ (a_2 : M), (a ≤ a_2 ∧ a_2 < b) ∧ a_2 * c = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : ExistsMulOfLE M
a b c x : M
h : a * c ≤ x ∧ x < b * c → ∃ (a_2 : M), (a ≤ a_2 ∧ a_2 < b) ∧ a_2 * c = x
⊢ a * c ≤ x ∧ x < b * c ↔ ∃ (a_1 : M), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 * c = x
have h₁ : (∃ (a_1 : M), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 * c = x) → a * c ≤ x ∧ x < b * c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : ExistsMulOfLE M
a b c x : M
h₁ : a * c ≤ x
h₂ : x < b * c
⊢ ∃ (a_1 : M), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 * c = x
have h : ∀ (d : M) (h₁ : a * c ≤ a * c * d) (h₂ : a * c * d < b * c), ∃ (a_1 : M), (a ≤ a_1 ∧ a_1 < b) ∧ a_1 * c = a * c * d
Tactic: obtain ⟨d, rfl⟩ := exists_mul_of_le h₁
Cleared hypotheses: x, h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (goal)
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : ExistsMulOfLE M
a b c d : M
h₁ : a * c ≤ a * c * d
h₂ : a * c * d < b * c
⊢ a * d * c = a * c * d
have simp_rw : a * (d * c) = a * (c * d)
Tactic: simp_rw [mul_assoc, mul_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (hypothesis)
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : ExistsMulOfLE M
a b c : M
⊢ #(Ico (a * c) (b * c)) = #(Ico a b)
have this : Ico (a * c) (b * c) = map (mulRightEmbedding c) (Ico a b)
Tactic: have : (Ico (a * c) (b * c)) = (Ico a b).map (mulRightEmbedding c) := by
    ext x
    simp only [mem_Ico, mem_map, mulRightEmbedding_apply]
    constructor
    · rintro ⟨h₁, h₂⟩
      obtain ⟨d, rfl⟩ := exists_mul_of_le h₁
      exact ⟨a * d, ⟨by simpa using h₁, by simpa [mul_right_comm a c d] using h₂⟩,
        by simp_rw [mul_assoc, mul_comm]⟩
    · aesop
-- Lean 4 proof step from Mathlib.Algebra.Order.Monoid.LocallyFiniteOrder (hypothesis)
Goal:
M : Type u_1
inst : CancelCommMonoid M
inst_1 : LinearOrder M
inst_2 : IsOrderedMonoid M
inst_3 : LocallyFiniteOrder M
inst_4 : ExistsMulOfLE M
a b : M
ha : 1 ≤ a
hb : 1 ≤ b
⊢ #(Ico 1 (a * b)) = #(Ico 1 a) + #(Ico 1 b)
have this : Ico 1 b ∪ Ico (1 * b) (a * b) = Ico 1 (a * b)
Tactic: have : Ico 1 b ∪ Ico (1 * b) (a * b) = Ico 1 (a * b) := by
    simp [Ico_union_Ico, ha, hb, Right.one_le_mul ha hb]