awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Module.Rat
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : DistribMulAction ℚ≥0 α
inst_4 : PosSMulMono ℚ≥0 α
q : ℚ≥0
a : α
ha : a ≤ 0
⊢ |q • a| = q • |a|

Tactic:
simp [*, abs_of_nonneg, abs_of_nonpos, smul_nonneg, smul_nonpos_of_nonneg_of_nonpos]

Premises used: smul_nonneg, abs_of_nonpos, abs_of_nonneg, smul_nonpos_of_nonneg_of_nonpos
-- Module: Mathlib.Algebra.Order.Module.Rat
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : DistribMulAction ℚ≥0 α
inst_4 : PosSMulMono ℚ≥0 α
q : ℚ≥0
a : α
ha : 0 ≤ a
⊢ |q • a| = q • |a|

Tactic:
simp [*, abs_of_nonneg, abs_of_nonpos, smul_nonneg, smul_nonpos_of_nonneg_of_nonpos]

Premises used: smul_nonneg, abs_of_nonpos, abs_of_nonneg, smul_nonpos_of_nonneg_of_nonpos
-- Module: Mathlib.Algebra.Order.Module.Rat
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
q : ℚ≥0
hq : 0 < q
a b : α
hab : a < b
rw : (↑q : α) * a < (↑q : α) * b
⊢ q • a < q • b

Tactic:
rw [NNRat.smul_def, NNRat.smul_def]

Premises used: NNRat.smul_def
-- Module: Mathlib.Algebra.Order.Module.Rat
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
q : ℚ≥0
hq : 0 < q
a b : α
hab : a < b
⊢ (↑q : α) * a < (↑q : α) * b

Tactic:
mul_lt_mul_of_pos_left hab <| NNRat.cast_pos.2 hq

Premises used: Iff.mpr, mul_lt_mul_of_pos_left, NNRat.cast_pos
-- Module: Mathlib.Algebra.Order.Module.Rat
Goal:
α : Type u_1
inst : Semifield α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
q : ℚ≥0
hq : 0 < q
a b : α
hab : a < b
⊢ (↑q : α) * a < (↑q : α) * b

Tactic:
exact mul_lt_mul_of_pos_left hab <| NNRat.cast_pos.2 hq

Premises used: Iff.mpr, mul_lt_mul_of_pos_left, NNRat.cast_pos
-- Module: Mathlib.Algebra.Order.Module.Rat
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
q : ℚ
hq : 0 < q
a b : α
hab : a < b
rw : (↑q : α) * a < (↑q : α) * b
⊢ q • a < q • b

Tactic:
rw [Rat.smul_def, Rat.smul_def]

Premises used: Rat.smul_def
-- Module: Mathlib.Algebra.Order.Module.Rat
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
q : ℚ
hq : 0 < q
a b : α
hab : a < b
⊢ (↑q : α) * a < (↑q : α) * b

Tactic:
mul_lt_mul_of_pos_left hab <| Rat.cast_pos.2 hq

Premises used: Iff.mpr, mul_lt_mul_of_pos_left, Rat.cast_pos
-- Module: Mathlib.Algebra.Order.Module.Rat
Goal:
α : Type u_1
inst : Field α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
q : ℚ
hq : 0 < q
a b : α
hab : a < b
⊢ (↑q : α) * a < (↑q : α) * b

Tactic:
exact mul_lt_mul_of_pos_left hab <| Rat.cast_pos.2 hq

Premises used: Iff.mpr, mul_lt_mul_of_pos_left, Rat.cast_pos
-- Module: Mathlib.Algebra.Order.Monoid.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a : Associates M
d : Associates M
c : Associates M
⊢ a * c ≤ a * d * c

Tactic:
⟨d, mul_right_comm ..⟩

Premises used: mul_right_comm, Exists.intro
-- Module: Mathlib.Algebra.Order.Monoid.Associated
Goal:
M : Type u_1
inst : CommMonoidWithZero M
a : Associates M
d : Associates M
c : Associates M
⊢ a * c ≤ a * d * c

Tactic:
exact ⟨d, mul_right_comm ..⟩
-- Module: Mathlib.Algebra.Order.Monoid.Basic
Goal:
α : Type u
β : Type u_1
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : CommMonoid β
inst_4 : Preorder β
f : β → α
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a b : β
ab : a ≤ b
c : β
rw : f a * f c ≤ f b * f c
⊢ f (a * c) ≤ f (b * c)

Tactic:
rw [mul, mul]
-- Module: Mathlib.Algebra.Order.Monoid.Basic
Goal:
α : Type u
β : Type u_1
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : CommMonoid β
inst_4 : Preorder β
f : β → α
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a b : β
ab : a ≤ b
c : β
grw grw₁ : f b * f c ≤ f b * f c
⊢ f a * f c ≤ f b * f c

Tactic:
grw [le.2 ab]

Premises used: Iff.mpr
-- Module: Mathlib.Algebra.Order.Monoid.Basic
Goal:
α : Type u
β : Type u_1
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedMonoid α
inst_3 : CommMonoid β
inst_4 : LinearOrder β
f : β → α
hf : StrictMono f
mul : ∀ (x y : β), f (x * y) = f x * f y
⊢ IsOrderedMonoid β

Tactic:
Function.Injective.isOrderedMonoid f mul hf.le_iff_le

Premises used: Function.Injective.isOrderedMonoid, StrictMono.le_iff_le
-- Module: Mathlib.Algebra.Order.Monoid.Basic
Goal:
α : Type u
β : Type u_1
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedCancelMonoid α
inst_3 : CommMonoid β
inst_4 : Preorder β
f : β → α
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a b c : β
bc : a * b ≤ a * c
rwa : f (a * b) ≤ f a * f c
rwa₁ : f (a * b) ≤ f (a * c)
rwa₂ rwa₃ rwa₄ rwa₅ : a * b ≤ a * c
⊢ f a * f b ≤ f a * f c

Tactic:
rwa [← mul, ← mul, le]
-- Module: Mathlib.Algebra.Order.Monoid.Basic
Goal:
α : Type u
β : Type u_1
inst : CommMonoid α
inst_1 : Preorder α
inst_2 : IsOrderedCancelMonoid α
inst_3 : CommMonoid β
inst_4 : LinearOrder β
f : β → α
hf : StrictMono f
mul : ∀ (x y : β), f (x * y) = f x * f y
a b c : β
h : a * b ≤ a * c
⊢ b ≤ c

Tactic:
simpa [← hf.le_iff_le, mul] using h

Premises used: StrictMono.le_iff_le
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : OrderBot α
inst_3 : CanonicallyOrderedAdd α
s : Finset ι
f : ι → α
⊢ s.sup f = 0 ↔ ∀ i ∈ s, f i = 0

Tactic:
simp [← bot_eq_zero']

Premises used: bot_eq_zero'
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
ι : Type u_1
α : Type u_2
inst : AddCommMonoid α
inst_1 : LinearOrder α
inst_2 : OrderBot α
inst_3 : CanonicallyOrderedAdd α
s : Finset ι
f : ι → α
hs : s.Nonempty
⊢ s.sup' hs f = 0 ↔ ∀ i ∈ s, f i = 0

Tactic:
simp [sup'_eq_sup]

Premises used: Finset.sup'_eq_sup
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : Sub α
inst_4 : OrderedSub α
β : Type u_2
f : α → β
k : α
x : β
h : x ∈ f '' Ici k
y : α
hy : y ∈ Ici k
hfy : f y = x
⊢ (fun (x : α) ↦ f (x + k)) (y - k) = x

Tactic:
simpa [tsub_add_cancel_of_le hy] using hfy

Premises used: tsub_add_cancel_of_le
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
inl : ∀ (h : a < b), a < b + c ↔ a < b ∨ ∃ d < c, a = b + d
inr : ∀ (h : b ≤ a), a < b + c ↔ a < b ∨ ∃ d < c, a = b + d
⊢ a < b + c ↔ a < b ∨ ∃ d < c, a = b + d

Tactic:
obtain h | h := lt_or_ge a b

Premises used: lt_or_ge
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
h : a < b
⊢ a < b + c

Tactic:
have : a < b + c := h.trans_le (le_self_add ..)
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
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
inl₆ : ∀ w < c, a = b + w → a < b + c
inl₇ : a < b → a < b + c
inl₈ : ∀ w < c, a = b + w → a < b + c
inl₉ : a < b → a < b + c
inl₁₀ : ∀ w < c, a = b + w → a < b + c
inl₁₁ : a < b + c → ¬a < b → ∃ d < c, a = b + d
⊢ a < b + c ↔ a < b ∨ ∃ d < c, a = b + d

Tactic:
tauto
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
h : b ≤ a
inr : ∀ (a : α) (h : b ≤ b + a), b + a < b + c ↔ b + a < b ∨ ∃ d < c, b + a = b + d
⊢ a < b + c ↔ a < b ∨ ∃ d < c, a = b + d

Tactic:
obtain ⟨a, rfl⟩ := exists_add_of_le h

Premises used: ExistsAddOfLE.exists_add_of_le, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
a : α
h : b ≤ b + a
⊢ b + a < b + c ↔ b + a < b ∨ ∃ d < c, b + a = b + d

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
simp_rw : (∀ (a : α), (a < b ∨ ∃ d < c, a = b + d) → P a) ↔ (∀ a < b, P a) ∧ ∀ d < c, P (b + d)
⊢ (∀ a < b + c, P a) ↔ (∀ a < b, P a) ∧ ∀ d < c, P (b + d)

Tactic:
simp_rw [lt_add_iff_lt_left_or_exists_lt]

Premises used: lt_add_iff_lt_left_or_exists_lt
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
⊢ (∀ (a : α), (a < b ∨ ∃ d < c, a = b + d) → P a) ↔ (∀ a < b, P a) ∧ ∀ d < c, P (b + d)

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
simp_rw : (∃ (a : α), (a < b ∨ ∃ d < c, a = b + d) ∧ P a) ↔ (∃ a < b, P a) ∨ ∃ d < c, P (b + d)
⊢ (∃ a < b + c, P a) ↔ (∃ a < b, P a) ∨ ∃ d < c, P (b + d)

Tactic:
simp_rw [lt_add_iff_lt_left_or_exists_lt]

Premises used: lt_add_iff_lt_left_or_exists_lt
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
⊢ (∃ (a : α), (a < b ∨ ∃ d < c, a = b + d) ∧ P a) ↔ (∃ a < b, P a) ∨ ∃ d < c, P (b + d)

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
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
inr : ∀ (h : b ≤ a), a ≤ b + c ↔ a < b ∨ ∃ d ≤ c, a = b + d
⊢ a ≤ b + c ↔ a < b ∨ ∃ d ≤ c, a = b + d

Tactic:
obtain h | h := lt_or_ge a b

Premises used: lt_or_ge
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
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

Tactic:
have : a ≤ b + c := h.le.trans (le_self_add ..)
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
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
inl₆ : ∀ w ≤ c, a = b + w → a ≤ b + c
inl₇ : a < b → a ≤ b + c
inl₈ : ∀ w ≤ c, a = b + w → a ≤ b + c
inl₉ : a < b → a ≤ b + c
inl₁₀ : ∀ w ≤ c, a = b + w → a ≤ b + c
inl₁₁ : a ≤ b + c → ¬a < b → ∃ d ≤ c, a = b + d
⊢ a ≤ b + c ↔ a < b ∨ ∃ d ≤ c, a = b + d

Tactic:
tauto
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
h : b ≤ a
inr : ∀ (a : α) (h : b ≤ b + a), b + a ≤ b + c ↔ b + a < b ∨ ∃ d ≤ c, b + a = b + d
⊢ a ≤ b + c ↔ a < b ∨ ∃ d ≤ c, a = b + d

Tactic:
obtain ⟨a, rfl⟩ := exists_add_of_le h

Premises used: ExistsAddOfLE.exists_add_of_le, rfl
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
a : α
h : b ≤ b + a
⊢ b + a ≤ b + c ↔ b + a < b ∨ ∃ d ≤ c, b + a = b + d

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
simp_rw : (∀ (a : α), (a < b ∨ ∃ d ≤ c, a = b + d) → P a) ↔ (∀ a < b, P a) ∧ ∀ d ≤ c, P (b + d)
⊢ (∀ a ≤ b + c, P a) ↔ (∀ a < b, P a) ∧ ∀ d ≤ c, P (b + d)

Tactic:
simp_rw [le_add_iff_lt_left_or_exists_le]

Premises used: le_add_iff_lt_left_or_exists_le
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
⊢ (∀ (a : α), (a < b ∨ ∃ d ≤ c, a = b + d) → P a) ↔ (∀ a < b, P a) ∧ ∀ d ≤ c, P (b + d)

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
simp_rw : (∃ (a : α), (a < b ∨ ∃ d ≤ c, a = b + d) ∧ P a) ↔ (∃ a < b, P a) ∨ ∃ d ≤ c, P (b + d)
⊢ (∃ a ≤ b + c, P a) ↔ (∃ a < b, P a) ∨ ∃ d ≤ c, P (b + d)

Tactic:
simp_rw [le_add_iff_lt_left_or_exists_le]

Premises used: le_add_iff_lt_left_or_exists_le
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : Add α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
⊢ (∃ (a : α), (a < b ∨ ∃ d ≤ c, a = b + d) ∧ P a) ↔ (∃ a < b, P a) ∨ ∃ d ≤ c, P (b + d)

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : AddCommMagma α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
rw : (a < c ∨ ∃ d < b, a = c + d) ↔ a < c ∨ ∃ d < b, a = d + c
⊢ a < b + c ↔ a < c ∨ ∃ d < b, a = d + c

Tactic:
rw [add_comm, lt_add_iff_lt_left_or_exists_lt]

Premises used: lt_add_iff_lt_left_or_exists_lt, add_comm
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : AddCommMagma α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
⊢ (a < c ∨ ∃ d < b, a = c + d) ↔ a < c ∨ ∃ d < b, a = d + c

Tactic:
simp_rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : AddCommMagma α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
simp_rw : (∀ (a : α), (a < c ∨ ∃ d < b, a = d + c) → P a) ↔ (∀ a < c, P a) ∧ ∀ d < b, P (d + c)
⊢ (∀ a < b + c, P a) ↔ (∀ a < c, P a) ∧ ∀ d < b, P (d + c)

Tactic:
simp_rw [lt_add_iff_lt_right_or_exists_lt]

Premises used: lt_add_iff_lt_right_or_exists_lt
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : AddCommMagma α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
⊢ (∀ (a : α), (a < c ∨ ∃ d < b, a = d + c) → P a) ↔ (∀ a < c, P a) ∧ ∀ d < b, P (d + c)

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : AddCommMagma α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
simp_rw : (∃ (a : α), (a < c ∨ ∃ d < b, a = d + c) ∧ P a) ↔ (∃ a < c, P a) ∨ ∃ d < b, P (d + c)
⊢ (∃ a < b + c, P a) ↔ (∃ a < c, P a) ∨ ∃ d < b, P (d + c)

Tactic:
simp_rw [lt_add_iff_lt_right_or_exists_lt]

Premises used: lt_add_iff_lt_right_or_exists_lt
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : AddCommMagma α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftReflectLT α
inst_4 : IsLeftCancelAdd α
⊢ (∃ (a : α), (a < c ∨ ∃ d < b, a = d + c) ∧ P a) ↔ (∃ a < c, P a) ∨ ∃ d < b, P (d + c)

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : AddCommMagma α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
rw : (a < c ∨ ∃ d ≤ b, a = c + d) ↔ a < c ∨ ∃ d ≤ b, a = d + c
⊢ a ≤ b + c ↔ a < c ∨ ∃ d ≤ b, a = d + c

Tactic:
rw [add_comm, le_add_iff_lt_left_or_exists_le]

Premises used: add_comm, le_add_iff_lt_left_or_exists_le
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
inst_1 : AddCommMagma α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
⊢ (a < c ∨ ∃ d ≤ b, a = c + d) ↔ a < c ∨ ∃ d ≤ b, a = d + c

Tactic:
simp_rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : AddCommMagma α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
simp_rw : (∀ (a : α), (a < c ∨ ∃ d ≤ b, a = d + c) → P a) ↔ (∀ a < c, P a) ∧ ∀ d ≤ b, P (d + c)
⊢ (∀ a ≤ b + c, P a) ↔ (∀ a < c, P a) ∧ ∀ d ≤ b, P (d + c)

Tactic:
simp_rw [le_add_iff_lt_right_or_exists_le]

Premises used: le_add_iff_lt_right_or_exists_le
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : AddCommMagma α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
⊢ (∀ (a : α), (a < c ∨ ∃ d ≤ b, a = d + c) → P a) ↔ (∀ a < c, P a) ∧ ∀ d ≤ b, P (d + c)

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : AddCommMagma α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
simp_rw : (∃ (a : α), (a < c ∨ ∃ d ≤ b, a = d + c) ∧ P a) ↔ (∃ a < c, P a) ∨ ∃ d ≤ b, P (d + c)
⊢ (∃ a ≤ b + c, P a) ↔ (∃ a < c, P a) ∨ ∃ d ≤ b, P (d + c)

Tactic:
simp_rw [le_add_iff_lt_right_or_exists_le]

Premises used: le_add_iff_lt_right_or_exists_le
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Basic
Goal:
α : Type u_1
inst : LinearOrder α
P : α → Prop
b c : α
inst_1 : AddCommMagma α
inst_2 : CanonicallyOrderedAdd α
inst_3 : AddLeftMono α
inst_4 : IsLeftCancelAdd α
⊢ (∃ (a : α), (a < c ∨ ∃ d ≤ b, a = d + c) ∧ P a) ↔ (∃ a < c, P a) ∨ ∃ d ≤ b, P (d + c)

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : Mul α
inst_1 : LE α
inst_2 : CanonicallyOrderedMul α
a b : α
⊢ a ≤ b * a

Tactic:
CanonicallyOrderedMul.le_mul_self _ _

Premises used: CanonicallyOrderedMul.le_mul_self
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : Mul α
inst_1 : LE α
inst_2 : CanonicallyOrderedMul α
a b : α
⊢ a ≤ a * b

Tactic:
CanonicallyOrderedMul.le_self_mul _ _

Premises used: CanonicallyOrderedMul.le_self_mul
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : Mul α
inst_1 : LE α
inst_2 : CanonicallyOrderedMul α
a b : α
⊢ a ≤ b * a

Tactic:
le_mul_self

Premises used: le_mul_self
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : Mul α
inst_1 : LE α
inst_2 : CanonicallyOrderedMul α
a b : α
⊢ a ≤ a * b

Tactic:
le_self_mul

Premises used: le_self_mul
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : Mul α
inst_1 : LE α
inst_2 : CanonicallyOrderedMul α
a c : α
⊢ a ≤ a * c

Tactic:
le_self_mul

Premises used: le_self_mul
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : Mul α
inst_1 : LE α
inst_2 : CanonicallyOrderedMul α
a c : α
⊢ a ≤ a * c

Tactic:
exact le_self_mul

Premises used: le_self_mul
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : Mul α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedMul α
a b c : α
⊢ a * b ≤ c → a ≤ c

Tactic:
le_self_mul.trans

Premises used: le_self_mul, LE.le.trans
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : Mul α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedMul α
a b c : α
⊢ a ≤ b → a ≤ b * c

Tactic:
le_self_mul.trans'

Premises used: le_self_mul, LE.le.trans'
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : Mul α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedMul α
a b c : α
⊢ a * b ≤ c → b ≤ c

Tactic:
le_mul_self.trans

Premises used: le_mul_self, LE.le.trans
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : Mul α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedMul α
a b c : α
⊢ a ≤ c → a ≤ b * c

Tactic:
le_mul_self.trans'

Premises used: le_mul_self, LE.le.trans'
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : CommMagma α
inst_1 : Preorder α
inst_2 : CanonicallyOrderedMul α
a b : α
⊢ a ≤ b ↔ ∃ (c : α), b = c * a

Tactic:
simp only [mul_comm _ a, le_iff_exists_mul]

Premises used: mul_comm, le_iff_exists_mul
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a b : α
h : a < b
obtain : ∀ (c : α) (hc : b = a * c), ∃ (c : α), ∃ (x : 1 < c), a * c = b
⊢ ∃ (c : α), ∃ (x : 1 < c), a * c = b

Tactic:
obtain ⟨c, hc⟩ := le_iff_exists_mul.1 h.le

Premises used: LT.lt.le, Iff.mp, le_iff_exists_mul
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
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

Tactic:
⟨c, one_lt_iff_ne_one.2 ?_, hc.symm⟩

Premises used: Iff.mpr, Exists.intro, Eq.symm, one_lt_iff_ne_one
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a b : α
h : a < b
c : α
hc : b = a * c
refine : c ≠ 1
⊢ ∃ (c : α), ∃ (x : 1 < c), a * c = b

Tactic:
refine ⟨c, one_lt_iff_ne_one.2 ?_, hc.symm⟩
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a b : α
h : a < b
hc : b = a * 1
⊢ False

Tactic:
simp [hc] at h
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a b : α
inst_3 : MulLeftStrictMono α
rw : (∃ (x : α), b = a * x ∧ a ≠ b) ↔ ∃ (c : α), c > 1 ∧ b = a * c
⊢ a < b ↔ ∃ (c : α), c > 1 ∧ b = a * c

Tactic:
rw [lt_iff_le_and_ne, le_iff_exists_mul, ← exists_and_right]

Premises used: lt_iff_le_and_ne, exists_and_right, le_iff_exists_mul
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a b : α
inst_3 : MulLeftStrictMono α
h : ∀ (a_1 : α), b = a * a_1 ∧ a ≠ b ↔ a_1 > 1 ∧ b = a * a_1
⊢ (∃ (x : α), b = a * x ∧ a ≠ b) ↔ ∃ (c : α), c > 1 ∧ b = a * c

Tactic:
apply exists_congr

Premises used: exists_congr
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a b : α
inst_3 : MulLeftStrictMono α
c : α
h : b = a * c → (a ≠ b ↔ 1 < c)
⊢ b = a * c ∧ a ≠ b ↔ c > 1 ∧ b = a * c

Tactic:
rw [and_comm, and_congr_left_iff, gt_iff_lt]

Premises used: and_comm, and_congr_left_iff, gt_iff_lt
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a : α
inst_3 : MulLeftStrictMono α
c : α
h : a ≠ a * c → 1 < c
h₁ : 1 < c → a ≠ a * c
⊢ a ≠ a * c ↔ 1 < c

Tactic:
constructor
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a : α
inst_3 : MulLeftStrictMono α
c : α
h : a ≠ a * c → c ≠ 1
⊢ a ≠ a * c → 1 < c

Tactic:
rw [one_lt_iff_ne_one]

Premises used: one_lt_iff_ne_one
-- Module: Mathlib.Algebra.Order.Monoid.Canonical.Defs
Goal:
α : Type u
inst : MulOneClass α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
a : α
inst_3 : MulLeftStrictMono α
c : α
h : c = 1 → a = a * c
⊢ a ≠ a * c → c ≠ 1

Tactic:
apply mt

Premises used: mt