awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulRightMono α
a b : α
rw : 1 * b ≤ a / b * b ↔ b ≤ a
rw₁ : b ≤ a / b * b ↔ b ≤ a
rw₂ : b ≤ a * b⁻¹ * b ↔ b ≤ a
rw₃ rw₄ : b ≤ a ↔ b ≤ a
⊢ 1 ≤ a / b ↔ b ≤ a

Tactic:
rw [← mul_le_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]

Premises used: mul_le_mul_iff_right, div_eq_mul_inv, inv_mul_cancel_right, one_mul
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulRightMono α
a b : α
rw : a / b * b ≤ 1 * b ↔ a ≤ b
rw₁ : a / b * b ≤ b ↔ a ≤ b
rw₂ : a * b⁻¹ * b ≤ b ↔ a ≤ b
rw₃ rw₄ : a ≤ b ↔ a ≤ b
⊢ a / b ≤ 1 ↔ a ≤ b

Tactic:
rw [← mul_le_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]

Premises used: mul_le_mul_iff_right, div_eq_mul_inv, inv_mul_cancel_right, one_mul
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulRightMono α
a b c : α
rw : a * b ≤ c / b * b ↔ a * b ≤ c
rw₁ : a * b ≤ c * b⁻¹ * b ↔ a * b ≤ c
rw₂ rw₃ : a * b ≤ c ↔ a * b ≤ c
⊢ a ≤ c / b ↔ a * b ≤ c

Tactic:
rw [← mul_le_mul_iff_right b, div_eq_mul_inv, inv_mul_cancel_right]

Premises used: mul_le_mul_iff_right, div_eq_mul_inv, inv_mul_cancel_right
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulRightMono α
a b c : α
rw : a / c * c ≤ b * c ↔ a ≤ b * c
rw₁ : a * c⁻¹ * c ≤ b * c ↔ a ≤ b * c
rw₂ rw₃ : a ≤ b * c ↔ a ≤ b * c
⊢ a / c ≤ b ↔ a ≤ b * c

Tactic:
rw [← mul_le_mul_iff_right c, div_eq_mul_inv, inv_mul_cancel_right]

Premises used: mul_le_mul_iff_right, div_eq_mul_inv, inv_mul_cancel_right
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α_1 : Type u
inst : Group α_1
inst_1 : LE α_1
inst_2 : MulRightMono α_1
a b c : α_1
α : Type u_1
inst_3 : AddGroup α
inst_4 : LE α
inst_5 : AddRightMono α
⊢ OrderedSub α

Tactic:
⟨fun _ _ _ => sub_le_iff_le_add⟩

Premises used: sub_le_iff_le_add, OrderedSub.mk
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
b c a : α
rw : a * b⁻¹ ≤ a / c ↔ c ≤ b
rw₁ : a * b⁻¹ ≤ a * c⁻¹ ↔ c ≤ b
rw₂ : a⁻¹ * (a * b⁻¹) ≤ a⁻¹ * (a * c⁻¹) ↔ c ≤ b
rw₃ : b⁻¹ ≤ a⁻¹ * (a * c⁻¹) ↔ c ≤ b
rw₄ : b⁻¹ ≤ c⁻¹ ↔ c ≤ b
rw₅ rw₆ : c ≤ b ↔ c ≤ b
⊢ a / b ≤ a / c ↔ c ≤ b

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_le_mul_iff_left a⁻¹, inv_mul_cancel_left,
    inv_mul_cancel_left, inv_le_inv_iff]

Premises used: inv_mul_cancel_left, mul_le_mul_iff_left, div_eq_mul_inv, inv_le_inv_iff, Inv.inv
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b : α
h : a ≤ b
c : α
⊢ c / b ≤ c / a

Tactic:
(div_le_div_iff_left c).2 h

Premises used: Iff.mpr, div_le_div_iff_left
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : CommGroup α
inst_1 : LE α
inst_2 : MulLeftMono α
a b c d : α
⊢ a / b ≤ c / d ↔ a * d ≤ c * b

Tactic:
simpa only [div_eq_mul_inv] using mul_inv_le_mul_inv_iff'

Premises used: mul_inv_le_mul_inv_iff', div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : CommGroup α
inst_1 : LE α
inst_2 : MulLeftMono α
a b c : α
rw : b * a ≤ c ↔ a * b ≤ c
rw₁ rw₂ : a * b ≤ c ↔ a * b ≤ c
⊢ b ≤ c / a ↔ a * b ≤ c

Tactic:
rw [le_div_iff_mul_le, mul_comm]

Premises used: mul_comm, le_div_iff_mul_le
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : CommGroup α
inst_1 : LE α
inst_2 : MulLeftMono α
a b c : α
rw : a ≤ c * b ↔ a ≤ b * c
rw₁ rw₂ : a ≤ b * c ↔ a ≤ b * c
⊢ a / b ≤ c ↔ a ≤ b * c

Tactic:
rw [div_le_iff_le_mul, mul_comm]

Premises used: mul_comm, div_le_iff_le_mul
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : CommGroup α
inst_1 : LE α
inst_2 : MulLeftMono α
a b c : α
⊢ b⁻¹ ≤ a / c ↔ c ≤ a * b

Tactic:
le_div_iff_mul_le.trans inv_mul_le_iff_le_mul'

Premises used: inv_mul_le_iff_le_mul', Iff.trans, le_div_iff_mul_le
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : CommGroup α
inst_1 : LE α
inst_2 : MulLeftMono α
a b c : α
rw : c ≤ b * a ↔ c ≤ a * b
rw₁ rw₂ : c ≤ a * b ↔ c ≤ a * b
⊢ a⁻¹ ≤ b / c ↔ c ≤ a * b

Tactic:
rw [inv_le_div_iff_le_mul, mul_comm]

Premises used: mul_comm, inv_le_div_iff_le_mul
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : CommGroup α
inst_1 : LE α
inst_2 : MulLeftMono α
a b c : α
⊢ a / b ≤ c ↔ a / c ≤ b

Tactic:
div_le_iff_le_mul'.trans div_le_iff_le_mul.symm

Premises used: div_le_iff_le_mul', Iff.trans, div_le_iff_le_mul, Iff.symm
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : CommGroup α
inst_1 : LE α
inst_2 : MulLeftMono α
a b c : α
⊢ a ≤ b / c ↔ c ≤ b / a

Tactic:
le_div_iff_mul_le'.trans le_div_iff_mul_le.symm

Premises used: le_div_iff_mul_le', Iff.trans, Iff.symm, le_div_iff_mul_le
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : CommGroup α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
rw : a * c ≤ b * d
⊢ a / d ≤ b / c

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, mul_comm b, mul_inv_le_inv_mul_iff, mul_comm]

Premises used: div_eq_mul_inv, mul_comm, mul_inv_le_inv_mul_iff
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : CommGroup α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ a * c ≤ b * d

Tactic:
mul_le_mul' hab hcd

Premises used: mul_le_mul'
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : CommGroup α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ a * c ≤ b * d

Tactic:
exact mul_le_mul' hab hcd

Premises used: mul_le_mul'
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulRightStrictMono α
a b c : α
⊢ a / c < b / c ↔ a < b

Tactic:
simpa only [div_eq_mul_inv] using mul_lt_mul_iff_right _

Premises used: div_eq_mul_inv, mul_lt_mul_iff_right
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulRightStrictMono α
a b : α
h : a < b
c : α
⊢ a / c < b / c

Tactic:
(div_lt_div_iff_right c).2 h

Premises used: Iff.mpr, div_lt_div_iff_right
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulRightStrictMono α
a b : α
rw : 1 * b < a / b * b ↔ b < a
rw₁ : b < a / b * b ↔ b < a
rw₂ : b < a * b⁻¹ * b ↔ b < a
rw₃ rw₄ : b < a ↔ b < a
⊢ 1 < a / b ↔ b < a

Tactic:
rw [← mul_lt_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]

Premises used: div_eq_mul_inv, mul_lt_mul_iff_right, inv_mul_cancel_right, one_mul
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulRightStrictMono α
a b : α
rw : a / b * b < 1 * b ↔ a < b
rw₁ : a / b * b < b ↔ a < b
rw₂ : a * b⁻¹ * b < b ↔ a < b
rw₃ rw₄ : a < b ↔ a < b
⊢ a / b < 1 ↔ a < b

Tactic:
rw [← mul_lt_mul_iff_right b, one_mul, div_eq_mul_inv, inv_mul_cancel_right]

Premises used: div_eq_mul_inv, mul_lt_mul_iff_right, inv_mul_cancel_right, one_mul
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulRightStrictMono α
a b c : α
rw : a * b < c / b * b ↔ a * b < c
rw₁ : a * b < c * b⁻¹ * b ↔ a * b < c
rw₂ rw₃ : a * b < c ↔ a * b < c
⊢ a < c / b ↔ a * b < c

Tactic:
rw [← mul_lt_mul_iff_right b, div_eq_mul_inv, inv_mul_cancel_right]

Premises used: div_eq_mul_inv, mul_lt_mul_iff_right, inv_mul_cancel_right
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulRightStrictMono α
a b c : α
rw : a / c * c < b * c ↔ a < b * c
rw₁ : a * c⁻¹ * c < b * c ↔ a < b * c
rw₂ rw₃ : a < b * c ↔ a < b * c
⊢ a / c < b ↔ a < b * c

Tactic:
rw [← mul_lt_mul_iff_right c, div_eq_mul_inv, inv_mul_cancel_right]

Premises used: div_eq_mul_inv, mul_lt_mul_iff_right, inv_mul_cancel_right
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
b c a : α
rw : a * b⁻¹ < a / c ↔ c < b
rw₁ : a * b⁻¹ < a * c⁻¹ ↔ c < b
rw₂ : a⁻¹ * (a * b⁻¹) < a⁻¹ * (a * c⁻¹) ↔ c < b
rw₃ : b⁻¹ < a⁻¹ * (a * c⁻¹) ↔ c < b
rw₄ : b⁻¹ < c⁻¹ ↔ c < b
rw₅ rw₆ : c < b ↔ c < b
⊢ a / b < a / c ↔ c < b

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_lt_mul_iff_left a⁻¹, inv_mul_cancel_left,
    inv_mul_cancel_left, inv_lt_inv_iff]

Premises used: inv_mul_cancel_left, mul_lt_mul_iff_left, div_eq_mul_inv, Inv.inv, inv_lt_inv_iff
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b c : α
rw : a⁻¹ < b * c⁻¹ ↔ c < a * b
rw₁ : a⁻¹ * c < b ↔ c < a * b
rw₂ rw₃ : c < a * b ↔ c < a * b
⊢ a⁻¹ < b / c ↔ c < a * b

Tactic:
rw [div_eq_mul_inv, lt_mul_inv_iff_mul_lt, inv_mul_lt_iff_lt_mul]

Premises used: lt_mul_inv_iff_mul_lt, div_eq_mul_inv, inv_mul_lt_iff_lt_mul
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
a b : α
h : a < b
c : α
⊢ c / b < c / a

Tactic:
(div_lt_div_iff_left c).2 h

Premises used: Iff.mpr, div_lt_div_iff_left
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : CommGroup α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b c d : α
⊢ a / b < c / d ↔ a * d < c * b

Tactic:
simpa only [div_eq_mul_inv] using mul_inv_lt_mul_inv_iff'

Premises used: div_eq_mul_inv, mul_inv_lt_mul_inv_iff'
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : CommGroup α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b c : α
rw : b * a < c ↔ a * b < c
rw₁ rw₂ : a * b < c ↔ a * b < c
⊢ b < c / a ↔ a * b < c

Tactic:
rw [lt_div_iff_mul_lt, mul_comm]

Premises used: lt_div_iff_mul_lt, mul_comm
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : CommGroup α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b c : α
rw : a < c * b ↔ a < b * c
rw₁ rw₂ : a < b * c ↔ a < b * c
⊢ a / b < c ↔ a < b * c

Tactic:
rw [div_lt_iff_lt_mul, mul_comm]

Premises used: mul_comm, div_lt_iff_lt_mul
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : CommGroup α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b c : α
⊢ b⁻¹ < a / c ↔ c < a * b

Tactic:
lt_div_iff_mul_lt.trans inv_mul_lt_iff_lt_mul'

Premises used: lt_div_iff_mul_lt, inv_mul_lt_iff_lt_mul', Iff.trans
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : CommGroup α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b c : α
⊢ a / b < c ↔ a / c < b

Tactic:
div_lt_iff_lt_mul'.trans div_lt_iff_lt_mul.symm

Premises used: div_lt_iff_lt_mul', Iff.trans, Iff.symm, div_lt_iff_lt_mul
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : CommGroup α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b c : α
⊢ a < b / c ↔ c < b / a

Tactic:
lt_div_iff_mul_lt'.trans lt_div_iff_mul_lt.symm

Premises used: lt_div_iff_mul_lt', lt_div_iff_mul_lt, Iff.trans, Iff.symm
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : CommGroup α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
a b c d : α
hab : a < b
hcd : c < d
rw : a * c < b * d
⊢ a / d < b / c

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, mul_comm b, mul_inv_lt_inv_mul_iff, mul_comm]

Premises used: div_eq_mul_inv, mul_comm, mul_inv_lt_inv_mul_iff
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : CommGroup α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
a b c d : α
hab : a < b
hcd : c < d
⊢ a * c < b * d

Tactic:
mul_lt_mul_of_lt_of_lt hab hcd

Premises used: mul_lt_mul_of_lt_of_lt
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : CommGroup α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
a b c d : α
hab : a < b
hcd : c < d
⊢ a * c < b * d

Tactic:
exact mul_lt_mul_of_lt_of_lt hab hcd

Premises used: mul_lt_mul_of_lt_of_lt
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a b c d : α
contrapose! : b ≤ a ∧ d ≤ c → b / c ≤ a / d
⊢ a / d < b / c → a < b ∨ c < d

Tactic:
contrapose!
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a b c d : α
⊢ b ≤ a ∧ d ≤ c → b / c ≤ a / d

Tactic:
fun h ↦ div_le_div'' h.1 h.2

Premises used: div_le_div'', And.right, And.left
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a b c d : α
⊢ b ≤ a ∧ d ≤ c → b / c ≤ a / d

Tactic:
exact fun h ↦ div_le_div'' h.1 h.2

Premises used: div_le_div''
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulRightMono α
a b : α
rw : cmp (a / b * b) (1 * b) = cmp a b
rw₁ : cmp (a / b * b) b = cmp a b
rw₂ rw₃ : cmp a b = cmp a b
⊢ cmp (a / b) 1 = cmp a b

Tactic:
rw [← cmp_mul_right' _ _ b, one_mul, div_mul_cancel]

Premises used: cmp_mul_right', div_mul_cancel, one_mul
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a b : α
h : ∀ (ε : α), 1 < ε → a < b * ε
h₁ : b < a
⊢ a < a

Tactic:
simpa using h _ (lt_inv_mul_iff_lt.mpr h₁)

Premises used: Iff.mpr, lt_inv_mul_iff_lt
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a b : α
⊢ a ≤ b ↔ ∀ (ε : α), 1 < ε → a < b * ε

Tactic:
⟨fun h _ => lt_mul_of_le_of_one_lt h, le_of_forall_one_lt_lt_mul⟩

Premises used: Iff.intro, lt_mul_of_le_of_one_lt, le_of_forall_one_lt_lt_mul
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a b : α
inst_3 : MulRightMono α
rw : a * a ≤ b * b ↔ a ≤ b
⊢ a / b ≤ a⁻¹ * b ↔ a ≤ b

Tactic:
rw [div_eq_mul_inv, mul_inv_le_inv_mul_iff]

Premises used: div_eq_mul_inv, mul_inv_le_inv_mul_iff
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a b : α
inst_3 : MulRightMono α
⊢ a * a ≤ b * b ↔ a ≤ b

Tactic:
⟨fun h => not_lt.mp fun k => not_lt.mpr h (mul_lt_mul_of_lt_of_lt k k), fun h =>
      mul_le_mul' h h⟩

Premises used: Iff.mpr, not_lt, mul_lt_mul_of_lt_of_lt, Iff.intro, Iff.mp, mul_le_mul'
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a b : α
inst_3 : MulRightMono α
⊢ a * a ≤ b * b ↔ a ≤ b

Tactic:
exact
    ⟨fun h => not_lt.mp fun k => not_lt.mpr h (mul_lt_mul_of_lt_of_lt k k), fun h =>
      mul_le_mul' h h⟩
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a b : α
rw : a / b ≤ a⁻¹ * b ↔ a ≤ b
⊢ a / b ≤ b / a ↔ a ≤ b

Tactic:
rw [div_eq_mul_inv b, mul_comm]

Premises used: div_eq_mul_inv, mul_comm
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a b : α
⊢ a / b ≤ a⁻¹ * b ↔ a ≤ b

Tactic:
div_le_inv_mul_iff

Premises used: div_le_inv_mul_iff
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u_1
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a b : α
⊢ a / b ≤ a⁻¹ * b ↔ a ≤ b

Tactic:
exact div_le_inv_mul_iff

Premises used: div_le_inv_mul_iff
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
β : Type u_1
inst : Group α
inst_1 : Preorder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
inst_4 : Preorder β
f : β → α
hf : Monotone f
⊢ Antitone.{u_1, u} (β := α) fun (x : β) ↦ (f x)⁻¹

Tactic:
fun _ _ hxy =>
  inv_le_inv_iff.2 (hf hxy)

Premises used: Iff.mpr, inv_le_inv_iff, Antitone
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
β : Type u_1
inst : Group α
inst_1 : Preorder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
inst_4 : Preorder β
f : β → α
hf : Antitone f
⊢ Monotone.{u_1, u} (β := α) fun (x : β) ↦ (f x)⁻¹

Tactic:
fun _ _ hxy =>
  inv_le_inv_iff.2 (hf hxy)

Premises used: Iff.mpr, Monotone, inv_le_inv_iff
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
β : Type u_1
inst : Group α
inst_1 : Preorder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
inst_4 : Preorder β
f : β → α
s : Set β
hf : MonotoneOn f s
⊢ AntitoneOn.{u_1, u} (β := α) (fun (x : β) ↦ (f x)⁻¹) s

Tactic:
fun _ hx _ hy hxy => inv_le_inv_iff.2 (hf hx hy hxy)

Premises used: Iff.mpr, inv_le_inv_iff, AntitoneOn
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
β : Type u_1
inst : Group α
inst_1 : Preorder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
inst_4 : Preorder β
f : β → α
s : Set β
hf : AntitoneOn f s
⊢ MonotoneOn.{u_1, u} (β := α) (fun (x : β) ↦ (f x)⁻¹) s

Tactic:
fun _ hx _ hy hxy => inv_le_inv_iff.2 (hf hx hy hxy)

Premises used: Iff.mpr, inv_le_inv_iff, MonotoneOn
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
β : Type u_1
inst : Group α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
inst_4 : Preorder β
f : β → α
hf : StrictMono f
⊢ StrictAnti.{u_1, u} (β := α) fun (x : β) ↦ (f x)⁻¹

Tactic:
fun _ _ hxy =>
  inv_lt_inv_iff.2 (hf hxy)

Premises used: Iff.mpr, StrictAnti, inv_lt_inv_iff
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
β : Type u_1
inst : Group α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
inst_4 : Preorder β
f : β → α
hf : StrictAnti f
⊢ StrictMono.{u_1, u} (β := α) fun (x : β) ↦ (f x)⁻¹

Tactic:
fun _ _ hxy =>
  inv_lt_inv_iff.2 (hf hxy)

Premises used: Iff.mpr, StrictMono, inv_lt_inv_iff
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
β : Type u_1
inst : Group α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
inst_4 : Preorder β
f : β → α
s : Set β
hf : StrictMonoOn f s
⊢ StrictAntiOn.{u_1, u} (β := α) (fun (x : β) ↦ (f x)⁻¹) s

Tactic:
fun _ hx _ hy hxy => inv_lt_inv_iff.2 (hf hx hy hxy)

Premises used: Iff.mpr, StrictAntiOn, inv_lt_inv_iff
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
β : Type u_1
inst : Group α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
inst_3 : MulRightStrictMono α
inst_4 : Preorder β
f : β → α
s : Set β
hf : StrictAntiOn f s
⊢ StrictMonoOn.{u_1, u} (β := α) (fun (x : β) ↦ (f x)⁻¹) s

Tactic:
fun _ hx _ hy hxy => inv_lt_inv_iff.2 (hf hx hy hxy)

Premises used: Iff.mpr, StrictMonoOn, inv_lt_inv_iff
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
⊢ StrictMono (β := ℤ) fun (x : ℕ) ↦ (↑x : ℤ)

Tactic:
fun _ _ ↦ Int.ofNat_lt.2

Premises used: Iff.mpr, StrictMono, Int.ofNat_lt
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
n : ℤ
⊢ (↑n.natAbs : ℤ) = |n|

Tactic:
n.abs_eq_natAbs.symm

Premises used: Eq.symm, Int.abs_eq_natAbs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
a : ℤ
⊢ |a|.natAbs = a.natAbs

Tactic:
grind
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
a : ℤ
rw : a.sign * (↑a.natAbs : ℤ) = a
rw₁ rw₂ : a = a
⊢ a.sign * |a| = a

Tactic:
rw [abs_eq_natAbs, sign_mul_natAbs a]

Premises used: Int.sign_mul_natAbs, Int.abs_eq_natAbs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
a : ℤ
rw : a.sign * a = (↑a.natAbs : ℤ)
rw₁ rw₂ : Eq (α := ℤ) (↑a.natAbs : ℤ) (↑a.natAbs : ℤ)
⊢ a.sign * a = |a|

Tactic:
rw [abs_eq_natAbs, sign_mul_self_eq_natAbs]

Premises used: Int.sign_mul_self_eq_natAbs, Int.abs_eq_natAbs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
a : ℤ
rw : (↑a.natAbs : ℤ) ≤ HMul.hMul (α := ℤ) (↑a.natAbs : ℤ) (↑a.natAbs : ℤ)
⊢ (↑a.natAbs : ℤ) ≤ HPow.hPow (β := ℕ) a 2

Tactic:
rw [← Int.natAbs_sq a, sq]

Premises used: sq, Int.natAbs_sq
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
a : ℤ
norm_cast : a.natAbs ≤ a.natAbs * a.natAbs
⊢ (↑a.natAbs : ℤ) ≤ HMul.hMul (α := ℤ) (↑a.natAbs : ℤ) (↑a.natAbs : ℤ)

Tactic:
norm_cast
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
a : ℤ
⊢ a.natAbs ≤ a.natAbs * a.natAbs

Tactic:
apply Nat.le_mul_self

Premises used: Nat.le_mul_self
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
b : ℤ
⊢ b ≤ HPow.hPow (β := ℕ) b 2

Tactic:
le_trans le_natAbs (natAbs_le_self_sq _)

Premises used: Int.le_natAbs, Int.natAbs_le_self_sq, le_trans
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
n : ℕ
⊢ Eq (α := ℤ) |(↑n : ℤ)| (↑n : ℤ)

Tactic:
abs_of_nonneg (natCast_nonneg n)

Premises used: abs_of_nonneg, Int.natCast_nonneg
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
i j : ℤ
⊢ 0 < (i - j).natAbs ↔ i ≠ j

Tactic:
grind
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
i j : ℤ
⊢ (i - j).natAbs ≠ 0 ↔ i ≠ j

Tactic:
Nat.ne_zero_iff_zero_lt.trans natAbs_sub_pos_iff

Premises used: Nat.ne_zero_iff_zero_lt, Int.natAbs_sub_pos_iff, Iff.trans
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
a : ℤ
⊢ |a| < 1 ↔ a = 0

Tactic:
grind
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
a : ℤ
⊢ |a| ≤ 1 ↔ a = 0 ∨ a = 1 ∨ a = -1

Tactic:
grind
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
z : ℤ
h₀ : z ≠ 0
⊢ 1 ≤ |z|

Tactic:
add_one_le_iff.mpr (abs_pos.mpr h₀)

Premises used: Iff.mpr, Int.add_one_le_iff, abs_pos, Int.add
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
m x : ℤ
h1 : m ∣ x
h2 : |x| < m
by_contra : ∀ (h : ¬x = 0), False
⊢ x = 0

Tactic:
by_contra h
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
m x : ℤ
h1 : m ∣ x
h2 : |x| < m
h : ¬x = 0
⊢ m.natAbs ≤ x.natAbs

Tactic:
have := Int.natAbs_le_of_dvd_ne_zero h1 h
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
m x : ℤ
h1 : m ∣ x
h2 : |x| < m
h : ¬x = 0
this : m.natAbs ≤ x.natAbs
⊢ (↑x.natAbs : ℤ) < m

Tactic:
rw [Int.abs_eq_natAbs] at h2

Premises used: Int.abs_eq_natAbs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
m x : ℤ
h1 : m ∣ x
h2 : |x| < m
h : ¬x = 0
this : m.natAbs ≤ x.natAbs
h2₁ : (↑x.natAbs : ℤ) < m
⊢ ¬x = 0

Tactic:
rw [Int.abs_eq_natAbs] at h2

Premises used: Int.abs_eq_natAbs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
m x : ℤ
h1 : m ∣ x
h2 : |x| < m
h : ¬x = 0
this : m.natAbs ≤ x.natAbs
h2₁ : (↑x.natAbs : ℤ) < m
h₁ : ¬x = 0
⊢ m.natAbs ≤ x.natAbs

Tactic:
rw [Int.abs_eq_natAbs] at h2

Premises used: Int.abs_eq_natAbs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
m x : ℤ
h1 : m ∣ x
h2 : (↑x.natAbs : ℤ) < m
h : ¬x = 0
this : m.natAbs ≤ x.natAbs
⊢ False

Tactic:
lia
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
m a b : ℕ
ha : a < m
hb : b < m
⊢ |HSub.hSub (α := ℤ) (↑b : ℤ) (↑a : ℤ)| < (↑m : ℤ)

Tactic:
grind
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
a b : ℤ
H1 : 0 ≤ a
H2_1 : a < |b|
n : ℕ
H2 : a < (↑-[n+1].natAbs : ℤ)
rw : a / - -[n+1] = -0
⊢ -(a / -[n+1]) = -0

Tactic:
rw [← Int.ediv_neg]

Premises used: Int.ediv_neg
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
a b : ℤ
H1 : 0 ≤ a
H2_1 : a < |b|
n : ℕ
H2 : a < (↑-[n+1].natAbs : ℤ)
⊢ a / - -[n+1] = -0

Tactic:
ediv_eq_zero_of_lt H1 H2

Premises used: Int.ediv_eq_zero_of_lt, Int.neg, Int.negOfNat
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
a b : ℤ
H1 : 0 ≤ a
H2_1 : a < |b|
n : ℕ
H2 : a < (↑-[n+1].natAbs : ℤ)
⊢ a / - -[n+1] = -0

Tactic:
exact ediv_eq_zero_of_lt H1 H2

Premises used: Int.ediv_eq_zero_of_lt
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
a b : ℤ
⊢ a % |b| = a % b

Tactic:
abs_by_cases (fun i => a % i = a % b) rfl (emod_neg _ _)

Premises used: Int.emod_neg, abs_by_cases, HMod.hMod, Eq, rfl
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
a b : ℤ
H : b ≠ 0
rw : a % |b| < |b|
⊢ a % b < |b|

Tactic:
rw [← emod_abs]

Premises used: Int.emod_abs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
a b : ℤ
H : b ≠ 0
⊢ a % |b| < |b|

Tactic:
emod_lt_of_pos _ (abs_pos.2 H)

Premises used: Iff.mpr, abs_pos, Int.emod_lt_of_pos
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Int
Goal:
a b : ℤ
H : b ≠ 0
⊢ a % |b| < |b|

Tactic:
exact emod_lt_of_pos _ (abs_pos.2 H)

Premises used: Iff.mpr, abs_pos, Int.emod_lt_of_pos