awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a : α
inst_3 : MulRightMono α
⊢ |a|ₘ ≤ 1 ↔ a = 1

Tactic:
(one_le_mabs a).ge_iff_eq'.trans mabs_eq_one

Premises used: LE.le.ge_iff_eq', mabs_eq_one, Iff.trans, one_le_mabs
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a b : α
inst_3 : MulRightMono α
ha : a ≤ 1
hab : b ≤ a
rw : a⁻¹ ≤ b⁻¹
⊢ |a|ₘ ≤ |b|ₘ

Tactic:
rw [mabs_of_le_one ha, mabs_of_le_one (hab.trans ha)]

Premises used: mabs_of_le_one, LE.le.trans
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a b : α
inst_3 : MulRightMono α
ha : a ≤ 1
hab : b ≤ a
⊢ a⁻¹ ≤ b⁻¹

Tactic:
inv_le_inv_iff.mpr hab

Premises used: Iff.mpr, inv_le_inv_iff
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a b : α
inst_3 : MulRightMono α
ha : a ≤ 1
hab : b ≤ a
⊢ a⁻¹ ≤ b⁻¹

Tactic:
exact inv_le_inv_iff.mpr hab

Premises used: Iff.mpr, inv_le_inv_iff
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a b : α
inst_3 : MulRightMono α
rw rw₁ : b⁻¹ < a ∧ a < b ↔ b⁻¹ < a ∧ a < b
⊢ a⁻¹ < b ∧ a < b ↔ b⁻¹ < a ∧ a < b

Tactic:
rw [inv_lt']

Premises used: inv_lt'
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
a b : α
inst_3 : MulRightMono α
h : |a|ₘ < b
⊢ b⁻¹ < a

Tactic:
(mabs_lt.mp h).1

Premises used: And.left, Iff.mp, mabs_lt
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b : α
inl : ∀ (ab : a ≤ b), max a b / min a b = |a / b|ₘ
inr : ∀ (ba : b ≤ a), max a b / min a b = |a / b|ₘ
⊢ max a b / min a b = |a / b|ₘ

Tactic:
rcases le_total a b with ab | ba

Premises used: le_total
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b : α
ab : a ≤ b
inl : a / b ≤ 1
⊢ max a b / min a b = |a / b|ₘ

Tactic:
rw [max_eq_right ab, min_eq_left ab, mabs_of_le_one, inv_div]

Premises used: mabs_of_le_one, max_eq_right, min_eq_left, inv_div
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b : α
ab : a ≤ b
inl inl₁ inl₂ inl₃ : a ≤ b
⊢ a / b ≤ 1

Tactic:
rwa [div_le_one']

Premises used: div_le_one'
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b : α
ba : b ≤ a
inr : 1 ≤ a / b
⊢ max a b / min a b = |a / b|ₘ

Tactic:
rw [max_eq_left ba, min_eq_right ba, mabs_of_one_le]

Premises used: mabs_of_one_le, max_eq_left, min_eq_right
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b : α
ba : b ≤ a
inr inr₁ inr₂ inr₃ : b ≤ a
⊢ 1 ≤ a / b

Tactic:
rwa [one_le_div']

Premises used: one_le_div'
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Group α
inst_1 : LinearOrder α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
a b : α
rw : max a b / min a b = |a / b|ₘ
rw₁ rw₂ : |a / b|ₘ = |a / b|ₘ
⊢ max a b / min a b = |b / a|ₘ

Tactic:
rw [mabs_div_comm, max_div_min_eq_mabs']

Premises used: mabs_div_comm, max_div_min_eq_mabs'
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : AddCommGroup α
s : Set α
⊢ IsSolid (solidClosure s)

Tactic:
fun _ ⟨y, hy, hxy⟩ _ hzx ↦ ⟨y, hy, hzx.trans hxy⟩

Premises used: Membership.mem, LatticeOrderedAddCommGroup.solidClosure, _private.0.LatticeOrderedAddCommGroup.isSolid_solidClosure.match_1, And.intro, Exists.intro, LE.le.trans, LatticeOrderedAddCommGroup.IsSolid
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
α : Type u_1
inst : Lattice α
inst_1 : AddCommGroup α
s t : Set α
hst : s ⊆ t
ht : IsSolid t
⊢ solidClosure s ⊆ t

Tactic:
fun _ ⟨_, hy, hxy⟩ ↦ ht (hst hy) hxy

Premises used: Membership.mem, Set.Subset, _private.0.LatticeOrderedAddCommGroup.solidClosure_min.match_1
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
ι : Type u_2
α : ι → Type u_3
inst : (i : ι) → AddGroup (α i)
inst_1 : (i : ι) → Lattice (α i)
f : (i : ι) → α i
i : ι
⊢ |f| i = |f i|

Tactic:
rfl

Premises used: abs, rfl
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Abs
Goal:
ι : Type u_2
α : ι → Type u_3
inst : (i : ι) → AddGroup (α i)
inst_1 : (i : ι) → Lattice (α i)
f : (i : ι) → α i
⊢ |f| = fun (i : ι) ↦ |f i|

Tactic:
rfl

Premises used: abs, rfl
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a : α
rw : a * a⁻¹ ≤ a * 1 ↔ 1 ≤ a
⊢ a⁻¹ ≤ 1 ↔ 1 ≤ a

Tactic:
rw [← mul_le_mul_iff_left a]

Premises used: mul_le_mul_iff_left
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a : α
⊢ a * a⁻¹ ≤ a * 1 ↔ 1 ≤ a

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a : α
rw : a * 1 ≤ a * a⁻¹ ↔ a ≤ 1
⊢ 1 ≤ a⁻¹ ↔ a ≤ 1

Tactic:
rw [← mul_le_mul_iff_left a]

Premises used: mul_le_mul_iff_left
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a : α
⊢ a * 1 ≤ a * a⁻¹ ↔ a ≤ 1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a b c : α
rw : a * b ≤ a * (a⁻¹ * c) ↔ a * b ≤ c
⊢ b ≤ a⁻¹ * c ↔ a * b ≤ c

Tactic:
rw [← mul_le_mul_iff_left a]

Premises used: mul_le_mul_iff_left
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a b c : α
⊢ a * b ≤ a * (a⁻¹ * c) ↔ a * b ≤ c

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a b c : α
rw : b * (b⁻¹ * a) ≤ b * c ↔ a ≤ b * c
rw₁ rw₂ : a ≤ b * c ↔ a ≤ b * c
⊢ b⁻¹ * a ≤ c ↔ a ≤ b * c

Tactic:
rw [← mul_le_mul_iff_left b, mul_inv_cancel_left]

Premises used: mul_le_mul_iff_left, mul_inv_cancel_left
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a b : α
rw rw₁ : 1 ≤ a * b ↔ 1 ≤ a * b
⊢ a * a⁻¹ ≤ a * b ↔ 1 ≤ a * b

Tactic:
rw [mul_inv_cancel]

Premises used: mul_inv_cancel
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a b : α
rw rw₁ : b * a ≤ 1 ↔ b * a ≤ 1
⊢ b * a ≤ b * b⁻¹ ↔ b * a ≤ 1

Tactic:
rw [mul_inv_cancel]

Premises used: mul_inv_cancel
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a b : α
rw : b * 1 ≤ b * (b⁻¹ * a) ↔ b ≤ a
rw₁ : b ≤ b * (b⁻¹ * a) ↔ b ≤ a
rw₂ rw₃ : b ≤ a ↔ b ≤ a
⊢ 1 ≤ b⁻¹ * a ↔ b ≤ a

Tactic:
rw [← mul_le_mul_iff_left b, mul_one, mul_inv_cancel_left]

Premises used: mul_le_mul_iff_left, mul_one, mul_inv_cancel_left
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a b : α
rw rw₁ : b ≤ a ↔ b ≤ a
⊢ b ≤ a * 1 ↔ b ≤ a

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a : α
rw : a * 1 < a * a⁻¹ ↔ a < 1
rw₁ : a * 1 < 1 ↔ a < 1
rw₂ rw₃ : a < 1 ↔ a < 1
⊢ 1 < a⁻¹ ↔ a < 1

Tactic:
rw [← mul_lt_mul_iff_left a, mul_inv_cancel, mul_one]

Premises used: mul_lt_mul_iff_left, mul_inv_cancel, mul_one
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a : α
rw : a * a⁻¹ < a * 1 ↔ 1 < a
rw₁ : 1 < a * 1 ↔ 1 < a
rw₂ rw₃ : 1 < a ↔ 1 < a
⊢ a⁻¹ < 1 ↔ 1 < a

Tactic:
rw [← mul_lt_mul_iff_left a, mul_inv_cancel, mul_one]

Premises used: mul_lt_mul_iff_left, mul_inv_cancel, mul_one
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b c : α
rw : a * b < a * (a⁻¹ * c) ↔ a * b < c
⊢ b < a⁻¹ * c ↔ a * b < c

Tactic:
rw [← mul_lt_mul_iff_left a]

Premises used: mul_lt_mul_iff_left
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b c : α
⊢ a * b < a * (a⁻¹ * c) ↔ a * b < c

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b c : α
rw : b * (b⁻¹ * a) < b * c ↔ a < b * c
rw₁ rw₂ : a < b * c ↔ a < b * c
⊢ b⁻¹ * a < c ↔ a < b * c

Tactic:
rw [← mul_lt_mul_iff_left b, mul_inv_cancel_left]

Premises used: mul_lt_mul_iff_left, mul_inv_cancel_left
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b : α
rw rw₁ : 1 < a * b ↔ 1 < a * b
⊢ a * a⁻¹ < a * b ↔ 1 < a * b

Tactic:
rw [mul_inv_cancel]

Premises used: mul_inv_cancel
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b : α
rw rw₁ : b * a < 1 ↔ b * a < 1
⊢ b * a < b * b⁻¹ ↔ b * a < 1

Tactic:
rw [mul_inv_cancel]

Premises used: mul_inv_cancel
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b : α
rw : b * 1 < b * (b⁻¹ * a) ↔ b < a
rw₁ : b < b * (b⁻¹ * a) ↔ b < a
rw₂ rw₃ : b < a ↔ b < a
⊢ 1 < b⁻¹ * a ↔ b < a

Tactic:
rw [← mul_lt_mul_iff_left b, mul_one, mul_inv_cancel_left]

Premises used: mul_lt_mul_iff_left, mul_one, mul_inv_cancel_left
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b : α
rw rw₁ : b < a ↔ b < a
⊢ b < a * 1 ↔ b < a

Tactic:
rw [mul_one]

Premises used: mul_one
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulRightMono α
a : α
rw : a⁻¹ * a ≤ 1 * a ↔ 1 ≤ a
⊢ a⁻¹ ≤ 1 ↔ 1 ≤ a

Tactic:
rw [← mul_le_mul_iff_right a]

Premises used: mul_le_mul_iff_right
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulRightMono α
a : α
⊢ a⁻¹ * a ≤ 1 * a ↔ 1 ≤ a

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulRightMono α
a : α
rw : 1 * a ≤ a⁻¹ * a ↔ a ≤ 1
⊢ 1 ≤ a⁻¹ ↔ a ≤ 1

Tactic:
rw [← mul_le_mul_iff_right a]

Premises used: mul_le_mul_iff_right
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulRightMono α
a : α
⊢ 1 * a ≤ a⁻¹ * a ↔ a ≤ 1

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulRightMono α
a b : α
rw rw₁ : 1 ≤ b * a ↔ 1 ≤ b * a
⊢ a⁻¹ * a ≤ b * a ↔ 1 ≤ b * a

Tactic:
rw [inv_mul_cancel]

Premises used: inv_mul_cancel
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulRightMono α
a b : α
rw rw₁ : a * b ≤ 1 ↔ a * b ≤ 1
⊢ a * b ≤ b⁻¹ * b ↔ a * b ≤ 1

Tactic:
rw [inv_mul_cancel]

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

Tactic:
rw [inv_mul_cancel_right]

Premises used: 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 rw₁ : c * b ≤ a ↔ c * b ≤ a
⊢ c * b ≤ a * b⁻¹ * b ↔ c * b ≤ a

Tactic:
rw [inv_mul_cancel_right]

Premises used: inv_mul_cancel_right
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulRightMono α
a b : α
rw rw₁ : a ≤ b ↔ a ≤ b
⊢ a ≤ 1 * b ↔ a ≤ b

Tactic:
rw [one_mul]

Premises used: one_mul
-- 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₂ rw₃ : b ≤ a ↔ b ≤ a
⊢ 1 ≤ a * b⁻¹ ↔ b ≤ a

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

Premises used: mul_le_mul_iff_right, 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 rw₁ : b ≤ a ↔ b ≤ a
⊢ b ≤ 1 * a ↔ b ≤ a

Tactic:
rw [one_mul]

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

Tactic:
rw [← mul_lt_mul_iff_right a, inv_mul_cancel, one_mul]

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

Tactic:
rw [← mul_lt_mul_iff_right a, inv_mul_cancel, one_mul]

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

Tactic:
rw [inv_mul_cancel]

Premises used: inv_mul_cancel
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulRightStrictMono α
a b : α
rw rw₁ : a * b < 1 ↔ a * b < 1
⊢ a * b < b⁻¹ * b ↔ a * b < 1

Tactic:
rw [inv_mul_cancel]

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

Tactic:
rw [← mul_lt_mul_iff_right b, inv_mul_cancel_right]

Premises used: 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 rw₁ : c * b < a ↔ c * b < a
⊢ c * b < a * b⁻¹ * b ↔ c * b < a

Tactic:
rw [inv_mul_cancel_right]

Premises used: inv_mul_cancel_right
-- 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 < 1 * b ↔ a < b
rw₂ rw₃ : a < b ↔ a < b
⊢ a * b⁻¹ < 1 ↔ a < b

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

Premises used: 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 : 1 * 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, inv_mul_cancel_right]

Premises used: 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 rw₁ : b < a ↔ b < a
⊢ b < 1 * a ↔ b < a

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a b : α
⊢ a / b ≤ a ↔ 1 ≤ b

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a b : α
⊢ a ≤ a / b ↔ b ≤ 1

Tactic:
simp [div_eq_mul_inv]

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

Tactic:
rw [← mul_le_mul_iff_left a, ← mul_le_mul_iff_right b]

Premises used: mul_le_mul_iff_right, mul_le_mul_iff_left
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a b : α
inst_3 : MulRightMono α
⊢ a * a⁻¹ * b ≤ a * b⁻¹ * b ↔ b ≤ a

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulLeftMono α
a b c d : α
inst_3 : MulRightMono α
rw : d * (a * b⁻¹) ≤ d * (d⁻¹ * c) ↔ d * a ≤ c * b
rw₁ : d * (a * b⁻¹) * b ≤ d * (d⁻¹ * c) * b ↔ d * a ≤ c * b
rw₂ : d * (a * b⁻¹) * b ≤ c * b ↔ d * a ≤ c * b
rw₃ : d * (a * b⁻¹ * b) ≤ c * b ↔ d * a ≤ c * b
rw₄ rw₅ : d * a ≤ c * b ↔ d * a ≤ c * b
⊢ a * b⁻¹ ≤ d⁻¹ * c ↔ d * a ≤ c * b

Tactic:
rw [← mul_le_mul_iff_left d, ← mul_le_mul_iff_right b, mul_inv_cancel_left, mul_assoc,
    inv_mul_cancel_right]

Premises used: mul_le_mul_iff_right, mul_assoc, mul_le_mul_iff_left, mul_inv_cancel_left, inv_mul_cancel_right
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b : α
⊢ a / b < a ↔ 1 < b

Tactic:
simp [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b : α
inst_3 : MulRightStrictMono α
rw : a * a⁻¹ * b < a * b⁻¹ * b ↔ b < a
⊢ a⁻¹ < b⁻¹ ↔ b < a

Tactic:
rw [← mul_lt_mul_iff_left a, ← mul_lt_mul_iff_right b]

Premises used: mul_lt_mul_iff_left, mul_lt_mul_iff_right
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b : α
inst_3 : MulRightStrictMono α
⊢ a * a⁻¹ * b < a * b⁻¹ * b ↔ b < a

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b : α
inst_3 : MulRightStrictMono α
rw : b⁻¹ < a⁻¹⁻¹ ↔ b⁻¹ < a
rw₁ rw₂ : b⁻¹ < a ↔ b⁻¹ < a
⊢ a⁻¹ < b ↔ b⁻¹ < a

Tactic:
rw [← inv_lt_inv_iff, inv_inv]

Premises used: inv_inv, inv_lt_inv_iff
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LT α
inst_2 : MulLeftStrictMono α
a b : α
inst_3 : MulRightStrictMono α
rw : b⁻¹⁻¹ < a⁻¹ ↔ b < a⁻¹
rw₁ rw₂ : b < a⁻¹ ↔ b < a⁻¹
⊢ a < b⁻¹ ↔ b < a⁻¹

Tactic:
rw [← inv_lt_inv_iff, inv_inv]

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

Tactic:
rw [← mul_lt_mul_iff_left d, ← mul_lt_mul_iff_right b, mul_inv_cancel_left, mul_assoc,
    inv_mul_cancel_right]

Premises used: mul_lt_mul_iff_left, mul_assoc, mul_lt_mul_iff_right, mul_inv_cancel_left, inv_mul_cancel_right
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a : α
h : 1 ≤ a
⊢ a⁻¹ ≤ a

Tactic:
le_trans (Left.inv_le_one_iff.mpr h) h

Premises used: Iff.mpr, Left.inv_le_one_iff, le_trans
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : Preorder α
inst_2 : MulLeftMono α
a : α
h : a ≤ 1
⊢ a ≤ a⁻¹

Tactic:
le_trans h (Left.one_le_inv_iff.mpr h)

Premises used: Iff.mpr, Left.one_le_inv_iff, le_trans
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
a : α
h : 1 < a
⊢ a⁻¹ < a

Tactic:
(Left.inv_lt_one_iff.mpr h).trans h

Premises used: Iff.mpr, Left.inv_lt_one_iff, LT.lt.trans
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : Preorder α
inst_2 : MulLeftStrictMono α
a : α
h : a < 1
⊢ a < a⁻¹

Tactic:
lt_trans h (Left.one_lt_inv_iff.mpr h)

Premises used: Iff.mpr, lt_trans, Left.one_lt_inv_iff
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : Preorder α
inst_2 : MulRightMono α
a : α
h : 1 ≤ a
⊢ a⁻¹ ≤ a

Tactic:
le_trans (Right.inv_le_one_iff.mpr h) h

Premises used: Iff.mpr, Right.inv_le_one_iff, le_trans
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : Preorder α
inst_2 : MulRightMono α
a : α
h : a ≤ 1
⊢ a ≤ a⁻¹

Tactic:
le_trans h (Right.one_le_inv_iff.mpr h)

Premises used: Iff.mpr, Right.one_le_inv_iff, le_trans
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : Preorder α
inst_2 : MulRightStrictMono α
a : α
h : 1 < a
⊢ a⁻¹ < a

Tactic:
(Right.inv_lt_one_iff.mpr h).trans h

Premises used: Iff.mpr, Right.inv_lt_one_iff, LT.lt.trans
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : Preorder α
inst_2 : MulRightStrictMono α
a : α
h : a < 1
⊢ a < a⁻¹

Tactic:
lt_trans h (Right.one_lt_inv_iff.mpr h)

Premises used: Iff.mpr, Right.one_lt_inv_iff, lt_trans
-- 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
⊢ c⁻¹ * a ≤ b ↔ a ≤ b * c

Tactic:
rw [inv_mul_le_iff_le_mul, mul_comm]

Premises used: mul_comm, inv_mul_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 : α
rw : a * b⁻¹ ≤ c ↔ b⁻¹ * a ≤ c
rw₁ rw₂ : b⁻¹ * a ≤ c ↔ b⁻¹ * a ≤ c
⊢ a * b⁻¹ ≤ c ↔ a ≤ b * c

Tactic:
rw [← inv_mul_le_iff_le_mul, mul_comm]

Premises used: mul_comm, inv_mul_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 d : α
rw : a * b⁻¹ ≤ d⁻¹ * c ↔ a * d ≤ c * b
rw₁ : d * a ≤ c * b ↔ a * d ≤ c * b
rw₂ rw₃ : a * d ≤ c * b ↔ a * d ≤ c * b
⊢ a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b

Tactic:
rw [mul_comm c, mul_inv_le_inv_mul_iff, mul_comm]

Premises used: mul_comm, mul_inv_le_inv_mul_iff
-- 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
⊢ c⁻¹ * a < b ↔ a < b * c

Tactic:
rw [inv_mul_lt_iff_lt_mul, mul_comm]

Premises used: inv_mul_lt_iff_lt_mul, 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 * b⁻¹ < c ↔ b⁻¹ * a < c
rw₁ rw₂ : b⁻¹ * a < c ↔ b⁻¹ * a < c
⊢ a * b⁻¹ < c ↔ a < b * c

Tactic:
rw [← inv_mul_lt_iff_lt_mul, mul_comm]

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

Tactic:
rw [mul_comm c, mul_inv_lt_inv_mul_iff, mul_comm]

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

Tactic:
simpa only [div_eq_mul_inv] using mul_le_mul_iff_right _

Premises used: mul_le_mul_iff_right, div_eq_mul_inv
-- Module: Mathlib.Algebra.Order.Group.Unbundled.Basic
Goal:
α : Type u
inst : Group α
inst_1 : LE α
inst_2 : MulRightMono α
a b : α
h : a ≤ b
c : α
⊢ a / c ≤ b / c

Tactic:
(div_le_div_iff_right c).2 h

Premises used: Iff.mpr, div_le_div_iff_right